diff options
| -rw-r--r-- | riscv/main.sail | 12 | ||||
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv.sail | 28 | ||||
| -rw-r--r-- | src/sail_lib.ml | 20 |
4 files changed, 60 insertions, 4 deletions
diff --git a/riscv/main.sail b/riscv/main.sail index 28afe5ac..43820e25 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -34,10 +34,16 @@ val elf_entry = { c: "elf_entry" } : unit -> int -val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} +val main : unit -> unit effect pure //{barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} function main () = { - PC = __GetSlice_int(64, elf_entry(), 0); + + print(assembly(ITYPE(0b000000000000, 0b00000, 0b11010, RISCV_ADDI))); + print(assembly(assembly("addi zero, zero, 0x0"))); + print(assembly(assembly("ldu.aq zero, zero, 0x0"))); + print_bits("assembled lui zero, 0x0: ", encdec(assembly("lui zero, 0x0"))); + print_bits("assembled jal zero, 0x123456 : ", encdec(assembly("jal zero, 0x123456"))); + /*PC = __GetSlice_int(64, elf_entry(), 0); try { init_sys (); loop () @@ -45,5 +51,5 @@ function main () = { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), Error_EBREAK() => print("EBREAK"), Error_internal_error() => print("Error: internal error") - } + }*/ } diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 67089228..be81ce17 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -15,6 +15,10 @@ val hex_bits_20 : bits(20) <-> string val hex_bits_20_forwards = "string_of_bits" : bits(20) -> string val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) +val hex_bits_21 : bits(21) <-> string +val hex_bits_21_forwards = "string_of_bits" : bits(21) -> string +val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) + val spaces_forwards : unit -> string function spaces_forwards () = " " diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 17dbc288..f0380ffc 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -15,12 +15,18 @@ scattered function print_insn val assembly : ast <-> string scattered mapping assembly +val encdec : ast <-> bits(32) +scattered mapping encdec + /* ****************************************************************** */ union clause ast = UTYPE : (bits(20), regbits, uop) function clause decode imm : bits(20) @ rd : regbits @ 0b0110111 = Some(UTYPE(imm, rd, RISCV_LUI)) function clause decode imm : bits(20) @ rd : regbits @ 0b0010111 = Some(UTYPE(imm, rd, RISCV_AUIPC)) +mapping clause encdec = UTYPE(imm, rd, RISCV_LUI) <-> imm : bits(20) @ rd : regbits @ 0b0110111 +mapping clause encdec = UTYPE(imm, rd, RISCV_AUIPC) <-> imm : bits(20) @ rd : regbits @ 0b0010111 + function clause execute UTYPE(imm, rd, op) = let off : xlenbits = EXTS(imm @ 0x000) in let ret : xlenbits = match op { @@ -48,6 +54,11 @@ union clause ast = RISCV_JAL : (bits(21), regbits) function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_JAL(imm[19] @ imm[7..0] @ imm[8] @ imm[18..13] @ imm[12..9] @ 0b0, rd)) +/* TODO: handle 2-byte-alignment in mappings */ + +mapping clause encdec = RISCV_JAL(imm_19 : bits(1) @ imm_7_0 : bits(8) @ imm_8 : bits(1) @ imm_18_13 : bits(6) @ imm_12_9 : bits(4) @ 0b0, rd) + <-> imm_19 : bits(1) @ imm_18_13 : bits(6) @ imm_12_9 : bits(4) @ imm_8 : bits(1) @ imm_7_0 : bits(8) @ rd : regbits @ 0b1101111 + function clause execute (RISCV_JAL(imm, rd)) = { let pc : xlenbits = PC; X(rd) = nextPC; /* compatible with JAL and C.JAL */ @@ -58,6 +69,8 @@ function clause execute (RISCV_JAL(imm, rd)) = { function clause print_insn (RISCV_JAL(imm, rd)) = "jal " ^ rd ^ ", " ^ BitStr(imm) +mapping clause assembly = RISCV_JAL(imm, rd) <-> "jal" ^^ spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ hex_bits_21(imm) + /* ****************************************************************** */ union clause ast = RISCV_JALR : (bits(12), regbits, regbits) @@ -379,6 +392,18 @@ function clause print_insn (STORE(imm, rs2, rs1, width, aq, rl)) = } in insn ^ rs2 ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) +val store_operands : (bits(12), regbits, regbits, bool, bool) <-> string +mapping store_operands = { + (imm, rs1, rd, aq, rl) <-> maybe_aq(aq) ^^ maybe_rl(rl) ^^ spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits_12(imm) +} + + /* STORE(imm, rs1, rd, width, aq, rl) */ +mapping clause assembly = STORE(imm, rs1, rd, DOUBLE, aq, rl) <-> "sd" ^^ store_operands(imm, rs1, rd, aq, rl) +mapping clause assembly = STORE(imm, rs1, rd, WORD, aq, rl) <-> "sw" ^^ store_operands(imm, rs1, rd, aq, rl) +mapping clause assembly = STORE(imm, rs1, rd, HALF, aq, rl) <-> "sh" ^^ store_operands(imm, rs1, rd, aq, rl) +mapping clause assembly = STORE(imm, rs1, rd, BYTE, aq, rl) <-> "sb" ^^ store_operands(imm, rs1, rd, aq, rl) + + /* ****************************************************************** */ union clause ast = ADDIW : (bits(12), regbits, regbits) @@ -1532,4 +1557,5 @@ end decode end decodeCompressed end execute end print_insn -end assembly
\ No newline at end of file +end assembly +end encdec
\ No newline at end of file diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 415fc9fd..bab4000b 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -654,3 +654,23 @@ let hex_bits_12_matches_prefix s = ZSome ((bits_of_int 2048 n, len)) else ZNone () + +let hex_bits_20_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 1048576 then + ZSome ((bits_of_int 524288 n, len)) + else + ZNone () + +let hex_bits_21_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 2097152 then + ZSome ((bits_of_int 1048576 n, len)) + else + ZNone () |