4 files changed, 14 insertions, 15 deletions
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 7cf3044..7ac4294 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -288,7 +288,6 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
 union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)
 
 /* Load unsigned double is only present in RV128I, not RV64I */
-/* TODO: aq/rl */
 mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if size_bits(size) != 0b11 | not_bool(is_unsigned)
   <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if size_bits(size) != 0b11 | not_bool(is_unsigned)
 
@@ -364,7 +363,6 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
 /* ****************************************************************** */
 union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)
 
-/* TODO: aq/rl */
 mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
   <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011
 
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 4986278..d09a795 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -3,7 +3,7 @@
 
 /* These instructions are only legal if misa.C() is true.  Instead of
  * checking this in every execute clause, we currently do the check in one place
- * in the fetch-execute logic.  This may need revisiting for TestRig.
+ * in the fetch-execute logic.
  */
 
 /* ****************************************************************** */
@@ -325,7 +325,6 @@ mapping clause assembly = C_AND(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_SUBW : (cregbits, cregbits)
 
-/* TODO: invalid on RV32 */
 mapping clause encdec_compressed = C_SUBW(rsd, rs2)
       if sizeof(xlen) == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
@@ -345,7 +344,6 @@ mapping clause assembly = C_SUBW(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_ADDW : (cregbits, cregbits)
 
-/* TODO: invalid on RV32 */
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
       if sizeof(xlen) == 64
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
@@ -402,20 +400,26 @@ mapping clause assembly = C_BNEZ(imm, rs)
 union clause ast = C_SLLI : (bits(6), regbits)
 
 /* TODO: On RV32, also need shamt[5] == 0 */
-mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd) if nzui5 @ nzui40 != 0b000000 & rsd != zreg
-  <-> 0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10 if nzui5 @ nzui40 != 0b000000 & rsd != zreg
+mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg
+  <-> 0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg
 
 function clause execute (C_SLLI(shamt, rsd)) =
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
 
-mapping clause assembly = C_SLLI(shamt, rsd) if shamt != 0b000000 & rsd != zreg
-  <-> "c.slli" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(shamt) if shamt != 0b000000 & rsd != zreg
+mapping clause assembly = C_SLLI(shamt, rsd)
+      if shamt != 0b000000 & rsd != zreg
+  <-> "c.slli" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(shamt)
+      if shamt != 0b000000 & rsd != zreg
 
 /* ****************************************************************** */
 union clause ast = C_LWSP : (bits(6), regbits)
 
-mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd) if rd != zreg
-  <-> 0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 if rd != zreg
+mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd)
+      if rd != zreg
+  <-> 0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
+      if rd != zreg
 
 function clause execute (C_LWSP(uimm, rd)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index cab8d9c..b133ac2 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -2,7 +2,7 @@
 /* This file specifies the instructions in the 'M' extension.         */
 
 /* ****************************************************************** */
-/* FIXME: separate these out into separate ast variants */
+
 union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
 
 mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index f865cd1..f866fab 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -43,8 +43,6 @@ register x30 : regtype
 register x31 : regtype
 
 val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape}
-/*function rX 0 = 0x0000000000000000
-and rX (r if r > 0) = Xs[r]*/
 function rX r = {
   let v : regtype =
     match r {
@@ -136,7 +134,6 @@ function wX (r, in_v) = {
   };
   if (r != 0) then {
      rvfi_wX(r, in_v);
-     // Xs[r] = v;
      print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
   }
 }