diff options
Diffstat (limited to 'risc-v')
23 files changed, 1069 insertions, 17 deletions
diff --git a/risc-v/Makefile b/risc-v/Makefile new file mode 100644 index 00000000..2f6af138 --- /dev/null +++ b/risc-v/Makefile @@ -0,0 +1,13 @@ + +SAIL:=../src/sail.native + +all: lem_ast shallow + +lem_ast: riscv.sail $(SAIL) + $(SAIL) -lem_ast $< + +shallow: riscv.sail $(SAIL) + $(SAIL) -lem_lib Riscv_extras_embed -lem $< + +clean: + rm -f riscv.lem riscv_embed*.lem diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen new file mode 100644 index 00000000..ee7cb3e1 --- /dev/null +++ b/risc-v/hgen/ast.hgen @@ -0,0 +1,13 @@ +| `RISCVThreadStart +| `RISCVUTYPE of bit20 * reg * riscvUop +| `RISCVJAL of bit20 * reg +| `RISCVJALR of bit12 * reg * reg +| `RISCVBType of bit12 * reg * reg * riscvBop +| `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 +| `RISCVADDIW of bit12 * reg * reg +| `RISCVSHIFTW of bit5 * reg * reg * riscvSop +| `RISCVRTYPEW of reg * reg * reg * riscvRopw diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen new file mode 100644 index 00000000..03318805 --- /dev/null +++ b/risc-v/hgen/fold.hgen @@ -0,0 +1,13 @@ +| `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))) diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen new file mode 100644 index 00000000..e614b714 --- /dev/null +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -0,0 +1,122 @@ +(*| `MIPSThreadStart -> + SYSCALL_THREAD_START + +| `MIPSStopFetching -> + ImplementationDefinedStopFetching0 + +(* Note different argument order, which reflects difference + between instruction encoding and asm format *) +| `MIPSRType (op, rd, rs, rt) -> + (translate_rtype_op op) + ( + translate_reg "rs" rs, + translate_reg "rt" rt, + translate_reg "rd" rd + ) + + +(* Note different argument order similar to above *) +| `MIPSIType (op, rt, rs, imm) -> + (translate_itype_op op) + ( + translate_reg "rs" rs, + translate_reg "rt" rt, + translate_imm16 "imm" imm + ) + + +| `MIPSShiftI (op, rd, rt, sa) -> + (translate_shifti_op op) + ( + translate_reg "rt" rt, + translate_reg "rd" rd, + translate_imm5 "sa" sa + ) + + +| `MIPSShiftV (op, rd, rt, rs) -> + (translate_shiftv_op op) + ( + translate_reg "rs" rs, + translate_reg "rt" rt, + translate_reg "rd" rd + ) + + +| `MIPSMulDiv (op, rs, rt) -> + (translate_muldiv_op op) + ( + translate_reg "rs" rs, + translate_reg "rt" rt + ) + + +| `MIPSMFHiLo (op, rs) -> + (translate_mfhilo_op op) + ( + translate_reg "rs" rs + ) + +| `MIPSLUI (rt, imm) -> + LUI + ( + translate_reg "rt" rt, + translate_imm16 "imm" imm + ) + +| `MIPSLoad (width, signed, linked, base, rt, offset) -> + Load + ( + translate_wordsize "width" width, + translate_bool "signed" signed, + translate_bool "linked" linked, + translate_reg "base" base, + translate_reg "rt" rt, + translate_imm16 "offset" offset + ) + +| `MIPSStore (width, conditional, base, rt, offset) -> + Store + ( + translate_wordsize "width" width, + translate_bool "conditional" conditional, + translate_reg "base" base, + translate_reg "rt" rt, + translate_imm16 "offset" offset + ) + +| `MIPSLSLR (store, double, left, base, rt, offset) -> + (translate_lslr_op store double left) + ( + translate_reg "base" base, + translate_reg "rt" rt, + translate_imm16 "offset" offset + ) + +| `MIPSSYNC -> SYNC +| `MIPSBEQ (rs, rt, offset, ne, likely) -> + BEQ + (translate_reg "rs" rs, + translate_reg "rt" rt, + translate_imm16 "offset" offset, + translate_bool "ne" ne, + translate_bool "likely" likely + ) + +| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> + BCMPZ + (translate_reg "rs" rs, + translate_imm16 "offset" offset, + translate_cmp "cmp" cmp, + translate_bool "link" link, + translate_bool "likely" likely + ) +| `MIPSJ (offset) -> + J (translate_imm26 "offset" offset) +| `MIPSJAL (offset) -> + JAL (translate_imm26 "offset" offset) +| `MIPSJR(rd) -> + JR (translate_reg "rd" rd) +| `MIPSJALR(rd, rs) -> + JALR (translate_reg "rd" rd, translate_reg "rs" rs) +*)
\ No newline at end of file diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen new file mode 100644 index 00000000..1c925e2b --- /dev/null +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -0,0 +1,121 @@ +let is_inc = false +(* +let translate_rtype_op op = uppercase (pp_rtype_op op) + +let translate_rtype_op op x = match op with + | MIPSROpADD -> ADD x + | MIPSROpADDU -> ADDU x + | MIPSROpAND -> AND x + | MIPSROpDADD -> DADD x + | MIPSROpDADDU -> DADDU x + | MIPSROpDSUB -> DSUB x + | MIPSROpDSUBU -> DSUBU x + | MIPSROpMOVN -> MOVN x + | MIPSROpMOVZ -> MOVZ x + | MIPSROpMUL -> MUL x + | MIPSROpNOR -> NOR x + | MIPSROpOR -> OR x + | MIPSROpSLT -> SLT x + | MIPSROpSLTU -> SLTU x + | MIPSROpSUB -> SUB x + | MIPSROpSUBU -> SUBU x + | MIPSROpXOR -> XOR x + +let translate_itype_op op x = match op with + | MIPSIOpADDI -> ADDI x + | MIPSIOpADDIU -> ADDIU x + | MIPSIOpANDI -> ANDI x + | MIPSIOpDADDI -> DADDI x + | MIPSIOpDADDIU -> DADDIU x + | MIPSIOpORI -> ORI x + | MIPSIOpSLTI -> SLTI x + | MIPSIOpSLTIU -> SLTIU x + | MIPSIOpXORI -> XORI x + +let translate_shifti_op op x = match op with + | MIPSDSLL -> DSLL x + | MIPSDSLL32 -> DSLL32 x + | MIPSDSRA -> DSRA x + | MIPSDSRA32 -> DSRA32 x + | MIPSDSRL -> DSRL x + | MIPSDSRL32 -> DSRL32 x + | MIPSSLL -> SLL x + | MIPSSRA -> SRA x + | MIPSSRL -> SRL x + +let translate_shiftv_op op x = match op with + | MIPSDSLLV -> DSLLV x + | MIPSDSRAV -> DSRAV x + | MIPSDSRLV -> DSRLV x + | MIPSSLLV -> SLLV x + | MIPSSRAV -> SRAV x + | MIPSSRLV -> SRLV x + +let translate_muldiv_op op x = match op with + | MIPSDDIV -> DDIV x + | MIPSDDIVU -> DDIVU x + | MIPSDIV -> DIV x + | MIPSDIVU -> DIVU x + | MIPSDMULT -> DMULT x + | MIPSDMULTU -> DMULTU x + | MIPSMADD -> MADD x + | MIPSMADDU -> MADDU x + | MIPSMSUB -> MSUB x + | MIPSMSUBU -> MSUBU x + | MIPSMULT -> MULT x + | MIPSMULTU -> MULTU x + +let translate_mfhilo_op op x = match op with + | MIPSMFHI -> MFHI x + | MIPSMFLO -> MFLO x + | MIPSMTHI -> MTHI x + | MIPSMTLO -> MTLO x + +let translate_load_op width signed linked = uppercase (pp_load_op width signed linked) + +let translate_store_op width conditional = uppercase (pp_store_op width conditional) + +let translate_lslr_op store double left x = match (store,double,left) with + | (false, false, true ) -> LWL x + | (false, false, false) -> LWR x + | (false, true , true ) -> LDL x + | (false, true , false) -> LDR x + | (true , false, true ) -> SWL x + | (true , false, false) -> SWR x + | (true , true , true ) -> SDL x + | (true , true , false) -> SDR x + +let translate_beq_op ne likely = uppercase (pp_beq_op ne likely) + +let translate_bcmpz_op cmp link likely = uppercase (pp_bcmpz_op cmp link likely) + + +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_imm26 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value) +let translate_imm16 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,Nat_big_num.of_int value) +let translate_imm5 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value) +let translate_bool name = function + | true -> Sail_values.B1 + | false -> Sail_values.B0 + +let translate_wordsize _ = function + | MIPSByte -> Mips_embed_types.B2 + | MIPSHalf -> Mips_embed_types.H + | MIPSWord -> Mips_embed_types.W + | MIPSDouble -> Mips_embed_types.D + +let translate_cmp _ = function + | MIPS_EQ -> EQ' + | MIPS_NE -> NE + | MIPS_GE -> GE + | MIPS_GEU -> GEU + | MIPS_GT -> GT' + | MIPS_LE -> LE + | MIPS_LT -> LT' + | MIPS_LTU -> LTU +*) diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen new file mode 100644 index 00000000..a75eef9f --- /dev/null +++ b/risc-v/hgen/lexer.hgen @@ -0,0 +1,60 @@ +"lwu" , UTYPE { op=RSICVLUI }; +"auipc" , UTYPE { op=RSICVAUIPC }; + +"jal", JAL; +"jalr", JALR; + +"beq", BTYPE {op=RISCVBEQ}; +"bne", BTYPE {op=RISCVBNE}; +"blt", BTYPE {op=RISCVBLT}; +"bge", BTYPE {op=RISCVBGE}; +"bltu", BTYPE {op=RISCVBLTU}; +"bgeu", BTYPE {op=RISCVBGEU}; + +"addi", ITYPE {op=RISCVADDI}; +"stli", ITYPE {op=RISCVSTLI}; +"sltiu", ITYPE {op=RISCVSLTIU}; +"xori", ITYPE {op=RISCVXORI}; +"ori", ITYPE {op=RISCVORI}; +"andi", ITYPE {op=RISCVANDI}; + +"slli", SHIFTIOP{op=RISCVSLLI}; +"srli", SHIFTIOP{op=RISCVSRLI}; +"srai", SHIFTIOP{op=RISCVSRAI}; + +"add", RTYPE{op=RISCVADD}; +"sub", RTYPE{op=RISCVSUB}; +"sll", RTYPE{op=RISCVSLL}; +"slt", RTYPE{op=RISCVSLT}; +"sltu", RTYPE{op=RISCVSLT}; +"xor", RTYPE{op=RISCVXOR}; +"srl", RTYPE{op=RISCVSRL}; +"sra", RTYPE{op=RISCVSRA}; +"or", RTYPE{op=RISCVOR}; +"and", RTYPE{op=RISCVAND}; + +"lb", LOAD{unsigned=false; width=RISCBYTE}; +"lbu", LOAD{unsigned=true; width=RISCBYTE}; +"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=RISCBYTE}; +"sh", STORE{width=RISCVHALF}; +"sw", STORE{width=RISCVWORD}; +"sd", STORE{width=RISCVDOUBLE}; + +"addiw", ADDIW; + +"slliw", SHIFTW{op=RISCVSLL}; +"srliw", SHIFTW{op=RISCVSRL}; +"sraiw", SHIFTW{op=RISCVSRA}; + +"addw", RTYPEW{op=RISCVADDW}; +"subw", RTYPEW{op=RISCVSUBW}; +"sslw", RTYPEW{op=RISCVSLLW}; +"srlw", RTYPEW{op=RISCVSRLW}; +"sraw", RTYPEW{op=RISCVSRAW}; + diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen new file mode 100644 index 00000000..ff14c428 --- /dev/null +++ b/risc-v/hgen/map.hgen @@ -0,0 +1,12 @@ +| `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) diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen new file mode 100644 index 00000000..ba4dcac7 --- /dev/null +++ b/risc-v/hgen/parser.hgen @@ -0,0 +1,24 @@ +| UTYPE reg COMMA NUM + { `RISCVUTYPE($4, $2, $1.o) } +| JAL reg COMMA NUM + { `RISCVJAL($4, $2) } +| JALR reg COMMA reg COMMA NUM + { `RISCVJALR($6, $4, $2) } +| BTYPE reg COMMA reg COMMA NUM + { `RISCVBType($6, $4, $2, $1.op) } +| ITYPE reg COMMA reg COMMA NUM + { `RISCVIType(o$6, $4, $2, $1.op) } +| SHIFTIOP reg COMMA reg COMMA NUM + { `RISCVShiftIop($6, $4, $2, $1.op) } +| RTYPE reg COMMA reg COMMA reg + { `RISCVRType ($6, $3, $2, $1.op) } +| LOAD reg COMMA NUM LPAR reg RPAR + { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) } +| STORE reg COMMA NUM LPAR reg RPAR + { `RISCVStore($4, $6, $2, $1.width) } (* reg order? *) +| ADDIW reg COMMA reg COMMA NUM + { `RISCVADDIW ($6, $4, $2) } +| SHIFTW reg COMMA reg COMMA NUM + { `RISCVSHIFTW ($6, $4, $2, $1.op) } +| RTYPEW reg COMMA reg COMMA reg + { `RISCVRTYPEW ($6, $4, $2, $1.op) } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen new file mode 100644 index 00000000..f8cb0e30 --- /dev/null +++ b/risc-v/hgen/pretty.hgen @@ -0,0 +1,12 @@ +| `RISCVUTYPE(imm, rd, op) -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm +| `RISCVJAL(imm, rd) -> sprintf "jal %s, %d" (pp_reg rd) imm +| `RISCVJALR(imm, rs, rd) -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm +| `RISCVBType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm +| `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, rs, rd, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rd) imm (pp_reg rs) +| `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) diff --git a/risc-v/hgen/regs_out_in.hgen b/risc-v/hgen/regs_out_in.hgen new file mode 100644 index 00000000..8e1fd093 --- /dev/null +++ b/risc-v/hgen/regs_out_in.hgen @@ -0,0 +1,5 @@ +(* for each instruction instance, identify the role of the registers + and possible branching: (outputs, inputs, voidstars, branch) *) + +| `MIPSAdd -> + ([], [], [], [Next]) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen new file mode 100644 index 00000000..8064aa19 --- /dev/null +++ b/risc-v/hgen/sail_trans_out.hgen @@ -0,0 +1,12 @@ +| ("UTYPE", [imm; rd; op]) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) +| ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) +| ("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_simm12 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) +| ("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) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen new file mode 100644 index 00000000..9473d011 --- /dev/null +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -0,0 +1,99 @@ +(*| SYSCALL_THREAD_START -> `MIPSThreadStart +| (ADD (rs, rt, rd)) -> `MIPSRType (MIPSROpADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (ADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (AND (rs, rt, rd)) -> `MIPSRType (MIPSROpAND , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (DADD (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (DADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (DSUB (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (DSUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (MOVN (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (MOVZ (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (MUL (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (NOR (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (OR (rs, rt, rd)) -> `MIPSRType (MIPSROpOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (SLT (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (SLTU (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (SUB (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (SUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) +| (XOR (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) + +| (ADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (ADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (ANDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) +| (DADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (ORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) +| (SLTI (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (SLTIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) +| (XORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) + +| (DSLL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (DSLL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (DSRA (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (DSRA32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (DSRL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (DSRL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (SLL (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (SRA (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) +| (SRL (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) + +| DSLLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) +| DSRAV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) +| DSRLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) +| SLLV (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) +| SRAV (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) +| SRLV (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) + +| DDIV (rs, rt) -> `MIPSMulDiv (MIPSDDIV , (translate_out_ireg rs), (translate_out_ireg rt)) +| DDIVU (rs, rt) -> `MIPSMulDiv (MIPSDDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) +| DIV (rs, rt) -> `MIPSMulDiv (MIPSDIV , (translate_out_ireg rs), (translate_out_ireg rt)) +| DIVU (rs, rt) -> `MIPSMulDiv (MIPSDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) +| DMULT (rs, rt) -> `MIPSMulDiv (MIPSDMULT , (translate_out_ireg rs), (translate_out_ireg rt)) +| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) +| MADD (rs, rt) -> `MIPSMulDiv (MIPSMADD , (translate_out_ireg rs), (translate_out_ireg rt)) +| MADDU (rs, rt) -> `MIPSMulDiv (MIPSMADDU , (translate_out_ireg rs), (translate_out_ireg rt)) +| MSUB (rs, rt) -> `MIPSMulDiv (MIPSMSUB , (translate_out_ireg rs), (translate_out_ireg rt)) +| MSUBU (rs, rt) -> `MIPSMulDiv (MIPSMSUBU , (translate_out_ireg rs), (translate_out_ireg rt)) +| MULT (rs, rt) -> `MIPSMulDiv (MIPSMULT , (translate_out_ireg rs), (translate_out_ireg rt)) +| MULTU (rs, rt) -> `MIPSMulDiv (MIPSMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) + +| MFHI (rs) -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs)) +| MFLO (rs) -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs)) +| MTHI (rs) -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs)) +| MTLO (rs) -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs)) + +| LUI (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm)) +| Load (width, signed, linked, base, rt, offset) -> + `MIPSLoad ( + (translate_out_wordWidth width), + (translate_out_bool signed), + (translate_out_bool linked), + (translate_out_ireg base), + (translate_out_ireg rt), + (translate_out_simm16 offset) + ) +| Store (width, conditional, base, rt, offset) -> + `MIPSStore ( + (translate_out_wordWidth width), + (translate_out_bool conditional), + (translate_out_ireg base), + (translate_out_ireg rt), + (translate_out_simm16 offset) + ) +| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) +| SYNC -> `MIPSSYNC +| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely)) +| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely)) +| J (offset) -> `MIPSJ (translate_out_imm26 offset) +| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset) +| JR (rd) -> `MIPSJR (translate_out_ireg rd) +| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs) + +*)
\ No newline at end of file diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen new file mode 100644 index 00000000..2c2efd8e --- /dev/null +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -0,0 +1,40 @@ +(*let translate_out_big_bit = Sail_values.unsigned + +let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) +let translate_out_signed_int inst bits = + let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in + if (i >= (1 lsl (bits - 1))) then + (i - (1 lsl bits)) else + i + +let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) + +let translate_out_imm26 imm = translate_out_int imm + +let translate_out_imm16 imm = translate_out_int imm +let translate_out_simm16 imm = translate_out_signed_int imm 16 + +let translate_out_imm5 imm = translate_out_int imm + +let translate_out_bool = function + | Sail_values.B1 -> true + | Sail_values.B0 -> false + | _ -> failwith "translate_out_bool Undef" + + +let translate_out_wordWidth = function + | Mips_embed_types.B2 -> MIPSByte + | Mips_embed_types.H -> MIPSHalf + | Mips_embed_types.W -> MIPSWord + | Mips_embed_types.D -> MIPSDouble + +let translate_out_cmp = function + | Mips_embed_types.EQ' -> MIPS_EQ (* equal *) + | Mips_embed_types.NE -> MIPS_NE (* not equal *) + | Mips_embed_types.GE -> MIPS_GE (* signed greater than or equal *) + | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) + | Mips_embed_types.GT' -> MIPS_GT (* signed strictly greater than *) + | Mips_embed_types.LE -> MIPS_LE (* signed less than or equal *) + | Mips_embed_types.LT' -> MIPS_LT (* signed strictly less than *) + | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) +*)
\ No newline at end of file diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen new file mode 100644 index 00000000..cc993ae3 --- /dev/null +++ b/risc-v/hgen/token_types.hgen @@ -0,0 +1,12 @@ +type token_UTYPE = {op : riscvUop } +type token_JAL = unit +type token_JALR = unit +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_ADDIW = unit +type token_SHIFTW = {op : riscvSop } +type token_RTYPEW = {op : riscvRopw } diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen new file mode 100644 index 00000000..0a874b81 --- /dev/null +++ b/risc-v/hgen/tokens.hgen @@ -0,0 +1,13 @@ +%token <RISCVHGenBase.token_UTYPE> UTYPE +%token <RISCVHGenBase.token_JAL> JAL +%token <RISCVHGenBase.token_JALR> JALR +%token <RISCVHGenBase.token_BType> BTYPE +%token <RISCVHGenBase.token_IType> ITYPE +%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP +%token <RISCVHGenBase.token_RTYPE> RTYPE +%token <RISCVHGenBase.token_Load> LOAD +%token <RISCVHGenBase.token_Store> STORE +%token <RISCVHGenBase.token_ADDIW> ADDIW +%token <RISCVHGenBase.token_SHIFTW> SHIFTW +%token <RISCVHGenBase.token_RTYPEW> RTYPEW + diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen new file mode 100644 index 00000000..3b825af2 --- /dev/null +++ b/risc-v/hgen/trans_sail.hgen @@ -0,0 +1,105 @@ +| `RISCVUTYPE(imm, rd, op) -> + ("UTYPE", + [ + translate_imm20 "imm" imm; + translate_reg "rd" rd; + translate_uop "op" op; + ], + []) +| `RISCVJAL(imm, rd) -> + ("JAL", + [ + translate_imm20 "imm" imm; + translate_reg "rd" rd; + ], + []) +| `RISCVJALR(imm, rs, rd) -> + ("JALR", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rd; + translate_reg "rd" rd; + ], + []) +| `RISCVBType(imm, rs2, rs1, op) -> + ("BTYPE", + [ + translate_imm12 "imm" imm; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_bop "op" op; + ], + []) +| `RISCVIType(imm, rs1, rd, op) -> + ("ITYPE", + [ + translate_imm12 "imm" imm; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_iop "op" op; + ], + []) +| `RISCVShiftIop(imm, rs, rd, op) -> + ("SHIFTIOP", + [ + translate_imm6 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRType (rs2, rs1, rd, op) -> + ("RTYPE", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_rop "op" op; + ], + []) +| `RISCVLoad(imm, rs, rd, unsigned, width) -> + ("LOAD", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_bool "unsigned" unsigned; + translate_width "width" width; + ], + []) +| `RISCVStore(imm, rs, rd, width) -> + ("LOAD", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_width "width" width; + ], + []) +| `RISCVADDIW(imm, rs, rd) -> + ("ADDIW", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + ], + []) +| `RISCVSHIFTW(imm, rs, rd, op) -> + ("SHIFTW", + [ + translate_imm5 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRTYPEW(rs2, rs1, rd, op) -> + ("RTYPEW", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_ropw "op" op; + ], + []) + diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen new file mode 100644 index 00000000..e31b11f8 --- /dev/null +++ b/risc-v/hgen/types.hgen @@ -0,0 +1,116 @@ +type bit20 = int +type bit12 = int +type bit6 = int +type bit5 = int + +type riscvUop = (* upper immediate ops *) +| RISCVLUI +| RISCVAUIPC + +let pp_riscv_uop = function +| RISCVLUI -> "lui" +| RISCVAUIPC -> "auipc" + + +type riscvBop = (* branch ops *) +| RISCVBEQ +| RISCVBNE +| RISCVBLT +| RISCVBGE +| RISCVBLTU +| RISCVBGEU + +let pp_riscv_bop = function +| RISCVBEQ -> "beq" +| RISCVBNE -> "bne" +| RISCVBLT -> "blt" +| RISCVBGE -> "bge" +| RISCVBLTU -> "bltu" +| RISCVBGEU -> "bgeu" + +type riscvIop = (* immediate ops *) +| RISCVADDI +| RISCVSLTI +| RISCVSLTIU +| RISCVXORI +| RISCVORI +| RISCVANDI + +let pp_riscv_iop = function +| RISCVADDI -> "addi" +| RISCVSLTI -> "slti" +| RISCVSLTIU -> "sltiu" +| RISCVXORI -> "xori" +| RISCVORI -> "ori" +| RISCVANDI -> "andi" + +type riscvSop = (* shift ops *) +| RISCVSLLI +| RISCVSRLI +| RISCVSRAI + +let pp_riscv_sop = function +| RISCVSLLI -> "slli" +| RISCVSRLI -> "srli" +| RISCVSRAI -> "srai" + +type riscvRop = (* reg-reg ops *) +| RISCVADD +| RISCVSUB +| RISCVSLL +| RISCVSLT +| RISCVSLTU +| RISCVXOR +| RISCVSRL +| RISCVSRA +| RISCVOR +| RISCVAND + +let pp_riscv_rop = function +| RISCVADD -> "add" +| RISCVSUB -> "sub" +| RISCVSLL -> "sll" +| RISCVSLT -> "slt" +| RISCVSLTU -> "sltu" +| RISCVXOR -> "xor" +| RISCVSRL -> "srl" +| RISCVSRA -> "sra" +| RISCVOR -> "or" +| RISCVAND -> "and" + +type riscvRopw = (* reg-reg 32-bit ops *) +| RISCVADDW +| RISCVSUBW +| RISCVSLLW +| RISCVSRLW +| RISCVSRAW + +let pp_riscv_ropw = function +| RISCVADDW -> "addw" +| RISCVSUBW -> "subw" +| RISCVSLLW -> "sllw" +| RISCVSRLW -> "srlw" +| RISCVSRAW -> "sraw" + +type wordWidth = + | RISCVBYTE + | RISCVHALF + | 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" diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen new file mode 100644 index 00000000..99d3d375 --- /dev/null +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -0,0 +1,78 @@ +let translate_out_big_bit = function + | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits + | _ -> assert false + +let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) +let translate_out_signed_int inst bits = + let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in + if (i >= (1 lsl (bits - 1))) then + (i - (1 lsl bits)) else + i + +let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) + +let translate_out_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm12 imm = translate_out_signed_int imm 12 +let translate_out_imm6 imm = translate_out_int imm +let translate_out_imm5 imm = translate_out_int imm + +let translate_out_bool = function + | (name, Bit, [Bitc_one]) -> true + | (name, Bit, [Bitc_zero]) -> false + | _ -> assert false + +let translate_out_enum (name,_,bits) = + Nat_big_num.to_int (IInt.integer_of_bit_list bits) + +let translate_out_wordWidth w = + match translate_out_enum w with + | 0 -> RISCVBYTE + | 1 -> RISCVHALF + | 2 -> RISCVWORD + | 3 -> RISCVDOUBLE + | _ -> failwith "Unknown wordWidth in sail translate out" + +let translate_out_uop op = match translate_out_enum op with + | 0 -> RISCVLUI + | 1 -> RISCVAUIPC + | _ -> failwith "Unknown uop in sail translate out" + +let translate_out_bop op = match translate_out_enum op with +| 0 -> RISCVBEQ +| 1 -> RISCVBNE +| 2 -> RISCVBLT +| 3 -> RISCVBGE +| 4 -> RISCVBLTU +| 5 -> RISCVBGEU + +let translate_out_iop op = match translate_out_enum op with +| 0 -> RISCVADDI +| 1 -> RISCVSLTI +| 2 -> RISCVSLTIU +| 3 -> RISCVXORI +| 4 -> RISCVORI +| 5 -> RISCVANDI + +let translate_out_sop op = match translate_out_enum op with +| 0 -> RISCVSLLI +| 1 -> RISCVSRLI +| 2 -> RISCVSRAI + +let translate_out_rop op = match translate_out_enum op with +| 0 -> RISCVADD +| 1 -> RISCVSUB +| 2 -> RISCVSLL +| 3 -> RISCVSLT +| 4 -> RISCVSLTU +| 5 -> RISCVXOR +| 6 -> RISCVSRL +| 7 -> RISCVSRA +| 8 -> RISCVOR +| 9 -> RISCVAND + +let translate_out_ropw op = match translate_out_enum op with +| 0 -> RISCVADDW +| 1 -> RISCVSUBW +| 2 -> RISCVSLLW +| 3 -> RISCVSRLW +| 4 -> RISCVSRAW diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen new file mode 100644 index 00000000..9dd36d5e --- /dev/null +++ b/risc-v/hgen/types_trans_sail.hgen @@ -0,0 +1,33 @@ +let translate_enum enum_values name value = + let rec bit_count n = + if n = 0 then 0 + else 1 + (bit_count (n lsr 1)) in + let rec find_index element = function + | h::tail -> if h = element then 0 else 1 + (find_index element tail) + | _ -> failwith "translate_enum could not find value" + in + let size = bit_count (List.length enum_values) in + let index = find_index value enum_values in + (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_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_imm20 name value = + (name, Bvector (Some 26), bit_list_of_integer 26 (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_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_bool name value = + (name, Bit, [if value then Bitc_one else Bitc_zero]) diff --git a/risc-v/risc-v.sail b/risc-v/riscv.sail index 4b90e792..c91a0104 100644 --- a/risc-v/risc-v.sail +++ b/risc-v/riscv.sail @@ -72,6 +72,8 @@ 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 @@ -192,31 +194,52 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = } in wGPR(rd, result) -union ast member ((bit[12]), regno, regno, bool, [|8|]) LOAD -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 1)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 2)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 4)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 8)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 1)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 2)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 4)) +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)) = let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in let (bit[64]) result = if unsigned then - EXTZ(MEMr(addr, width)) + switch (width) { + case BYTE -> EXTZ(MEMr(addr, 1)) + case WORD -> EXTZ(MEMr(addr, 2)) + case HALF -> EXTZ(MEMr(addr, 4)) + case DOUBLE -> MEMr(addr, 8) + } else - EXTS(MEMr(addr, width)) in + switch (width) { + case BYTE -> EXTS(MEMr(addr, 1)) + case WORD -> EXTS(MEMr(addr, 2)) + case HALF -> EXTS(MEMr(addr, 4)) + case DOUBLE -> MEMr(addr, 8) + } in wGPR(rd, result) -union ast member ((bit[12]), regno, regno, [|8|]) STORE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 1)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 2)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 4)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 8)) +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)) = let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { - MEMea(addr, width); - MEMval(addr, width, rGPR(rs2)); + switch (width) { + case BYTE -> MEMea(addr, 1) + case WORD -> MEMea(addr, 2) + case HALF -> MEMea(addr, 4) + case DOUBLE -> MEMea(addr, 8) + }; + let rs2_val = rGPR(rs2) in + switch (width) { + case BYTE -> MEMval(addr, 1, rs2_val) + case WORD -> MEMval(addr, 2, rs2_val) + case HALF -> MEMval(addr, 4, rs2_val) + case DOUBLE -> MEMval(addr, 8, rs2_val) + } } union ast member ((bit[12]), regno, regno) ADDIW @@ -258,6 +281,8 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = } in wGPR(rd, EXTS(result)) +function clause decode _ = None + end ast end decode end execute diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem new file mode 100644 index 00000000..c09c85c2 --- /dev/null +++ b/risc-v/riscv_extras.lem @@ -0,0 +1,58 @@ +open import Pervasives +open import Interp_ast +open import Interp_interface +open import Sail_impl_base +open import Interp_inter_imp +import Set_extra + +let memory_parameter_transformer mode v = + match v with + | Interp_ast.V_tuple [location;length] -> + let (v,loc_regs) = extern_with_track mode extern_vector_value location in + + match length with + | Interp_ast.V_lit (L_aux (L_num len) _) -> + (v,(natFromInteger len),loc_regs) + | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> + match loc_regs with + | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))) + | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) + end + | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'" + end + | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + +let memory_parameter_transformer_option_address _mode v = + match v with + | Interp_ast.V_tuple [location;_] -> + Just (extern_vector_value location) + | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + + +let read_memory_functions : memory_reads = + [ ("MEMr", (MR Read_plain memory_parameter_transformer)); + ("MEMr_reserve", (MR Read_reserve 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)); + ] + +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))))); + ] + +let barrier_functions = [ + ("MEM_sync", Barrier_MIPS_SYNC); + ] diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem new file mode 100644 index 00000000..cbc8bd0d --- /dev/null +++ b/risc-v/riscv_extras_embed.lem @@ -0,0 +1,32 @@ +open import Pervasives +open import Pervasives_extra +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) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_conditional : (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 + +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_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_Isync + +let duplicate (bit,len) = + let bits = repeat [bit] len in + let start = len - 1 in + Vector bits start false diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem new file mode 100644 index 00000000..7fb62161 --- /dev/null +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -0,0 +1,34 @@ +open import Pervasives +open import Pervasives_extra +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) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_conditional : (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 + + +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_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_MIPS_SYNC + + +let duplicate (bit,len) = + let bits = repeat [bit] len in + let start = len - 1 in + Vector bits start false |