summaryrefslogtreecommitdiff
path: root/risc-v/riscv.sail
diff options
context:
space:
mode:
Diffstat (limited to 'risc-v/riscv.sail')
-rw-r--r--risc-v/riscv.sail497
1 files changed, 292 insertions, 205 deletions
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 4a80adb0..3d52d111 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -1,317 +1,404 @@
-default Order dec
-
-typedef regval = bit[64]
-typedef regno = bit[5]
-
-register (regval) x0
-register (regval) x1
-register (regval) x2
-register (regval) x3
-register (regval) x4
-register (regval) x5
-register (regval) x6
-register (regval) x7
-register (regval) x8
-register (regval) x9
-register (regval) x10
-register (regval) x11
-register (regval) x12
-register (regval) x13
-register (regval) x14
-register (regval) x15
-register (regval) x16
-register (regval) x17
-register (regval) x18
-register (regval) x19
-register (regval) x20
-register (regval) x21
-register (regval) x22
-register (regval) x23
-register (regval) x24
-register (regval) x25
-register (regval) x26
-register (regval) x27
-register (regval) x28
-register (regval) x29
-register (regval) x30
-register (regval) x31
-
-register (bit[64]) PC
-register (bit[64]) nextPC
-
-let (vector <0, 32, inc, (register<(regval)>)>) GPRs =
- [x0, x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31]
-
-function (regval) rGPR ((regno) r) =
- if (r == 0) then
- 0
- else
- GPRs[r]
-
-function unit wGPR((regno) r, (regval) v) =
- if (r != 0) then
- GPRs[r] := v
-
-function forall 'a. 'a effect { escape } not_implemented((string) message) =
-{
- exit message;
-}
-
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
-val extern unit -> unit effect { barr } MEM_fence_rw_rw
-val extern unit -> unit effect { barr } MEM_fence_r_rw
-val extern unit -> unit effect { barr } MEM_fence_rw_w
-
-(* Ideally these would be sail builtin *)
-function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
- let (bit[128]) v128 = EXTS(v) in
- (v128 >> shift)[63..0]
-
-function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) =
- let (bit[64]) v64 = EXTS(v) in
- (v64 >> shift)[31..0]
-
-typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
-typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
-typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
-typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
-typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
-typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
-
-typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
-
-scattered function unit execute
scattered typedef ast = const union
val bit[32] -> option<ast> effect pure decode
-
scattered function option<ast> decode
+scattered function unit execute
+
+(********************************************************************)
union ast member ((bit[20]), regno, uop) UTYPE
-function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI))
-function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC))
+function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, RISCV_LUI))
+function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, RISCV_AUIPC))
function clause execute (UTYPE(imm, rd, op)) =
let (bit[64]) off = EXTS(imm : 0x000) in
let ret = switch (op) {
- case LUI -> off
- case AUIPC -> PC + off
+ case RISCV_LUI -> off
+ case RISCV_AUIPC -> PC + off
} in
wGPR(rd, ret)
-union ast member ((bit[21]), regno) JAL
-function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
-function clause execute (JAL(imm, rd)) =
- let (bit[64]) offset = EXTS(imm) in {
- nextPC := PC + offset;
- wGPR(rd, PC + 4);
- }
+(********************************************************************)
+union ast member ((bit[21]), regno) RISCV_JAL
+
+function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (RISCV_JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
+
+function clause execute (RISCV_JAL(imm, rd)) = {
+ (bit[64]) pc := PC;
+ wGPR(rd, pc + 4);
+ (bit[64]) offset := EXTS(imm);
+ nextPC := pc + offset;
+}
+
+(********************************************************************)
+union ast member((bit[12]), regno, regno) RISCV_JALR
-union ast member((bit[12]), regno, regno) JALR
function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) =
- Some(JALR(imm, rs1, rd))
-function clause execute (JALR(imm, rs1, rd)) =
- let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in {
- nextPC := newPC[63..1] : 0b0;
- wGPR(rd, PC + 4);
- }
+ Some(RISCV_JALR(imm, rs1, rd))
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+ (* write rd before anything else to prevent unintended strength *)
+ wGPR(rd, PC + 4);
+ (bit[64]) newPC := rGPR(rs1) + EXTS(imm);
+ nextPC := newPC[63..1] : 0b0;
+}
+
+(********************************************************************)
union ast member ((bit[13]), regno, regno, bop) BTYPE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
+
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BEQ))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BNE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BLT))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BGE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BLTU))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) =
+ Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BGEU))
function clause execute (BTYPE(imm, rs2, rs1, op)) =
let rs1_val = rGPR(rs1) in
let rs2_val = rGPR(rs2) in
let taken = switch(op) {
- case BEQ -> rs1_val == rs2_val
- case BNE -> rs1_val != rs2_val
- case BLT -> rs1_val <_s rs2_val
- case BGE -> rs1_val >=_s rs2_val
- case BLTU -> rs1_val <_u rs2_val
- case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
+ case RISCV_BEQ -> rs1_val == rs2_val
+ case RISCV_BNE -> rs1_val != rs2_val
+ case RISCV_BLT -> rs1_val <_s rs2_val
+ case RISCV_BGE -> rs1_val >=_s rs2_val
+ case RISCV_BLTU -> rs1_val <_u rs2_val
+ case RISCV_BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
} in
if (taken) then
nextPC := PC + EXTS(imm)
+(********************************************************************)
union ast member ((bit[12]), regno, regno, iop) ITYPE
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI))
+
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_XORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ANDI))
+
function clause execute (ITYPE (imm, rs1, rd, op)) =
let rs1_val = rGPR(rs1) in
let imm64 = (bit[64]) (EXTS(imm)) in
let (bit[64]) result = switch(op) {
- case ADDI -> rs1_val + imm64
- case SLTI -> EXTZ(rs1_val <_s imm64)
- case SLTIU -> EXTZ(rs1_val <_u imm64)
- case XORI -> rs1_val ^ imm64
- case ORI -> rs1_val | imm64
- case ANDI -> rs1_val & imm64
+ case RISCV_ADDI -> rs1_val + imm64
+ case RISCV_SLTI -> EXTZ(rs1_val <_s imm64)
+ case RISCV_SLTIU -> EXTZ(rs1_val <_u imm64)
+ case RISCV_XORI -> rs1_val ^ imm64
+ case RISCV_ORI -> rs1_val | imm64
+ case RISCV_ANDI -> rs1_val & imm64
} in
wGPR(rd, result)
+(********************************************************************)
union ast member ((bit[6]), regno, regno, sop) SHIFTIOP
-function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI))
-function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI))
-function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI))
+
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))
+
function clause execute (SHIFTIOP(shamt, rs1, rd, op)) =
let rs1_val = rGPR(rs1) in
let result = switch(op) {
- case SLLI -> rs1_val >> shamt
- case SRLI -> rs1_val << shamt
- case SRAI -> shift_right_arith64(rs1_val, shamt)
+ case RISCV_SLLI -> rs1_val >> shamt
+ case RISCV_SRLI -> rs1_val << shamt
+ case RISCV_SRAI -> shift_right_arith64(rs1_val, shamt)
} in
wGPR(rd, result)
+(********************************************************************)
union ast member (regno, regno, regno, rop) RTYPE
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND))
+
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_AND))
+
function clause execute (RTYPE(rs2, rs1, rd, op)) =
let rs1_val = rGPR(rs1) in
let rs2_val = rGPR(rs2) in
let (bit[64]) result = switch(op) {
- case ADD -> rs1_val + rs2_val
- case SUB -> rs1_val - rs2_val
- case SLL -> rs1_val << (rs2_val[5..0])
- case SLT -> EXTZ(rs1_val <_s rs2_val)
- case SLTU -> EXTZ(rs1_val <_u rs2_val)
- case XOR -> rs1_val ^ rs2_val
- case SRL -> rs1_val >> (rs2_val[5..0])
- case SRA -> shift_right_arith64(rs1_val, rs2_val[5..0])
- case OR -> rs1_val | rs2_val
- case AND -> rs1_val & rs2_val
+ case RISCV_ADD -> rs1_val + rs2_val
+ case RISCV_SUB -> rs1_val - rs2_val
+ case RISCV_SLL -> rs1_val << (rs2_val[5..0])
+ case RISCV_SLT -> EXTZ(rs1_val <_s rs2_val)
+ case RISCV_SLTU -> EXTZ(rs1_val <_u rs2_val)
+ case RISCV_XOR -> rs1_val ^ rs2_val
+ case RISCV_SRL -> rs1_val >> (rs2_val[5..0])
+ case RISCV_SRA -> shift_right_arith64(rs1_val, rs2_val[5..0])
+ case RISCV_OR -> rs1_val | rs2_val
+ case RISCV_AND -> rs1_val & rs2_val
} in
wGPR(rd, result)
-union ast member ((bit[12]), regno, regno, bool, word_width) LOAD
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD))
-function clause execute(LOAD(imm, rs1, rd, unsigned, width)) =
+(********************************************************************)
+union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD
+
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD, false, false))
+
+function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
let (bit[64]) result = if unsigned then
switch (width) {
- case BYTE -> EXTZ(MEMr(addr, 1))
- case HALF -> EXTZ(MEMr(addr, 2))
- case WORD -> EXTZ(MEMr(addr, 4))
- case DOUBLE -> MEMr(addr, 8)
+ case BYTE -> EXTZ(mem_read(addr, 1, aq, rl, false))
+ case HALF -> EXTZ(mem_read(addr, 2, aq, rl, false))
+ case WORD -> EXTZ(mem_read(addr, 4, aq, rl, false))
+ case DOUBLE -> mem_read(addr, 8, aq, rl, false)
}
else
switch (width) {
- case BYTE -> EXTS(MEMr(addr, 1))
- case HALF -> EXTS(MEMr(addr, 2))
- case WORD -> EXTS(MEMr(addr, 4))
- case DOUBLE -> MEMr(addr, 8)
+ case BYTE -> EXTS(mem_read(addr, 1, aq, rl, false))
+ case HALF -> EXTS(mem_read(addr, 2, aq, rl, false))
+ case WORD -> EXTS(mem_read(addr, 4, aq, rl, false))
+ case DOUBLE -> mem_read(addr, 8, aq, rl, false)
} in
wGPR(rd, result)
-union ast member ((bit[12]), regno, regno, word_width) STORE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE))
-function clause execute (STORE(imm, rs2, rs1, width)) =
+(********************************************************************)
+union ast member ((bit[12]), regno, regno, word_width, bool, bool) STORE
+
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) =
+ Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) =
+ Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) =
+ Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) =
+ Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false))
+
+function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
switch (width) {
- case BYTE -> MEMea(addr, 1)
- case HALF -> MEMea(addr, 2)
- case WORD -> MEMea(addr, 4)
- case DOUBLE -> MEMea(addr, 8)
+ case BYTE -> mem_write_ea(addr, 1, aq, rl, false)
+ case HALF -> mem_write_ea(addr, 2, aq, rl, false)
+ case WORD -> mem_write_ea(addr, 4, aq, rl, false)
+ case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false)
};
let rs2_val = rGPR(rs2) in
switch (width) {
- case BYTE -> MEMval(addr, 1, rs2_val[7..0])
- case HALF -> MEMval(addr, 2, rs2_val[15..0])
- case WORD -> MEMval(addr, 4, rs2_val[31..0])
- case DOUBLE -> MEMval(addr, 8, rs2_val)
+ case BYTE -> mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false)
+ case HALF -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false)
+ case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false)
+ case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, false)
}
}
+(********************************************************************)
union ast member ((bit[12]), regno, regno) ADDIW
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd))
+
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) =
+ Some(ADDIW(imm, rs1, rd))
+
function clause execute (ADDIW(imm, rs1, rd)) =
let (bit[64]) imm64 = EXTS(imm) in
let (bit[64]) result64 = imm64 + rGPR(rs1) in
let (bit[64]) result32 = EXTS(result64[31..0]) in
wGPR(rd, result32)
+(********************************************************************)
union ast member ((bit[5]), regno, regno, sop) SHIFTW
-function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI))
-function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI))
-function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI))
+
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
+
function clause execute (SHIFTW(shamt, rs1, rd, op)) =
let rs1_val = (rGPR(rs1))[31..0] in
let result = switch(op) {
- case SLLI -> rs1_val >> shamt
- case SRLI -> rs1_val << shamt
- case SRAI -> shift_right_arith32(rs1_val, shamt)
+ case RISCV_SLLI -> rs1_val >> shamt
+ case RISCV_SRLI -> rs1_val << shamt
+ case RISCV_SRAI -> shift_right_arith32(rs1_val, shamt)
} in
wGPR(rd, EXTS(result))
+(********************************************************************)
union ast member (regno, regno, regno, ropw) RTYPEW
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW))
+
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))
+
function clause execute (RTYPEW(rs2, rs1, rd, op)) =
let rs1_val = (rGPR(rs1))[31..0] in
let rs2_val = (rGPR(rs2))[31..0] in
let (bit[32]) result = switch(op) {
- case ADDW -> rs1_val + rs2_val
- case SUBW -> rs1_val - rs2_val
- case SLLW -> rs1_val << (rs2_val[4..0])
- case SRLW -> rs1_val >> (rs2_val[4..0])
- case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
+ case RISCV_ADDW -> rs1_val + rs2_val
+ case RISCV_SUBW -> rs1_val - rs2_val
+ case RISCV_SLLW -> rs1_val << (rs2_val[4..0])
+ case RISCV_SRLW -> rs1_val >> (rs2_val[4..0])
+ case RISCV_SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
} in
wGPR(rd, EXTS(result))
+(********************************************************************)
union ast member (bit[4], bit[4]) FENCE
+
function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ))
+
function clause execute (FENCE(pred, succ)) = {
switch(pred, succ) {
case (0b0011, 0b0011) -> MEM_fence_rw_rw()
case (0b0010, 0b0011) -> MEM_fence_r_rw()
+ case (0b0010, 0b0010) -> MEM_fence_r_r()
case (0b0011, 0b0001) -> MEM_fence_rw_w()
+ case (0b0001, 0b0001) -> MEM_fence_w_w()
case _ -> not_implemented("unsupported fence")
}
}
+(********************************************************************)
union ast member unit FENCEI
-function clause decode (0b0000 : 0b0000 : 0b0000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
-function clause execute FENCEI = () (* XXX TODO *)
+function clause decode (0b000000000000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
+function clause execute FENCEI = MEM_fence_i()
+(********************************************************************)
union ast member unit ECALL
function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ())
-function clause execute ECALL = ()
+function clause execute ECALL = not_implemented("ECALL is not implemented")
+(********************************************************************)
union ast member unit EBREAK
function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ())
function clause execute EBREAK = { exit () }
+(********************************************************************)
+union ast member (bool, bool, regno, word_width, regno) LOADRES
+
+function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
+function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
+function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
+ let (bit[64]) addr = rGPR(rs1) in
+ let (bit[64]) result =
+ switch width {
+ case WORD -> EXTS(mem_read(addr, 4, aq, rl, true))
+ case DOUBLE -> mem_read(addr, 8, aq, rl, true)
+ } in
+ wGPR(rd, result)
+
+(********************************************************************)
+union ast member (bool, bool, regno, regno, word_width, regno) STORECON
+
+function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
+
+function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
+ (*(bit)*) status := if speculate_conditional_success() then 0 else 1;
+ wGPR(rd) := (bit[64]) (EXTZ([status]));
+
+ if status == 1 then () else {
+ (bit[64]) addr := rGPR(rs1);
+ switch width {
+ case WORD -> mem_write_ea(addr, 4, aq, rl, true)
+ case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true)
+ };
+ rs2_val := rGPR(rs2);
+ switch width {
+ case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true)
+ case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, true)
+ };
+ };
+}
+
+(********************************************************************)
+union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO
+
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+ Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+
+function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
+ (bit[64]) addr := rGPR(rs1);
+
+ switch (width) {
+ case WORD -> mem_write_ea(addr, 4, aq & rl, rl, true)
+ case DOUBLE -> mem_write_ea(addr, 8, aq & rl, rl, true)
+ };
+
+ (bit[64]) loaded :=
+ switch (width) {
+ case WORD -> EXTS(mem_read(addr, 4, aq, aq & rl, true))
+ case DOUBLE -> mem_read(addr, 8, aq, aq & rl, true)
+ };
+ wGPR(rd, loaded);
+
+ (bit[64]) rs2_val := rGPR(rs2);
+ (bit[64]) result :=
+ switch(op) {
+ case AMOSWAP -> rs2_val
+ case AMOADD -> rs2_val + loaded
+ case AMOXOR -> rs2_val ^ loaded
+ case AMOAND -> rs2_val & loaded
+ case AMOOR -> rs2_val | loaded
+
+ case AMOMIN -> (bit[64]) (min(signed(rs2_val), signed(loaded)))
+ case AMOMAX -> (bit[64]) (max(signed(rs2_val), signed(loaded)))
+ case AMOMINU -> (bit[64]) (min(unsigned(rs2_val), unsigned(loaded)))
+ case AMOMAXU -> (bit[64]) (max(unsigned(rs2_val), unsigned(loaded)))
+ };
+
+ switch (width) {
+ case WORD -> mem_write_value(addr, 4, result[31..0], aq & rl, rl, true)
+ case DOUBLE -> mem_write_value(addr, 8, result, aq & rl, rl, true)
+ };
+}
+
+(********************************************************************)
function clause decode _ = None
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:38:38 +0000