diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 6 | ||||
| -rw-r--r-- | riscv/riscv.sail | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 4b1dd7ea..153b41db 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -6,7 +6,10 @@ union option ('a : Type) = {None : unit, Some : 'a} val spaces : unit <-> string val opt_spaces : unit <-> string val def_spaces : unit <-> string -val hex_bits : forall 'n. (atom('n), bits('n)) <-> string +val hex_bits_12 : bits(12) <-> string + +val hex_bits_12_forwards = "string_of_bits" : bits(12) -> string +val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) val spaces_forwards : unit -> string function spaces_forwards () = " " @@ -37,7 +40,6 @@ val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool - val "eq_bit" : (bit, bit) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool diff --git a/riscv/riscv.sail b/riscv/riscv.sail index ed640ad3..8e734576 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -185,7 +185,7 @@ mapping operand_sep = { val itype_operands : (bits(12), regbits, regbits) <-> string mapping itype_operands = { - (imm, rs1, rd) <-> spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits(12, imm) + (imm, rs1, rd) <-> spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits_12(imm) } mapping clause assembly = ITYPE(imm, rs1, rd, RISCV_ADDI) <-> "addi" ^^ itype_operands(imm, rs1, rd) |