load-type riscv assembly

2 files changed, 43 insertions, 1 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 153b41db..67089228 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -6,11 +6,16 @@ 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_12 : bits(12) <-> 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 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 spaces_forwards : unit -> string
 function spaces_forwards () = " "
 val spaces_backwards : string -> unit
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 3431c504..17dbc288 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -35,6 +35,13 @@ function clause print_insn UTYPE(imm, rd, op) =
     RISCV_AUIPC => "auipc " ^ rd ^ ", " ^ BitStr(imm)
   }
 
+val utype_operands : (bits(20), regbits) <-> string
+mapping utype_operands = {
+  (imm, rd) <-> spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ hex_bits_20(imm)
+}
+
+mapping clause assembly = UTYPE(imm, rd, RISCV_LUI)   <-> "lui"   ^^ utype_operands(imm, rd)
+mapping clause assembly = UTYPE(imm, rd, RISCV_AUIPC) <-> "auipc" ^^ utype_operands(imm, rd)
 
 /* ****************************************************************** */
 union clause ast = RISCV_JAL : (bits(21), regbits)
@@ -292,6 +299,36 @@ function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+/* TODO FIXME: is this the actual aq/rl syntax? */
+val maybe_aq : bool <-> string
+mapping maybe_aq = {
+  true  <-> ".aq",
+  false <-> ""
+}
+
+val maybe_rl : bool <-> string
+mapping maybe_rl = {
+  true  <-> ".rl",
+  false <-> ""
+}
+
+val maybe_u : bool <-> string
+mapping maybe_u = {
+  true  <-> "u",
+  false <-> ""
+}
+
+val load_operands : (bits(12), regbits, regbits, bool, bool, bool) <-> string
+mapping load_operands = {
+  (imm, rs1, rd, is_unsigned, aq, rl) <-> maybe_u(is_unsigned) ^^ maybe_aq(aq) ^^ maybe_rl(rl) ^^ spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits_12(imm)
+}
+
+                       /* LOAD(imm, rs1, rd, is_unsigned,  width,    aq,    rl) */
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, DOUBLE,    aq,    rl) <-> "ld" ^^ load_operands(imm, rs1, rd, is_unsigned, aq, rl)
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned,   WORD,    aq,    rl) <-> "lw" ^^ load_operands(imm, rs1, rd, is_unsigned, aq, rl)
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned,   HALF,    aq,    rl) <-> "lh" ^^ load_operands(imm, rs1, rd, is_unsigned, aq, rl)
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned,   BYTE,    aq,    rl) <-> "lb" ^^ load_operands(imm, rs1, rd, is_unsigned, aq, rl)
+
 /* ****************************************************************** */
 union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)