diff options
Diffstat (limited to 'risc-v')
25 files changed, 1336 insertions, 404 deletions
diff --git a/risc-v/Makefile b/risc-v/Makefile index 856a48eb..8449c7c4 100644 --- a/risc-v/Makefile +++ b/risc-v/Makefile @@ -1,13 +1,14 @@ SAIL:=../src/sail.native -SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail +SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail all: lem_ast shallow lem_ast: $(SOURCES) $(SAIL) - $(SAIL) -lem_ast $(SOURCES) + $(SAIL) -lem_ast $(SOURCES) -o riscv shallow: $(SOURCES) $(SAIL) - $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) + $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) -o riscv clean: - rm -f riscv.lem riscv_embed*.lem + rm -f riscv.lem riscv_embed*.lem riscv_toFromInterp.lem + rm -f riscv_type*.lem diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen index 8983b5ae..b1968173 100644 --- a/risc-v/hgen/ast.hgen +++ b/risc-v/hgen/ast.hgen @@ -5,9 +5,13 @@ | `RISCVIType of bit12 * reg * reg * riscvIop | `RISCVShiftIop of bit6 * reg * reg * riscvSop | `RISCVRType of reg * reg * reg * riscvRop -| `RISCVLoad of bit12 * reg * reg * bool * wordWidth -| `RISCVStore of bit12 * reg * reg * wordWidth +| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool +| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool | `RISCVADDIW of bit12 * reg * reg | `RISCVSHIFTW of bit5 * reg * reg * riscvSop | `RISCVRTYPEW of reg * reg * reg * riscvRopw | `RISCVFENCE of bit4 * bit4 +| `RISCVFENCEI +| `RISCVLoadRes of bool * bool * reg * wordWidth * reg +| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg +| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen index 03318805..4c51e114 100644 --- a/risc-v/hgen/fold.hgen +++ b/risc-v/hgen/fold.hgen @@ -1,13 +1,16 @@ -| `RISCVThreadStart -> (y_reg, y_sreg) -| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) -| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) -| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) -| `RISCVLoad (_, r0, r1, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVStore (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVThreadStart -> (y_reg, y_sreg) +| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVLoad (_, r0, r1, _, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVStore (_, r0, r1, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVLoadRes (_, _, rs1, _, rd) -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg)) +| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) +| `RISCVAMO (_, _, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index 50026612..07c1d082 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -3,10 +3,10 @@ translate_imm20 "imm" imm, translate_reg "rd" rd, translate_uop op) -| `RISCVJAL(imm, rd) -> JAL0( +| `RISCVJAL(imm, rd) -> RISCV_JAL( translate_imm21 "imm" imm, translate_reg "rd" rd) -| `RISCVJALR(imm, rs, rd) -> JALR0( +| `RISCVJALR(imm, rs, rd) -> RISCV_JALR( translate_imm12 "imm" imm, translate_reg "rs" rd, translate_reg "rd" rd) @@ -30,17 +30,21 @@ translate_reg "rs1" rs1, translate_reg "rd" rd, translate_rop op) -| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD( +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD( translate_imm12 "imm" imm, translate_reg "rs" rs, translate_reg "rd" rd, translate_bool "unsigned" unsigned, - translate_wordWidth width) -| `RISCVStore(imm, rs, rd, width) -> STORE ( + translate_wordWidth width, + translate_bool "aq" aq, + translate_bool "rl" rl) +| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE ( translate_imm12 "imm" imm, translate_reg "rs" rs, translate_reg "rd" rd, - translate_wordWidth width) + translate_wordWidth width, + translate_bool "aq" aq, + translate_bool "rl" rl) | `RISCVADDIW(imm, rs, rd) -> ADDIW( translate_imm12 "imm" imm, translate_reg "rs" rs, @@ -56,5 +60,27 @@ translate_reg "rd" rd, translate_ropw op) | `RISCVFENCE(pred, succ) -> FENCE( - translate_imm4 "pred" pred, - translate_imm4 "succ" succ) + translate_imm4 "pred" pred, + translate_imm4 "succ" succ) +| `RISCVFENCEI -> FENCEI +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES( + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON( + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) +| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO( + translate_amoop op, + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen index 4d8bd87a..e6edd24d 100644 --- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -4,48 +4,59 @@ let translate_reg name value = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value)) let translate_uop op = match op with - | RISCVLUI -> LUI0 - | RISCVAUIPC -> AUIPC + | RISCVLUI -> RISCV_LUI + | RISCVAUIPC -> RISCV_AUIPC let translate_bop op = match op with - | RISCVBEQ -> BEQ0 - | RISCVBNE -> BNE - | RISCVBLT -> BLT - | RISCVBGE -> BGE - | RISCVBLTU -> BLTU - | RISCVBGEU -> BGEU + | RISCVBEQ -> RISCV_BEQ + | RISCVBNE -> RISCV_BNE + | RISCVBLT -> RISCV_BLT + | RISCVBGE -> RISCV_BGE + | RISCVBLTU -> RISCV_BLTU + | RISCVBGEU -> RISCV_BGEU let translate_iop op = match op with - | RISCVADDI -> ADDI0 - | RISCVSLTI -> SLTI0 - | RISCVSLTIU -> SLTIU0 - | RISCVXORI -> XORI0 - | RISCVORI -> ORI0 - | RISCVANDI -> ANDI0 + | RISCVADDI -> RISCV_ADDI + | RISCVSLTI -> RISCV_SLTI + | RISCVSLTIU -> RISCV_SLTIU + | RISCVXORI -> RISCV_XORI + | RISCVORI -> RISCV_ORI + | RISCVANDI -> RISCV_ANDI let translate_sop op = match op with - | RISCVSLLI -> SLLI - | RISCVSRLI -> SRLI - | RISCVSRAI -> SRAI + | RISCVSLLI -> RISCV_SLLI + | RISCVSRLI -> RISCV_SRLI + | RISCVSRAI -> RISCV_SRAI let translate_rop op = match op with - | RISCVADD -> ADD0 - | RISCVSUB -> SUB0 - | RISCVSLL -> SLL0 - | RISCVSLT -> SLT0 - | RISCVSLTU -> SLTU0 - | RISCVXOR -> XOR0 - | RISCVSRL -> SRL0 - | RISCVSRA -> SRA0 - | RISCVOR -> OR0 - | RISCVAND -> AND0 + | RISCVADD -> RISCV_ADD + | RISCVSUB -> RISCV_SUB + | RISCVSLL -> RISCV_SLL + | RISCVSLT -> RISCV_SLT + | RISCVSLTU -> RISCV_SLTU + | RISCVXOR -> RISCV_XOR + | RISCVSRL -> RISCV_SRL + | RISCVSRA -> RISCV_SRA + | RISCVOR -> RISCV_OR + | RISCVAND -> RISCV_AND let translate_ropw op = match op with - | RISCVADDW -> ADDW - | RISCVSUBW -> SUBW - | RISCVSLLW -> SLLW - | RISCVSRLW -> SRLW - | RISCVSRAW -> SRAW + | RISCVADDW -> RISCV_ADDW + | RISCVSUBW -> RISCV_SUBW + | RISCVSLLW -> RISCV_SLLW + | RISCVSRLW -> RISCV_SRLW + | RISCVSRAW -> RISCV_SRAW + +let translate_amoop op = match op with + | RISCVAMOSWAP -> AMOSWAP + | RISCVAMOADD -> AMOADD + | RISCVAMOXOR -> AMOXOR + | RISCVAMOAND -> AMOAND + | RISCVAMOOR -> AMOOR + | RISCVAMOMIN -> AMOMIN + | RISCVAMOMAX -> AMOMAX + | RISCVAMOMINU -> AMOMINU + | RISCVAMOMAXU -> AMOMAXU let translate_wordWidth op = match op with | RISCVBYTE -> BYTE diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index 5f2c8326..e42b8a62 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -33,18 +33,44 @@ "or", RTYPE{op=RISCVOR}; "and", RTYPE{op=RISCVAND}; -"lb", LOAD{unsigned=false; width=RISCVBYTE}; -"lbu", LOAD{unsigned=true; width=RISCVBYTE}; -"lh", LOAD{unsigned=false; width=RISCVHALF}; -"lhu", LOAD{unsigned=true; width=RISCVHALF}; -"lw", LOAD{unsigned=false; width=RISCVWORD}; -"lwu", LOAD{unsigned=true; width=RISCVWORD}; -"ld", LOAD{unsigned=false; width=RISCVDOUBLE}; - -"sb", STORE{width=RISCVBYTE}; -"sh", STORE{width=RISCVHALF}; -"sw", STORE{width=RISCVWORD}; -"sd", STORE{width=RISCVDOUBLE}; +"lb", LOAD{unsigned=false; width=RISCVBYTE; aq=false; rl=false}; +"lbu", LOAD{unsigned=true; width=RISCVBYTE; aq=false; rl=false}; +"lh", LOAD{unsigned=false; width=RISCVHALF; aq=false; rl=false}; +"lhu", LOAD{unsigned=true; width=RISCVHALF; aq=false; rl=false}; +"lw", LOAD{unsigned=false; width=RISCVWORD; aq=false; rl=false}; +"lwu", LOAD{unsigned=true; width=RISCVWORD; aq=false; rl=false}; +"ld", LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false}; + +"lb.aq", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=false}; +"lbu.aq", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=false}; +"lh.aq", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=false}; +"lhu.aq", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=false}; +"lw.aq", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=false}; +"lwu.aq", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=false}; +"ld.aq", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false}; + +"lb.aq.rl", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=true}; +"lbu.aq.rl", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=true}; +"lh.aq.rl", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=true}; +"lhu.aq.rl", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=true}; +"lw.aq.rl", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=true}; +"lwu.aq.rl", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=true}; +"ld.aq.rl", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true}; + +"sb", STORE{width=RISCVBYTE; aq=false; rl=false}; +"sh", STORE{width=RISCVHALF; aq=false; rl=false}; +"sw", STORE{width=RISCVWORD; aq=false; rl=false}; +"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false}; + +"sb.rl", STORE{width=RISCVBYTE; aq=false; rl=true}; +"sh.rl", STORE{width=RISCVHALF; aq=false; rl=true}; +"sw.rl", STORE{width=RISCVWORD; aq=false; rl=true}; +"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true}; + +"sb.aq.rl", STORE{width=RISCVBYTE; aq=true; rl=true}; +"sh.aq.rl", STORE{width=RISCVHALF; aq=true; rl=true}; +"sw.aq.rl", STORE{width=RISCVWORD; aq=true; rl=true}; +"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true}; "addiw", ADDIW (); @@ -62,3 +88,103 @@ "r", FENCEOPTION Fence_R; "w", FENCEOPTION Fence_W; "rw", FENCEOPTION Fence_RW; + +"fence.i", FENCEI (); + +"lr.w", LOADRES {width=RISCVWORD; aq=false; rl=false}; +"lr.w.aq", LOADRES {width=RISCVWORD; aq=true; rl=false}; +"lr.w.aq.rl", LOADRES {width=RISCVWORD; aq=true; rl=true}; +"lr.d", LOADRES {width=RISCVDOUBLE; aq=false; rl=false}; +"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true; rl=false}; +"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true; rl=true}; + +"sc.w", STORECON {width=RISCVWORD; aq=false; rl=false}; +"sc.w.rl", STORECON {width=RISCVWORD; aq=false; rl=true}; +"sc.w.aq.rl", STORECON {width=RISCVWORD; aq=true; rl=true}; +"sc.d", STORECON {width=RISCVDOUBLE; aq=false; rl=false}; +"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true}; +"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true; rl=true}; + +"amoswap.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP}; +"amoadd.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD}; +"amoand.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOAND}; +"amoor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOOR}; +"amoxor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOXOR}; +"amomax.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAX}; +"amomin.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMIN}; +"amomaxu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAXU}; +"amominu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMINU}; + +"amoswap.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOSWAP}; +"amoadd.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOADD}; +"amoand.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOAND}; +"amoor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOOR}; +"amoxor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOXOR}; +"amomax.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAX}; +"amomin.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMIN}; +"amomaxu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAXU}; +"amominu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMINU}; + +"amoswap.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOSWAP}; +"amoadd.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOADD}; +"amoand.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOAND}; +"amoor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOOR}; +"amoxor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOXOR}; +"amomax.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAX}; +"amomin.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMIN}; +"amomaxu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAXU}; +"amominu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMINU}; + +"amoswap.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOSWAP}; +"amoadd.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOADD}; +"amoand.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOAND}; +"amoor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOOR}; +"amoxor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOXOR}; +"amomax.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAX}; +"amomin.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMIN}; +"amomaxu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAXU}; +"amominu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMINU}; + +"amoswap.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOSWAP}; +"amoadd.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOADD}; +"amoand.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOAND}; +"amoor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOOR}; +"amoxor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOXOR}; +"amomax.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAX}; +"amomin.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMIN}; +"amomaxu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAXU}; +"amominu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMINU}; + +"amoswap.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOSWAP}; +"amoadd.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOADD}; +"amoand.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOAND}; +"amoor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOOR}; +"amoxor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOXOR}; +"amomax.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAX}; +"amomin.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMIN}; +"amomaxu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAXU}; +"amominu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMINU}; + +"amoswap.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOSWAP}; +"amoadd.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOADD}; +"amoand.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOAND}; +"amoor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOOR}; +"amoxor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOXOR}; +"amomax.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAX}; +"amomin.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMIN}; +"amomaxu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAXU}; +"amominu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMINU}; + +"amoswap.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOSWAP}; +"amoadd.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOADD}; +"amoand.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOAND}; +"amoor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOOR}; +"amoxor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOXOR}; +"amomax.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAX}; +"amomin.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMIN}; +"amomaxu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAXU}; +"amominu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMINU}; + +(** pseudo instructions *********************************************) + +"li", LI () diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen index ff14c428..bab5ced8 100644 --- a/risc-v/hgen/map.hgen +++ b/risc-v/hgen/map.hgen @@ -1,12 +1,15 @@ -| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) -| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) -| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) -| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) -| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y) -| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y) -| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y) -| `RISCVLoad (x, r0, r1, y, z) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z) -| `RISCVStore (x, r0, r1, y) -> `RISCVStore (x, map_reg r0, map_reg r1, y) -| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1) -| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y) -| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) +| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) +| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) +| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) +| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) +| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y) +| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y) +| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y) +| `RISCVLoad (x, r0, r1, y, z, a, b) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b) +| `RISCVStore (x, r0, r1, y, z, a) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a) +| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1) +| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y) +| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) +| `RISCVLoadRes (aq, rl, rs1, w, rd) -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd) +| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) +| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd) -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index 37fd8d8d..210e38fb 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -1,36 +1,74 @@ | UTYPE reg COMMA NUM - { `RISCVUTYPE($4, $2, $1.op) } + { (* it's not clear if NUM here should be before or after filling the + lowest 12 bits with zeros, or if it should be signed or unsigned; + currently assuming: NUM does not include the 12 zeros, and is unsigned *) + if not (iskbituimm 20 $4) then failwith "immediate is not 20bit" + else `RISCVUTYPE ($4, $2, $1.op) } | JAL reg COMMA NUM - { `RISCVJAL($4, $2) } + { if not ($4 mod 2 = 0) then failwith "odd offset" + else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit" + else `RISCVJAL ($4, $2) } | JALR reg COMMA reg COMMA NUM - { `RISCVJALR($6, $4, $2) } + { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit" + else `RISCVJALR ($6, $4, $2) } | BTYPE reg COMMA reg COMMA NUM - { `RISCVBType($6, $4, $2, $1.op) } + { if not ($6 mod 2 = 0) then failwith "odd offset" + else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit" + else `RISCVBType ($6, $4, $2, $1.op) } | ITYPE reg COMMA reg COMMA NUM - { `RISCVIType($6, $4, $2, $1.op) } + { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" + else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit" + else `RISCVIType ($6, $4, $2, $1.op) } +| ADDIW reg COMMA reg COMMA NUM + { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" + else `RISCVADDIW ($6, $4, $2) } | SHIFTIOP reg COMMA reg COMMA NUM - { `RISCVShiftIop($6, $4, $2, $1.op) } + { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit" + else `RISCVShiftIop ($6, $4, $2, $1.op) } +| SHIFTW reg COMMA reg COMMA NUM + { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit" + else `RISCVSHIFTW ($6, $4, $2, $1.op) } | RTYPE reg COMMA reg COMMA reg { `RISCVRType ($6, $4, $2, $1.op) } | LOAD reg COMMA NUM LPAR reg RPAR - { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) } + { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" + else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) } | STORE reg COMMA NUM LPAR reg RPAR - { `RISCVStore($4, $2, $6, $1.width) } -| ADDIW reg COMMA reg COMMA NUM - { `RISCVADDIW ($6, $4, $2) } -| SHIFTW reg COMMA reg COMMA NUM - { `RISCVSHIFTW ($6, $4, $2, $1.op) } + { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" + else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) } | RTYPEW reg COMMA reg COMMA reg { `RISCVRTYPEW ($6, $4, $2, $1.op) } | FENCE FENCEOPTION COMMA FENCEOPTION { match ($2, $4) with | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011) | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011) + | (Fence_R, Fence_R) -> `RISCVFENCE (0b0010, 0b0010) | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001) + | (Fence_W, Fence_W) -> `RISCVFENCE (0b0001, 0b0001) | (Fence_RW, Fence_R) -> failwith "'fence rw,r' is not supported" - | (Fence_R, Fence_R) -> failwith "'fence r,r' is not supported" | (Fence_R, Fence_W) -> failwith "'fence r,w' is not supported" | (Fence_W, Fence_RW) -> failwith "'fence w,rw' is not supported" | (Fence_W, Fence_R) -> failwith "'fence w,r' is not supported" - | (Fence_W, Fence_W) -> failwith "'fence w,w' is not supported" } +| FENCEI + { `RISCVFENCEI } +| LOADRES reg COMMA LPAR reg RPAR + { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) } +| LOADRES reg COMMA NUM LPAR reg RPAR + { if $4 <> 0 then failwith "'lr' offset must be 0" else + `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) } +| STORECON reg COMMA reg COMMA LPAR reg RPAR + { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) } +| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR + { if $6 <> 0 then failwith "'sc' offset must be 0" else + `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) } +| AMO reg COMMA reg COMMA LPAR reg RPAR + { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) } +| AMO reg COMMA reg COMMA NUM LPAR reg RPAR + { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else + `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) } + +/* pseudo-ops */ +| LI reg COMMA NUM + { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)" + else `RISCVIType ($4, IReg R0, $2, RISCVORI) } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index 1da3ef11..fc1c0000 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -7,9 +7,24 @@ | `RISCVIType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm | `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) -| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs) -| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1) + +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs) + +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (pp_reg rs2) imm (pp_reg rs1) + | `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm | `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) | `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ) +| `RISCVFENCEI -> sprintf "fence.i" + +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1) + +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) + +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) diff --git a/risc-v/hgen/pretty_xml.hgen b/risc-v/hgen/pretty_xml.hgen new file mode 100644 index 00000000..b0306161 --- /dev/null +++ b/risc-v/hgen/pretty_xml.hgen @@ -0,0 +1,137 @@ +| `RISCVThreadStart -> ("op_thread_start", []) + +| `RISCVStopFetching -> ("op_stop_fetching", []) + +| `RISCVUTYPE(imm, rd, op) -> + ("op_U_type", + [ ("op", pp_riscv_uop op); + ("uimm", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVJAL(imm, rd) -> + ("op_jal", + [ ("offset", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVJALR(imm, rs1, rd) -> + ("op_jalr", + [ ("offset", sprintf "%d" imm); + ("base", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVBType(imm, rs2, rs1, op) -> + ("op_branch", + [ ("op", pp_riscv_bop op); + ("offset", sprintf "%d" imm); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ]) + +| `RISCVIType(imm, rs1, rd, op) -> + ("op_I_type", + [ ("op", pp_riscv_iop op); + ("iimm", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVShiftIop(imm, rs1, rd, op) -> + ("op_IS_type", + [ ("op", pp_riscv_sop op); + ("shamt", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVSHIFTW(imm, rs1, rd, op) -> + ("op_ISW_type", + [ ("op", pp_riscv_sop op); + ("shamt", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVRType (rs2, rs1, rd, op) -> + ("op_R_type", + [ ("op", pp_riscv_rop op); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) -> + ("op_load", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("unsigned", if unsigned then "true" else "false"); + ("base", pp_reg rs1); + ("offset", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + ("op_store", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("src", pp_reg rs2); + ("base", pp_reg rs1); + ("offset", sprintf "%d" imm); + ]) + +| `RISCVADDIW(imm, rs1, rd) -> + ("op_addiw", + [ ("iimm", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVRTYPEW(rs2, rs1, rd, op) -> + ("op_RW_type", + [ ("op", pp_riscv_ropw op); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVFENCE(pred, succ) -> + ("op_fence", + [ ("pred", pp_riscv_fence_option pred); + ("succ", pp_riscv_fence_option succ); + ]) + +| `RISCVFENCEI -> ("op_fence_i", []) + +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + ("op_lr", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("addr", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + ("op_sc", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("addr", pp_reg rs1); + ("src", pp_reg rs2); + ("dest", pp_reg rd); + ]) + +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + ("op_amo", + [ ("op", pp_riscv_amo_op_part op); + ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("src", pp_reg rs2); + ("addr", pp_reg rs1); + ("dest", pp_reg rd); + ]) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index dca5bea1..2f9a80f1 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -6,9 +6,18 @@ | ("ITYPE", [imm; rs1; rd; op]) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) | ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | ("RTYPE", [rs2; rs1; rd; op]) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) -| ("LOAD", [imm; rs; rd; unsigned; width]) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width) -| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width) +| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl]) + -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| ("STORE", [imm; rs; rd; width; aq; rl]) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) | ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) | ("FENCE", [pred; succ]) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) +| ("FENCEI", []) -> `RISCVFENCEI +| ("LOADRES", [aq; rl; rs1; width; rd]) + -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| ("STORECON", [aq; rl; rs2; rs1; width; rd]) + -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| ("AMO", [op; aq; rl; rs2; rs1; width; rd]) + -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 6158ebd7..3025992e 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -1,14 +1,23 @@ | EBREAK -> `RISCVStopFetching | UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) -| JAL0( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) -| JALR0( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| RISCV_JAL( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) +| RISCV_JALR( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) | ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) | SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | RTYPE( rs2, rs1, rd, op) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) -| LOAD( imm, rs, rd, unsigned, width) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width) -| STORE( imm, rs, rd, width) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width) +| LOAD( imm, rs, rd, unsigned, width, aq, rl) + -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| STORE( imm, rs, rd, width, aq, rl) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) | ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) | FENCE( pred, succ) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) +| FENCEI -> `RISCVFENCEI +| LOADRES( aq, rl, rs1, width, rd) + -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| STORECON( aq, rl, rs2, rs1, width, rd) + -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| AMO( op, aq, rl, rs2, rs1, width, rd) + -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen index a891d7d0..6b3b7f51 100644 --- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -10,48 +10,59 @@ let translate_out_signed_int inst bits = let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) let translate_out_uop op = match op with - | LUI0 -> RISCVLUI - | AUIPC -> RISCVAUIPC + | RISCV_LUI -> RISCVLUI + | RISCV_AUIPC -> RISCVAUIPC let translate_out_bop op = match op with - | BEQ0 -> RISCVBEQ - | BNE -> RISCVBNE - | BLT -> RISCVBLT - | BGE -> RISCVBGE - | BLTU -> RISCVBLTU - | BGEU -> RISCVBGEU + | RISCV_BEQ -> RISCVBEQ + | RISCV_BNE -> RISCVBNE + | RISCV_BLT -> RISCVBLT + | RISCV_BGE -> RISCVBGE + | RISCV_BLTU -> RISCVBLTU + | RISCV_BGEU -> RISCVBGEU let translate_out_iop op = match op with - | ADDI0 -> RISCVADDI - | SLTI0 -> RISCVSLTI - | SLTIU0 -> RISCVSLTIU - | XORI0 -> RISCVXORI - | ORI0 -> RISCVORI - | ANDI0 -> RISCVANDI + | RISCV_ADDI -> RISCVADDI + | RISCV_SLTI -> RISCVSLTI + | RISCV_SLTIU -> RISCVSLTIU + | RISCV_XORI -> RISCVXORI + | RISCV_ORI -> RISCVORI + | RISCV_ANDI -> RISCVANDI let translate_out_sop op = match op with - | SLLI -> RISCVSLLI - | SRLI -> RISCVSRLI - | SRAI -> RISCVSRAI + | RISCV_SLLI -> RISCVSLLI + | RISCV_SRLI -> RISCVSRLI + | RISCV_SRAI -> RISCVSRAI let translate_out_rop op = match op with - | ADD0 -> RISCVADD - | SUB0 -> RISCVSUB - | SLL0 -> RISCVSLL - | SLT0 -> RISCVSLT - | SLTU0 -> RISCVSLTU - | XOR0 -> RISCVXOR - | SRL0 -> RISCVSRL - | SRA0 -> RISCVSRA - | OR0 -> RISCVOR - | AND0 -> RISCVAND + | RISCV_ADD -> RISCVADD + | RISCV_SUB -> RISCVSUB + | RISCV_SLL -> RISCVSLL + | RISCV_SLT -> RISCVSLT + | RISCV_SLTU -> RISCVSLTU + | RISCV_XOR -> RISCVXOR + | RISCV_SRL -> RISCVSRL + | RISCV_SRA -> RISCVSRA + | RISCV_OR -> RISCVOR + | RISCV_AND -> RISCVAND let translate_out_ropw op = match op with - | ADDW -> RISCVADDW - | SUBW -> RISCVSUBW - | SLLW -> RISCVSLLW - | SRLW -> RISCVSRLW - | SRAW -> RISCVSRAW + | RISCV_ADDW -> RISCVADDW + | RISCV_SUBW -> RISCVSUBW + | RISCV_SLLW -> RISCVSLLW + | RISCV_SRLW -> RISCVSRLW + | RISCV_SRAW -> RISCVSRAW + +let translate_out_amoop op = match op with + | AMOSWAP -> RISCVAMOSWAP + | AMOADD -> RISCVAMOADD + | AMOXOR -> RISCVAMOXOR + | AMOAND -> RISCVAMOAND + | AMOOR -> RISCVAMOOR + | AMOMIN -> RISCVAMOMIN + | AMOMAX -> RISCVAMOMAX + | AMOMINU -> RISCVAMOMINU + | AMOMAXU -> RISCVAMOMAXU let translate_out_wordWidth op = match op with | BYTE -> RISCVBYTE diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen index 2980b985..f29e318d 100644 --- a/risc-v/hgen/token_types.hgen +++ b/risc-v/hgen/token_types.hgen @@ -5,11 +5,19 @@ type token_BType = {op : riscvBop } type token_IType = {op : riscvIop } type token_ShiftIop = {op : riscvSop } type token_RTYPE = {op : riscvRop } -type token_Load = {unsigned: bool; width : wordWidth } -type token_Store = {width : wordWidth } +type token_Load = {unsigned: bool; width : wordWidth; aq: bool; rl: bool } +type token_Store = {width : wordWidth; aq: bool; rl: bool } type token_ADDIW = unit type token_SHIFTW = {op : riscvSop } type token_RTYPEW = {op : riscvRopw } type token_FENCE = unit +type token_FENCEI = unit +type token_LoadRes = {width : wordWidth; aq: bool; rl: bool } +type token_StoreCon = {width : wordWidth; aq: bool; rl: bool } +type token_AMO = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop } type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW + +(* pseudo-ops *) + +type token_LI = unit diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen index f952cf77..f812adbd 100644 --- a/risc-v/hgen/tokens.hgen +++ b/risc-v/hgen/tokens.hgen @@ -12,3 +12,8 @@ %token <RISCVHGenBase.token_RTYPEW> RTYPEW %token <RISCVHGenBase.token_FENCE> FENCE %token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION +%token <RISCVHGenBase.token_FENCEI> FENCEI +%token <RISCVHGenBase.token_LoadRes> LOADRES +%token <RISCVHGenBase.token_StoreCon> STORECON +%token <RISCVHGenBase.token_AMO> AMO +%token <RISCVHGenBase.token_LI> LI diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index df22d9dc..8b7cbe11 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -58,7 +58,7 @@ translate_rop "op" op; ], []) -| `RISCVLoad(imm, rs, rd, unsigned, width) -> +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> ("LOAD", [ translate_imm12 "imm" imm; @@ -66,15 +66,19 @@ translate_reg "rd" rd; translate_bool "unsigned" unsigned; translate_width "width" width; + translate_bool "aq" aq; + translate_bool "rl" rl; ], []) -| `RISCVStore(imm, rs2, rs1, width) -> +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> ("STORE", [ translate_imm12 "imm" imm; translate_reg "rs2" rs2; translate_reg "rs1" rs1; translate_width "width" width; + translate_bool "aq" aq; + translate_bool "rl" rl; ], []) | `RISCVADDIW(imm, rs, rd) -> @@ -110,3 +114,40 @@ translate_imm4 "succ" succ; ], []) +| `RISCVFENCEI -> + ("FENCEI", + [], + []) +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + ("LOADRES", + [ + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + ("STORECON", + [ + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + ("AMO", + [ + translate_amoop "op" op; + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen index 87fc9b95..a0b75606 100644 --- a/risc-v/hgen/types.hgen +++ b/risc-v/hgen/types.hgen @@ -99,22 +99,71 @@ type wordWidth = | RISCVWORD | RISCVDOUBLE -let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with - | (false, RISCVBYTE) -> "lb" - | (true, RISCVBYTE) -> "lbu" - | (false, RISCVHALF) -> "lh" - | (true, RISCVHALF) -> "lhu" - | (false, RISCVWORD) -> "lw" - | (true, RISCVWORD) -> "lwu" - | (_, RISCVDOUBLE) -> "ld" - | _ -> failwith "unexpected load op" - -let pp_riscv_store_op width = match width with -| RISCVBYTE -> "sb" -| RISCVHALF -> "sh" -| RISCVWORD -> "sw" -| RISCVDOUBLE -> "sd" -| _ -> failwith "unexpected store op" +let pp_word_width width : string = + begin match width with + | RISCVBYTE -> "b" + | RISCVHALF -> "h" + | RISCVWORD -> "w" + | RISCVDOUBLE -> "d" + end + +let pp_riscv_load_op (unsigned, width, aq, rl) = + "l" ^ + (pp_word_width width) ^ + (if unsigned then "u" else "") ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_store_op (width, aq, rl) = + "s" ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_load_reserved_op (aq, rl, width) = + "lr." ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_store_conditional_op (aq, rl, width) = + "sc." ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +type riscvAmoop = + | RISCVAMOSWAP + | RISCVAMOADD + | RISCVAMOXOR + | RISCVAMOAND + | RISCVAMOOR + | RISCVAMOMIN + | RISCVAMOMAX + | RISCVAMOMINU + | RISCVAMOMAXU + +let pp_riscv_amo_op_part = function + | RISCVAMOSWAP -> "swap" + | RISCVAMOADD -> "add" + | RISCVAMOXOR -> "xor" + | RISCVAMOAND -> "and" + | RISCVAMOOR -> "or" + | RISCVAMOMIN -> "min" + | RISCVAMOMAX -> "max" + | RISCVAMOMINU -> "minu" + | RISCVAMOMAXU -> "maxu" + +let pp_riscv_amo_op (op, aq, rl, width) = + "amo" ^ + pp_riscv_amo_op_part op ^ + begin match width with + | RISCVWORD -> ".w" + | RISCVDOUBLE -> ".d" + | _ -> assert false + end ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") let pp_riscv_fence_option = function | 0b0011 -> "rw" diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen index e22110d0..66a2020c 100644 --- a/risc-v/hgen/types_sail_trans_out.hgen +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -84,3 +84,15 @@ let translate_out_ropw op = match translate_out_enum op with | 3 -> RISCVSRLW | 4 -> RISCVSRAW | _ -> failwith "Unknown ropw in sail translate out" + +let translate_out_amoop op = match translate_out_enum op with +| 0 -> RISCVAMOSWAP +| 1 -> RISCVAMOADD +| 2 -> RISCVAMOXOR +| 3 -> RISCVAMOAND +| 4 -> RISCVAMOOR +| 5 -> RISCVAMOMIN +| 6 -> RISCVAMOMAX +| 7 -> RISCVAMOMINU +| 8 -> RISCVAMOMAXU +| _ -> failwith "Unknown amoop in sail translate out" diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen index 1bf174fa..238c7e5b 100644 --- a/risc-v/hgen/types_trans_sail.hgen +++ b/risc-v/hgen/types_trans_sail.hgen @@ -11,29 +11,47 @@ let translate_enum enum_values name value = (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index)) let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC] + let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *) + let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *) + let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *) + let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *) + let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *) + +let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU] + let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] + let translate_reg name value = (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value))) + let translate_imm21 name value = (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value)) + let translate_imm20 name value = (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value)) + let translate_imm16 name value = (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value)) + let translate_imm13 name value = (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value)) + let translate_imm12 name value = (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value)) + let translate_imm6 name value = (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value)) + let translate_imm5 name value = (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value)) + let translate_imm4 name value = (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value)) + let translate_bool name value = (name, Bit, [if value then Bitc_one else Bitc_zero]) 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 diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index aa5d8fb8..30043779 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -32,29 +32,52 @@ let memory_parameter_transformer_option_address _mode v = let read_memory_functions : memory_reads = - [ ("MEMr", (MR Read_plain memory_parameter_transformer)); - ("MEMr_reserve", (MR Read_reserve memory_parameter_transformer)); + [ ("MEMr", (MR Read_plain memory_parameter_transformer)); + ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); + ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); + ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer)); + ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); + ("MEMr_reserved_strong_acquire", + (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); ] let memory_writes : memory_writes = [] let memory_eas : memory_write_eas = - [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); - ("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer)); + [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); + ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); + ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); + ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); + ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); + ("MEMea_conditional_strong_release", + (MEA Write_RISCV_conditional_strong_release + memory_parameter_transformer)); ] let memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_strong_release", + (MV memory_parameter_transformer_option_address Nothing)); + ] +let speculate_conditional_success : excl_res = + let f = fun (IState interp context) b -> + let bool_res = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in + IState (Interp.add_answer_to_stack interp bool_res) context + in + Just ("speculate_conditional_success", (ER (Just f))) + let barrier_functions = [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); ("MEM_fence_r_rw", Barrier_RISCV_r_rw); + ("MEM_fence_r_r", Barrier_RISCV_r_r); ("MEM_fence_rw_w", Barrier_RISCV_rw_w); + ("MEM_fence_w_w", Barrier_RISCV_w_w); + ("MEM_fence_i", Barrier_RISCV_i); ] diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index 1146d1cd..32110079 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -4,31 +4,66 @@ open import Sail_impl_base open import Sail_values open import Prompt -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size +let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size +let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size +let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire (addr,size) + = read_mem false Read_RISCV_reserved_strong_acquire addr size -val MEMea : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit +val MEMea : (vector bitU * integer) -> M unit +val MEMea_release : (vector bitU * integer) -> M unit +val MEMea_strong_release : (vector bitU * integer) -> M unit +val MEMea_conditional : (vector bitU * integer) -> M unit +val MEMea_conditional_release : (vector bitU * integer) -> M unit +val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size +let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release (addr,size) + = write_mem_ea Write_RISCV_conditional_strong_release addr size -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_strong_release (_,_,v) + = write_mem_val v >>= fun _ -> return () + +let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) val MEM_fence_rw_rw : unit -> M unit val MEM_fence_r_rw : unit -> M unit +val MEM_fence_r_r : unit -> M unit val MEM_fence_rw_w : unit -> M unit +val MEM_fence_w_w : unit -> M unit +val MEM_fence_i : unit -> M unit let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w +let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_i () = barrier Barrier_RISCV_i let duplicate (bit,len) = let bits = repeat [bit] len in diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem index f6709ff7..3c922268 100644 --- a/risc-v/riscv_extras_embed_sequential.lem +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -4,32 +4,66 @@ open import Sail_impl_base open import Sail_values open import State -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size +let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size +let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size +let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire (addr,size) + = read_mem false Read_RISCV_reserved_strong_acquire addr size -val MEMea : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit +val MEMea : (vector bitU * integer) -> M unit +val MEMea_release : (vector bitU * integer) -> M unit +val MEMea_strong_release : (vector bitU * integer) -> M unit +val MEMea_conditional : (vector bitU * integer) -> M unit +val MEMea_conditional_release : (vector bitU * integer) -> M unit +val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size +let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release (addr,size) + = write_mem_ea Write_RISCV_conditional_strong_release addr size +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_strong_release (_,_,v) + = write_mem_val v >>= fun _ -> return () -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) val MEM_fence_rw_rw : unit -> M unit val MEM_fence_r_rw : unit -> M unit +val MEM_fence_r_r : unit -> M unit val MEM_fence_rw_w : unit -> M unit +val MEM_fence_w_w : unit -> M unit +val MEM_fence_i : unit -> M unit let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w +let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_i () = barrier Barrier_RISCV_i let duplicate (bit,len) = let bits = repeat [bit] len in diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index 0c7a67d8..dee9cc8e 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -20,16 +20,16 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( case (UTYPE ( imm, rd, op)) -> { if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; } - case (JAL ( imm, rd)) -> { + case (RISCV_JAL ( imm, rd)) -> { if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in Nias := [|| NIAFP_concrete_address (PC + offset) ||] } - case (JALR ( imm, rs, rd)) -> { + case (RISCV_JALR ( imm, rs, rd)) -> { if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in - Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; (* XXX this should br rs + offset... *) + Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; } case (BTYPE ( imm, rs2, rs1, op)) -> { if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; @@ -51,17 +51,29 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; } - case (LOAD ( imm, rs, rd, unsign, width)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *) + case (LOAD ( imm, rs, rd, unsign, width, aq, rl)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *) if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; aR := iR; - ik := IK_mem_read (Read_plain); + ik := + switch (aq, rl) { + case (false, false) -> IK_mem_read (Read_plain) + case (true, false) -> IK_mem_read (Read_RISCV_acquire) + case (false, true) -> exit "not implemented" + case (true, true) -> IK_mem_read (Read_RISCV_strong_acquire) + }; } - case (STORE( imm, rs2, rs1, width)) -> { + case (STORE( imm, rs2, rs1, width, aq, rl)) -> { if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR; - ik := IK_mem_write (Write_plain); + ik := + switch (aq, rl) { + case (false, false) -> IK_mem_write (Write_plain) + case (true, false) -> exit "not implemented" + case (false, true) -> IK_mem_write (Write_RISCV_release) + case (true, true) -> IK_mem_write (Write_RISCV_strong_release) + }; } case (ADDIW ( imm, rs, rd)) -> { if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; @@ -77,7 +89,56 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; } case (FENCE(pred, succ)) -> { - ik := IK_barrier (Barrier_MIPS_SYNC); + ik := + switch(pred, succ) { + case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw) + case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw) + case (0b0010, 0b0010) -> IK_barrier (Barrier_RISCV_r_r) + case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w) + case (0b0001, 0b0001) -> IK_barrier (Barrier_RISCV_w_w) + case _ -> exit "not implemented" + }; + } + case (FENCEI) -> { + ik := IK_barrier (Barrier_RISCV_i); + } + case (LOADRES ( aq, rl, rs1, width, rd)) -> { + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + aR := iR; + ik := switch (aq, rl) { + case (false, false) -> IK_mem_read (Read_RISCV_reserved) + case (true, false) -> IK_mem_read (Read_RISCV_reserved_acquire) + case (false, true) -> exit "not implemented" + case (true, true) -> IK_mem_read (Read_RISCV_reserved_strong_acquire) + }; + } + case (STORECON( aq, rl, rs2, rs1, width, rd)) -> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + + ik := switch (aq, rl) { + case (false, false) -> IK_mem_write (Write_RISCV_conditional) + case (false, true) -> IK_mem_write (Write_RISCV_conditional_release) + case (true, _) -> exit "not implemented" + }; + } + case (AMO( op, aq, rl, rs2, rs1, width, rd)) -> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + + ik := switch (aq, rl) { + case (false, false) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional) + case (false, true) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release) + case (true, false) -> IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional) + case (true, true) -> IK_mem_rmw (Read_RISCV_reserved_strong_acquire, + Write_RISCV_conditional_strong_release) + }; } }; (iR,oR,aR,Nias,Dia,ik) diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail new file mode 100644 index 00000000..b584ae9b --- /dev/null +++ b/risc-v/riscv_types.sail @@ -0,0 +1,166 @@ +default Order dec + +function forall 'a. 'a effect { escape } not_implemented((string) message) = + exit message + +typedef regval = bit[64] +typedef regno = bit[5] + +(* register (regval) x0 is hard-wired zero *) +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 <1, 31, 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 unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) = + if (unsigned(addr) mod width != 0) then + exit "misaligned memory access" + +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire + +function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) = +{ + if (aq | res) then + check_alignment(addr, width); + + switch (aq, rl, res) { + case (false, false, false) -> MEMr(addr, width) + case (true, false, false) -> MEMr_acquire(addr, width) + case (false, false, true) -> MEMr_reserved(addr, width) + case (true, false, true) -> MEMr_reserved_acquire(addr, width) + case (false, true, false) -> not_implemented("load.rl is not implemented") + case (true, true, false) -> MEMr_strong_acquire(addr, width) + case (false, true, true) -> not_implemented("lr.rl is not implemented") + case (true, true, true) -> MEMr_reserved_strong_acquire(addr, width) + } +} + +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release + +function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) = +{ + if (rl | con) then + check_alignment(addr, width); + + switch (aq, rl, con) { + case (false, false, false) -> MEMea(addr, width) + case (false, true, false) -> MEMea_release(addr, width) + case (false, false, true) -> MEMea_conditional(addr, width) + case (false, true , true) -> MEMea_conditional_release(addr, width) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMea_strong_release(addr, width) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true , true) -> MEMea_conditional_strong_release(addr, width) + } +} + +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release + +function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) = +{ + if (rl | con) then + check_alignment(addr, width); + + switch (aq, rl, con) { + case (false, false, false) -> MEMval(addr, width, value) + case (false, true, false) -> MEMval_release(addr, width, value) + case (false, false, true) -> MEMval_conditional(addr, width, value) + case (false, true, true) -> MEMval_conditional_release(addr, width, value) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMval_strong_release(addr, width, value) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true, true) -> MEMval_conditional_strong_release(addr, width, value) + } +} + +val extern unit -> bool effect {exmem} speculate_conditional_success + +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_r_r +val extern unit -> unit effect { barr } MEM_fence_rw_w +val extern unit -> unit effect { barr } MEM_fence_w_w +val extern unit -> unit effect { barr } MEM_fence_i + +typedef uop = enumerate {RISCV_LUI; RISCV_AUIPC} (* upper immediate ops *) +typedef bop = enumerate {RISCV_BEQ; RISCV_BNE; RISCV_BLT; RISCV_BGE; RISCV_BLTU; RISCV_BGEU} (* branch ops *) +typedef iop = enumerate {RISCV_ADDI; RISCV_SLTI; RISCV_SLTIU; RISCV_XORI; RISCV_ORI; RISCV_ANDI} (* immediate ops *) +typedef sop = enumerate {RISCV_SLLI; RISCV_SRLI; RISCV_SRAI} (* shift ops *) +typedef rop = enumerate {RISCV_ADD; RISCV_SUB; RISCV_SLL; RISCV_SLT; RISCV_SLTU; RISCV_XOR; RISCV_SRL; RISCV_SRA; RISCV_OR; RISCV_AND} (* reg-reg ops *) +typedef ropw = enumerate {RISCV_ADDW; RISCV_SUBW; RISCV_SLLW; RISCV_SRLW; RISCV_SRAW} (* reg-reg 32-bit ops *) +typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR; + AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *) + +typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE} + +(********************************************************************) + +(* 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] |