diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index a51fc7ba..77dee04d 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -156,7 +156,25 @@ module RISCV ``` `#NEXT[ I ]` sets up the pipeline to execute the the fetched instruction. ```k - rule #NEXT[ I ] => I ~> #CHECK_HALT ... + rule #NEXT[ I ] => I ~> #PC[ I ] ~> #CHECK_HALT ... +``` +`#PC[ I ]` updates the `PC` as needed to fetch the next instruction after executing `I`. For most instructions, this increments `PC` by the width of the instruction (always `4` bytes in the base ISA). For branch and jump instructions, which already manually update the `PC`, this is a no-op. +```k + syntax KItem ::= "#PC" "[" Instruction "]" + + rule #PC[ I ] => .K ... + PC => PC +Word pcIncrAmount(I) + + syntax Word ::= pcIncrAmount(Instruction) [function, total] + rule pcIncrAmount(BEQ _ , _ , _ ) => W(0) + rule pcIncrAmount(BNE _ , _ , _ ) => W(0) + rule pcIncrAmount(BLT _ , _ , _ ) => W(0) + rule pcIncrAmount(BLTU _ , _ , _ ) => W(0) + rule pcIncrAmount(BGE _ , _ , _ ) => W(0) + rule pcIncrAmount(BGEU _ , _ , _ ) => W(0) + rule pcIncrAmount(JAL _ , _ ) => W(0) + rule pcIncrAmount(JALR _ , _ ( _ )) => W(0) + rule pcIncrAmount(_) => W(4) [owise] ``` We then provide rules to consume and execute each instruction from the top of the pipeline. @@ -164,103 +182,83 @@ We then provide rules to consume and execute each instruction from the top of th ```k rule ADDI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) +Word chop(IMM)) - PC => PC +Word W(4) ``` `SLTI` treats the value in `RS` as a signed two's complement and compares it to `IMM`, writing `1` to `RD` if `RS` is less than `IMM` and `0` otherwise. ```k rule SLTI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS) - PC => PC +Word W(4) ``` `SLTIU` proceeds analogously, but treating `RS` and `IMM` as XLEN-bit unsigned integers. ```k rule SLTIU RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS) - PC => PC +Word W(4) ``` `ADDI`, `ORI`, and `XORI` perform bitwise operations between `RS` and `IMM`, storing the result in `RD`. ```k rule ANDI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) &Word chop(IMM)) - PC => PC +Word W(4) rule ORI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) |Word chop(IMM)) - PC => PC +Word W(4) rule XORI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) xorWord chop(IMM)) - PC => PC +Word W(4) ``` `SLLI`, `SRLI`, and `SRAI` perform logical left, logical right, and arithmetic right shifts respectively. ```k rule SLLI RD , RS , SHAMT => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) < - PC => PC +Word W(4) rule SRLI RD , RS , SHAMT => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) >>lWord SHAMT) - PC => PC +Word W(4) rule SRAI RD , RS , SHAMT => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) >>aWord SHAMT) - PC => PC +Word W(4) ``` `LUI` builds a 32-bit constant from the 20-bit immediate by setting the 12 least-significant bits to `0`, then sign extends to `XLEN` bits and places the result in register `RD`. ```k rule LUI RD , IMM => .K ... REGS => writeReg(REGS, RD, signExtend(IMM < - PC => PC +Word W(4) ``` `AUIPC` proceeds similarly to `LUI`, but adding the sign-extended constant to the current `PC` before placing the result in `RD`. ```k rule AUIPC RD , IMM => .K ... REGS => writeReg(REGS, RD, PC +Word signExtend(IMM < - PC => PC +Word W(4) + PC ``` The following instructions behave analogously to their `I`-suffixed counterparts, but taking their second argument from an `RS2` register rather than an immediate. ```k rule ADD RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) +Word readReg(REGS, RS2)) - PC => PC +Word W(4) rule SUB RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) -Word readReg(REGS, RS2)) - PC => PC +Word W(4) rule SLT RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS1) - PC => PC +Word W(4) rule SLTU RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS1) - PC => PC +Word W(4) rule AND RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) &Word readReg(REGS, RS2)) - PC => PC +Word W(4) rule OR RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) |Word readReg(REGS, RS2)) - PC => PC +Word W(4) rule XOR RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) xorWord readReg(REGS, RS2)) - PC => PC +Word W(4) ``` `SLL`, `SRL`, and `SRA` read their shift amount fom the lowest `log_2(XLEN)` bits of `RS2`. ```k rule SLL RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) < - PC => PC +Word W(4) rule SRL RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>lWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) - PC => PC +Word W(4) rule SRA RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>aWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) - PC => PC +Word W(4) ``` `JAL` stores `PC + 4` in `RD`, then increments `PC` by `OFFSET`. ```k @@ -336,46 +334,38 @@ The remaining branch instructions proceed analogously, but performing different ```k rule LB RD , OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, signExtend(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)), 8)) - PC => PC +Word W(4) MEM rule LH RD , OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2), 16)) - PC => PC +Word W(4) MEM rule LW RD , OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 4), 32)) - PC => PC +Word W(4) MEM ``` `LBU` and `LHU` are analogous to `LB` and `LH`, but zero-extending rather than sign-extending. ```k rule LBU RD , OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, W(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)))) - PC => PC +Word W(4) MEM rule LHU RD , OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, W(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2))) - PC => PC +Word W(4) MEM ``` Dually, `SB`, `SH`, and `SW` store the least-significant `1`, `2`, and `4` bytes respectively from `RS2` to the memory address which is `OFFSET` greater than the value in register `RS1`. ```k rule SB RS2 , OFFSET ( RS1 ) => .K ... REGS - PC => PC +Word W(4) MEM => storeByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 255) rule SH RS2 , OFFSET ( RS1 ) => .K ... REGS - PC => PC +Word W(4) MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 65535, 2) rule SW RS2 , OFFSET ( RS1 ) => .K ... REGS - PC => PC +Word W(4) MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 4294967295, 4) ``` We presume a single hart with exclusive access to memory, so `FENCE` and `FENCE.TSO` are no-ops.