Merge branch 'master' into inst_extensionsinst_extensions

17 files changed, 256 insertions, 222 deletions

diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md
index 4533b8b..82a418d 100644
--- a/doc/ExtendingGuide.md
+++ b/doc/ExtendingGuide.md
@@ -33,6 +33,15 @@ existing definitions for privilege levels and exceptions in
 `riscv_types.sail`, and modifying the exception handling and privilege
 transition functions in `riscv_sys_control.sail`.
 
+Modifying exception handling
+----------------------------
+
+An extension that needs to interact closely with exception handling
+may need to capture additional information at the time of an
+exception.  This is supported using the `ext` field in the
+`sync_exception` type in `riscv_sync_exception.sail`, which is where
+the extension can store this information.
+
 Adding low-level platform functionality
 ---------------------------------------
 
@@ -91,6 +100,13 @@ The handling of the memory addresses involved during exception
 handling can be extending using the interface defined in
 `riscv_sys_exceptions.sail`.
 
+Checking and transforming the program counter
+---------------------------------------------
+
+An extension might want to similarly check and transform accesses to
+the program counter.  This is supported by supplying implementations
+of the functions defined in `riscv_pc_access.sail`.
+
 Adding new instructions
 -----------------------
 
diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index 5c7e656..ad09cf0 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -25,13 +25,21 @@ The model contains the following Sail modules in the `model` directory:
   register type is separately defined in `riscv_reg_type.sail` so that
   extensions of the model can redefine it if required.
 
+- `riscv_regs.sail` contains the base register file, where each
+  register is defined as having the `regtype` type defined in
+  `riscv_reg_type.sail`.
+
+- `riscv_pc_access.sail` defines functions to access and modify the
+  program counter.
+
 - `riscv_sys_regs.sail` describes the privileged architectural state,
   viz. M-mode and S-mode CSRs, and contains helpers to interpret their
   content, such as WLRL and WARL fields.  `riscv_sys_control.sail`
   describes interrupt and exception delegation and dispatch, and the
   handling of privilege transitions. `riscv_sys_exceptions.sail`
   defines the handling of the addresses involved in exception
-  handling.
+  handling. `riscv_sync_exception.sail` describes the structure used
+  to capture the architectural information for an exception.
 
   Since WLRL and WARL fields are intended to capture platform-specific
   functionality, future versions of the model might separate their
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 25b6396..28e688d 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -46,7 +46,7 @@ type ext_data_addr_error = unit
 
 /* Default data addr is just base register + immediate offset (may be zero).
    Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regbits, offset : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
          -> Ext_DataAddr_Check(ext_data_addr_error) =
   let addr = X(base) + offset in
   Ext_DataAddr_OK(addr)
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 7dd20f3..0410f50 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -21,18 +21,18 @@ function lrsc_width_str(width : word_width) -> string =
   }
 
 /* ****************************************************************** */
-union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
+union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
 mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
   <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
-val default_loadres : (bool, bool, regbits, word_width, regbits) -> bool effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
+val default_loadres : (bool, bool, regidx, word_width, regidx) -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
 function default_loadres (aq, rl, rs1, width, rd) = {
   /* Get the address, X(rs1) (no offset).
    * Extensions might perform additional checks on address validity.
    */
   match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
-    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) => {
       let aligned : bool =
          /* BYTE and HALF would not occur due to the above check, but it doesn't hurt
@@ -48,9 +48,9 @@ function default_loadres (aq, rl, rs1, width, rd) = {
        * - Andrew Waterman, isa-dev, 10 Jul 2018.
        */
       if (~ (aligned))
-      then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
       else match translateAddr(vaddr, Read, Data) {
-             TR_Failure(e)    => { handle_mem_exception(vaddr, e); false },
+             TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
              TR_Address(addr) =>
                match (width, sizeof(xlen)) {
                  (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
@@ -75,7 +75,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
     }
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -83,13 +83,13 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
   <-> "lr." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
 /* ****************************************************************** */
-union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)
+union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)
 
 mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)
   <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
-val default_storecon : (bool, bool, regbits, regbits, word_width, regbits) -> bool effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
+val default_storecon : (bool, bool, regidx, regidx, word_width, regidx) -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
 function default_storecon (aq, rl, rs2, rs1, width, rd) = {
   /* normal non-rmem case
    * rmem: SC is allowed to succeed (but might fail later)
@@ -98,7 +98,7 @@ function default_storecon (aq, rl, rs2, rs1, width, rd) = {
    * Extensions might perform additional checks on address validity.
    */
   match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
-    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) => {
       let aligned : bool =
         /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
@@ -111,14 +111,14 @@ function default_storecon (aq, rl, rs2, rs1, width, rd) = {
           DOUBLE => vaddr[2..0] == 0b000
         };
       if (~ (aligned))
-      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
       else {
         if match_reservation(vaddr) == false then {
           /* cannot happen in rmem */
-          X(rd) = EXTZ(0b1); cancel_reservation(); true
+          X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
         } else {
           match translateAddr(vaddr, Write, Data) {
-            TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+            TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
             TR_Address(addr) => {
               let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
                 (WORD, _)    => mem_write_ea(addr, 4, aq, rl, true),
@@ -128,7 +128,7 @@ function default_storecon (aq, rl, rs2, rs1, width, rd) = {
                 _            => internal_error("STORECON expected word or double")
               };
               match (eares) {
-                MemException(e) => { handle_mem_exception(addr, e); false },
+                MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
                 MemValue(_) => {
                   rs2_val = X(rs2);
                   let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
@@ -139,9 +139,9 @@ function default_storecon (aq, rl, rs2, rs1, width, rd) = {
                     _            => internal_error("STORECON expected word or double")
                   };
                   match (res) {
-                    MemValue(true)  => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
-                    MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
-                    MemException(e) => { handle_mem_exception(addr, e); false }
+                    MemValue(true)  => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS },
+                    MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS },
+                    MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
                   }
                 }
               }
@@ -158,7 +158,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
     /* should only happen in rmem
      * rmem: allow SC to fail very early
      */
-    X(rd) = EXTZ(0b1); true
+    X(rd) = EXTZ(0b1); RETIRE_SUCCESS
   } else {
     if haveAtomics() then {
       /* dispatch defined combinations to the default implementation, others to the extension hook. */
@@ -170,7 +170,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       }
     } else {
       handle_illegal();
-      false
+      RETIRE_FAIL
     }
   }
 }
@@ -179,7 +179,7 @@ mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)
   <-> "sc." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)
+union clause ast = AMO : (amoop, bool, bool, regidx, regidx, word_width, regidx)
 
 mapping encdec_amoop : amoop <-> bits(5) = {
   AMOSWAP <-> 0b00001,
@@ -204,10 +204,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
      * Some extensions perform additional checks on address validity.
      */
     match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
-      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
         match translateAddr(vaddr, ReadWrite, Data) {
-          TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+          TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
           TR_Address(addr) => {
             let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
               (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
@@ -216,7 +216,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
             };
             rs2_val : xlenbits = X(rs2);
             match (eares) {
-              MemException(e) => { handle_mem_exception(addr, e); false },
+              MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
               MemValue(_) => {
                 let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
                   (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
@@ -224,7 +224,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   _            => internal_error ("AMO expected WORD or DOUBLE")
                 };
                 match (rval) {
-                  MemException(e)  => { handle_mem_exception(addr, e); false },
+                  MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL },
                   MemValue(loaded) => {
                     result  : xlenbits =
                       match op {
@@ -249,9 +249,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                       _            => internal_error("AMO expected WORD or DOUBLE")
                     };
                     match (wval) {
-                      MemValue(true)  => { X(rd) = loaded; true },
+                      MemValue(true)  => { X(rd) = loaded; RETIRE_SUCCESS },
                       MemValue(false) => { internal_error("AMO got false from mem_write_value") },
-                      MemException(e) => { handle_mem_exception(addr, e); false }
+                      MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
                     }
                   }
                 }
@@ -263,7 +263,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     }
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index c68c266..a9ebd8f 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -3,7 +3,7 @@
 
 
 /* ****************************************************************** */
-union clause ast = UTYPE : (bits(20), regbits, uop)
+union clause ast = UTYPE : (bits(20), regidx, uop)
 
 mapping encdec_uop : uop <-> bits(7) = {
   RISCV_LUI   <-> 0b0110111,
@@ -20,7 +20,7 @@ function clause execute UTYPE(imm, rd, op) = {
     RISCV_AUIPC => PC + off
   };
   X(rd) = ret;
-  true
+  RETIRE_SUCCESS
 }
 
 mapping utype_mnemonic : uop <-> string = {
@@ -32,7 +32,7 @@ mapping clause assembly = UTYPE(imm, rd, op)
   <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
 
 /* ****************************************************************** */
-union clause ast = RISCV_JAL : (bits(21), regbits)
+union clause ast = RISCV_JAL : (bits(21), regidx)
 
 mapping clause encdec = RISCV_JAL(imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9 @ 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 @ 0b1101111
@@ -55,18 +55,18 @@ function clause execute (RISCV_JAL(imm, rd)) = {
   match ext_control_check_pc(t) {
     Ext_ControlAddr_Error(e) => {
       ext_handle_control_check_error(e);
-      false
+      RETIRE_FAIL
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
       if   target[1] & (~ (haveRVC()))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align);
-        false
+        RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();
         set_next_pc(target);
-        true
+        RETIRE_SUCCESS
       }
     }
   }
@@ -78,7 +78,7 @@ mapping clause assembly = RISCV_JAL(imm, rd)
   <-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_21(imm)
 
 /* ****************************************************************** */
-union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
+union clause ast = RISCV_JALR : (bits(12), regidx, regidx)
 
 mapping clause encdec = RISCV_JALR(imm, rs1, rd)
   <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111
@@ -89,7 +89,7 @@ mapping clause assembly = RISCV_JALR(imm, rs1, rd)
 /* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
 
 /* ****************************************************************** */
-union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
+union clause ast = BTYPE : (bits(13), regidx, regidx, bop)
 
 mapping encdec_bop : bop <-> bits(3) = {
   RISCV_BEQ  <-> 0b000,
@@ -120,19 +120,19 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
     match ext_control_check_pc(t) {
       Ext_ControlAddr_Error(e) => {
         ext_handle_control_check_error(e);
-        false
+        RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
         if target[1] & (~ (haveRVC())) then {
           handle_mem_exception(target, E_Fetch_Addr_Align);
-          false;
+          RETIRE_FAIL;
         } else {
           set_next_pc(target);
-          true
+          RETIRE_SUCCESS
         }
       }
     }
-  } else true
+  } else RETIRE_SUCCESS
 }
 
 mapping btype_mnemonic : bop <-> string = {
@@ -148,7 +148,7 @@ mapping clause assembly = BTYPE(imm, rs2, rs1, op)
   <-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_13(imm)
 
 /* ****************************************************************** */
-union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
 
 mapping encdec_iop : iop <-> bits(3) = {
   RISCV_ADDI  <-> 0b000,
@@ -174,7 +174,7 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
     RISCV_XORI  => rs1_val ^ immext
   };
   X(rd) = result;
-  true
+  RETIRE_SUCCESS
 }
 
 mapping itype_mnemonic : iop <-> string = {
@@ -190,7 +190,7 @@ mapping clause assembly = ITYPE(imm, rs1, rd, op)
   <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
 
 /* ****************************************************************** */
-union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop)
+union clause ast = SHIFTIOP : (bits(6), regidx, regidx, sop)
 
 mapping encdec_sop : sop <-> bits(3) = {
   RISCV_SLLI <-> 0b001,
@@ -217,7 +217,7 @@ function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = {
                   else shift_right_arith64(rs1_val, shamt)
   };
   X(rd) = result;
-  true
+  RETIRE_SUCCESS
 }
 
 mapping shiftiop_mnemonic : sop <-> string = {
@@ -230,7 +230,7 @@ mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op)
   <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt)
 
 /* ****************************************************************** */
-union clause ast = RTYPE : (regbits, regbits, regbits, rop)
+union clause ast = RTYPE : (regidx, regidx, regidx, rop)
 
 mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_ADD)  <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011
 mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SLT)  <-> 0b0000000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011
@@ -265,7 +265,7 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
                   else shift_right_arith64(rs1_val, rs2_val[5..0])
   };
   X(rd) = result;
-  true
+  RETIRE_SUCCESS
 }
 
 mapping rtype_mnemonic : rop <-> string = {
@@ -285,7 +285,7 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
   <-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)
+union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool)
 
 /* Load unsigned double is only present in RV128I, not RV64I */
 mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if size_bits(size) != 0b11 | not_bool(is_unsigned)
@@ -296,12 +296,12 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
   match ext_data_get_addr(rs1, offset, Read, Data, width) {
-    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
       else match translateAddr(vaddr, Read, Data) {
-        TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+        TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr) =>
           match (width, sizeof(xlen)) {
             (BYTE, _)   =>
@@ -336,10 +336,10 @@ mapping maybe_u = {
 }
 
 mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
-  <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+  <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
 /* ****************************************************************** */
-union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)
+union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
 
 mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
   <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011
@@ -351,12 +351,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
   match ext_data_get_addr(rs1, offset, Write, Data, width) {
-    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
       else match translateAddr(vaddr, Write, Data) {
-        TR_Failure(e)    => { handle_mem_exception(vaddr, e); false },
+        TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr) => {
           let eares : MemoryOpResult(unit) = match width {
             BYTE   => mem_write_ea(addr, 1, aq, rl, false),
@@ -365,7 +365,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
             DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
           };
           match (eares) {
-            MemException(e) => { handle_mem_exception(addr, e); false },
+            MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
             MemValue(_) => {
               let rs2_val = X(rs2);
               let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
@@ -375,9 +375,9 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
                 (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
               };
               match (res) {
-                MemValue(true)  => true,
+                MemValue(true)  => RETIRE_SUCCESS,
                 MemValue(false) => internal_error("store got false from mem_write_value"),
-                MemException(e) => { handle_mem_exception(addr, e); false }
+                MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
               }
             }
           }
@@ -386,11 +386,11 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   }
 }
 
-mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl)
-  <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl)
+  <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
 /* ****************************************************************** */
-union clause ast = ADDIW : (bits(12), regbits, regbits)
+union clause ast = ADDIW : (bits(12), regidx, regidx)
 
 mapping clause encdec = ADDIW(imm, rs1, rd)
       if sizeof(xlen) == 64
@@ -400,7 +400,7 @@ mapping clause encdec = ADDIW(imm, rs1, rd)
 function clause execute (ADDIW(imm, rs1, rd)) = {
   let result : xlenbits = EXTS(imm) + X(rs1);
   X(rd) = EXTS(result[31..0]);
-  true
+  RETIRE_SUCCESS
 }
 
 mapping clause assembly = ADDIW(imm, rs1, rd)
@@ -409,7 +409,7 @@ mapping clause assembly = ADDIW(imm, rs1, rd)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
+union clause ast = SHIFTW : (bits(5), regidx, regidx, sop)
 
 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI)
       if sizeof(xlen) == 64
@@ -432,7 +432,7 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
     RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
   };
   X(rd) = EXTS(result);
-  true
+  RETIRE_SUCCESS
 }
 
 mapping shiftw_mnemonic : sop <-> string = {
@@ -447,7 +447,7 @@ mapping clause assembly = SHIFTW(shamt, rs1, rd, op)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
+union clause ast = RTYPEW : (regidx, regidx, regidx, ropw)
 
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW)
       if sizeof(xlen) == 64
@@ -481,7 +481,7 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
     RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
   };
   X(rd) = EXTS(result);
-  true
+  RETIRE_SUCCESS
 }
 
 mapping rtypew_mnemonic : ropw <-> string = {
@@ -498,7 +498,7 @@ mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw)
+union clause ast = SHIFTIWOP : (bits(5), regidx, regidx, sopw)
 
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
       if sizeof(xlen) == 64
@@ -521,7 +521,7 @@ function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
     RISCV_SRAIW => shift_right_arith32(rs1_val[31..0], shamt)
   };
   X(rd) = EXTS(result);
-  true
+  RETIRE_SUCCESS
 }
 
 mapping shiftiwop_mnemonic : sopw <-> string = {
@@ -558,7 +558,7 @@ function clause execute (FENCE(pred, succ)) = {
     _ => { print("FIXME: unsupported fence");
            () }
   };
-  true
+  RETIRE_SUCCESS
 }
 
 mapping bit_maybe_r : bits(1) <-> string = {
@@ -602,7 +602,7 @@ function clause execute (FENCE_TSO(pred, succ)) = {
     _ => { print("FIXME: unsupported fence");
            () }
   };
-  true
+  RETIRE_SUCCESS
 }
 
 mapping clause assembly = FENCE_TSO(pred, succ)
@@ -615,7 +615,7 @@ mapping clause encdec = FENCEI()
   <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
 /* fence.i is a nop for the memory model */
-function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ true }
+function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SUCCESS }
 
 mapping clause assembly = FENCEI() <-> "fence.i"
 
@@ -635,7 +635,7 @@ function clause execute ECALL() = {
              excinfo = (None() : option(xlenbits)),
              ext     = None() };
   set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC));
-  false
+  RETIRE_FAIL
 }
 
 mapping clause assembly = ECALL() <-> "ecall"
@@ -650,7 +650,7 @@ function clause execute MRET() = {
   if   cur_privilege == Machine
   then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC))
   else handle_illegal();
-  false
+  RETIRE_FAIL
 }
 
 mapping clause assembly = MRET() <-> "mret"
@@ -671,7 +671,7 @@ function clause execute SRET() = {
                   then handle_illegal()
                   else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC))
   };
-  false
+  RETIRE_FAIL
 }
 
 mapping clause assembly = SRET() <-> "sret"
@@ -684,7 +684,7 @@ mapping clause encdec = EBREAK()
 
 function clause execute EBREAK() = {
   handle_mem_exception(PC, E_Breakpoint);
-  false
+  RETIRE_FAIL
 }
 
 mapping clause assembly = EBREAK() <-> "ebreak"
@@ -697,17 +697,17 @@ mapping clause encdec = WFI()
 
 function clause execute WFI() =
   match cur_privilege {
-    Machine    => { platform_wfi(); true },
+    Machine    => { platform_wfi(); RETIRE_SUCCESS },
     Supervisor => if   mstatus.TW() == true
-                  then { handle_illegal(); false }
-                  else { platform_wfi(); true },
-    User       => { handle_illegal(); false }
+                  then { handle_illegal(); RETIRE_FAIL }
+                  else { platform_wfi(); RETIRE_SUCCESS },
+    User       => { handle_illegal(); RETIRE_FAIL }
   }
 
 mapping clause assembly = WFI() <-> "wfi"
 
 /* ****************************************************************** */
-union clause ast = SFENCE_VMA : (regbits, regbits)
+union clause ast = SFENCE_VMA : (regidx, regidx)
 
 mapping clause encdec = SFENCE_VMA(rs1, rs2)
   <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
@@ -716,13 +716,13 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
   let addr : option(xlenbits) = if rs1 == 0 then None() else Some(X(rs1));
   let asid : option(xlenbits) = if rs2 == 0 then None() else Some(X(rs2));
   match cur_privilege {
-    User       => { handle_illegal(); false },
+    User       => { handle_illegal(); RETIRE_FAIL },
     Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) {
-                    (Some(_), true)  => { handle_illegal(); false },
-                    (Some(_), false) => { flush_TLB(asid, addr); true },
+                    (Some(_), true)  => { handle_illegal(); RETIRE_FAIL },
+                    (Some(_), false) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
                     (_, _)           => internal_error("unimplemented sfence architecture")
                   },
-    Machine    => { flush_TLB(asid, addr); true }
+    Machine    => { flush_TLB(asid, addr); RETIRE_SUCCESS }
   }
 }
 
diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index d922249..8e98271 100644
--- a/model/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
@@ -6,7 +6,7 @@
 scattered union ast
 
 /* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> bool effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
+val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
 scattered function execute
 
 val assembly : ast <-> string
@@ -22,4 +22,4 @@ scattered mapping encdec_compressed
  * this hook allows the extension to implement these ast.  it has the
  * same semantics as execute.
  */
-val ext_execute : ast -> bool effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
+val ext_execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 27acf7a..c58c636 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -12,22 +12,22 @@ union clause ast = C_NOP : unit
 mapping clause encdec_compressed = C_NOP()
   <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01
 
-function clause execute C_NOP() = true
+function clause execute C_NOP() = RETIRE_SUCCESS
 
 mapping clause assembly = C_NOP() <-> "c.nop"
 
 /* ****************************************************************** */
 
-union clause ast = C_ADDI4SPN : (cregbits, bits(8))
+union clause ast = C_ADDI4SPN : (cregidx, bits(8))
 
 mapping clause encdec_compressed = C_ADDI4SPN(rd, nz96 @ nz54 @ nz3 @ nz2)
       if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
-  <-> 0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00
+  <-> 0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregidx @ 0b00
       if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
 
 function clause execute (C_ADDI4SPN(rdc, nzimm)) = {
   let imm : bits(12) = (0b00 @ nzimm @ 0b00);
-  let rd = creg2reg_bits(rdc);
+  let rd = creg2reg_idx(rdc);
   execute(ITYPE(imm, sp, rd, RISCV_ADDI))
 }
 
@@ -37,15 +37,15 @@ mapping clause assembly = C_ADDI4SPN(rdc, nzimm)
       if nzimm != 0b00000000
 
 /* ****************************************************************** */
-union clause ast = C_LW : (bits(5), cregbits, cregbits)
+union clause ast = C_LW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd)
-  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregbits @ 0b00
+  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
 
 function clause execute (C_LW(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
-  let rd = creg2reg_bits(rdc);
-  let rs = creg2reg_bits(rsc);
+  let rd = creg2reg_idx(rdc);
+  let rs = creg2reg_idx(rsc);
   execute(LOAD(imm, rs, rd, false, WORD, false, false))
 }
 
@@ -53,17 +53,17 @@ mapping clause assembly = C_LW(uimm, rsc, rdc)
   <-> "c.lw" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_7(uimm @ 0b00)
 
 /* ****************************************************************** */
-union clause ast = C_LD : (bits(5), cregbits, cregbits)
+union clause ast = C_LD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd)
       if sizeof(xlen) == 64
-  <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00
+  <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
       if sizeof(xlen) == 64
 
 function clause execute (C_LD(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
-  let rd = creg2reg_bits(rdc);
-  let rs = creg2reg_bits(rsc);
+  let rd = creg2reg_idx(rdc);
+  let rs = creg2reg_idx(rsc);
   execute(LOAD(imm, rs, rd, false, DOUBLE, false, false))
 }
 
@@ -73,15 +73,15 @@ mapping clause assembly = C_LD(uimm, rsc, rdc)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_SW : (bits(5), cregbits, cregbits)
+union clause ast = C_SW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2)
-  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregbits @ 0b00
+  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
 
 function clause execute (C_SW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
-  let rs1 = creg2reg_bits(rsc1);
-  let rs2 = creg2reg_bits(rsc2);
+  let rs1 = creg2reg_idx(rsc1);
+  let rs2 = creg2reg_idx(rsc2);
   execute(STORE(imm, rs2, rs1, WORD, false, false))
 }
 
@@ -89,7 +89,7 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2)
   <-> "c.sw" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_7(uimm @ 0b00)
 
 /* ****************************************************************** */
-union clause ast = C_SD : (bits(5), cregbits, cregbits)
+union clause ast = C_SD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
       if sizeof(xlen) == 64
@@ -98,8 +98,8 @@ mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
 
 function clause execute (C_SD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
-  let rs1 = creg2reg_bits(rsc1);
-  let rs2 = creg2reg_bits(rsc2);
+  let rs1 = creg2reg_idx(rsc1);
+  let rs2 = creg2reg_idx(rsc2);
   execute(STORE(imm, rs2, rs1, DOUBLE, false, false))
 }
 
@@ -109,11 +109,11 @@ mapping clause assembly = C_SD(uimm, rsc1, rsc2)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_ADDI : (bits(6), regbits)
+union clause ast = C_ADDI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDI(nzi5 @ nzi40, rsd)
       if nzi5 @ nzi40 != 0b000000 & rsd != zreg
-  <-> 0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01
+  <-> 0b000 @ nzi5 : bits(1) @ rsd : regidx @ nzi40 : bits(5) @ 0b01
       if nzi5 @ nzi40 != 0b000000 & rsd != zreg
 
 function clause execute (C_ADDI(nzi, rsd)) = {
@@ -143,11 +143,11 @@ mapping clause assembly = C_JAL(imm)
       if sizeof(xlen) == 32
 
 /* ****************************************************************** */
-union clause ast = C_ADDIW : (bits(6), regbits)
+union clause ast = C_ADDIW : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
       if rsd != zreg & sizeof(xlen) == 64
-  <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
+  <-> 0b001 @ imm5 : bits(1) @ rsd : regidx @ imm40 : bits(5) @ 0b01
       if rsd != zreg & sizeof(xlen) == 64
 
 function clause execute (C_ADDIW(imm, rsd)) =
@@ -159,11 +159,11 @@ mapping clause assembly = C_ADDIW(imm, rsd)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_LI : (bits(6), regbits)
+union clause ast = C_LI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LI(imm5 @ imm40, rd)
       if rd != zreg
-  <-> 0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01
+  <-> 0b010 @ imm5 : bits(1) @ rd : regidx @ imm40 : bits(5) @ 0b01
       if rd != zreg
 
 function clause execute (C_LI(imm, rd)) = {
@@ -195,11 +195,11 @@ mapping clause assembly = C_ADDI16SP(imm)
       if imm != 0b000000
 
 /* ****************************************************************** */
-union clause ast = C_LUI : (bits(6), regbits)
+union clause ast = C_LUI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LUI(imm17 @ imm1612, rd)
       if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
-  <-> 0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01
+  <-> 0b011 @ imm17 : bits(1) @ rd : regidx @ imm1612 : bits(5) @ 0b01
       if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
 
 function clause execute (C_LUI(imm, rd)) = {
@@ -213,15 +213,15 @@ mapping clause assembly = C_LUI(imm, rd)
       if rd != zreg & rd != sp & imm != 0b000000
 
 /* ****************************************************************** */
-union clause ast = C_SRLI : (bits(6), cregbits)
+union clause ast = C_SRLI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRLI(nzui5 @ nzui40, rsd)
       if nzui5 @ nzui40 != 0b000000
-  <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01
+  <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
       if nzui5 @ nzui40 != 0b000000
 
 function clause execute (C_SRLI(shamt, rsd)) = {
-  let rsd = creg2reg_bits(rsd);
+  let rsd = creg2reg_idx(rsd);
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRLI))
 }
 
@@ -231,15 +231,15 @@ mapping clause assembly = C_SRLI(shamt, rsd)
       if shamt != 0b000000
 
 /* ****************************************************************** */
-union clause ast = C_SRAI : (bits(6), cregbits)
+union clause ast = C_SRAI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRAI(nzui5 @ nzui40, rsd)
       if nzui5 @ nzui40 != 0b000000
-  <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01
+  <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
       if nzui5 @ nzui40 != 0b000000
 
 function clause execute (C_SRAI(shamt, rsd)) = {
-  let rsd = creg2reg_bits(rsd);
+  let rsd = creg2reg_idx(rsd);
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRAI))
 }
 
@@ -249,13 +249,13 @@ mapping clause assembly = C_SRAI(shamt, rsd)
       if shamt != 0b000000
 
 /* ****************************************************************** */
-union clause ast = C_ANDI : (bits(6), cregbits)
+union clause ast = C_ANDI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd)
-  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregbits @ i40 : bits(5) @ 0b01
+  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01
 
 function clause execute (C_ANDI(imm, rsd)) = {
-  let rsd = creg2reg_bits(rsd);
+  let rsd = creg2reg_idx(rsd);
   execute(ITYPE(EXTS(imm), rsd, rsd, RISCV_ANDI))
 }
 
@@ -263,14 +263,14 @@ mapping clause assembly = C_ANDI(imm, rsd)
   <-> "c.andi" ^ spc() ^ creg_name(rsd) ^ sep() ^ hex_bits_6(imm)
 
 /* ****************************************************************** */
-union clause ast = C_SUB : (cregbits, cregbits)
+union clause ast = C_SUB : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SUB(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
 
 function clause execute (C_SUB(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPE(rs2, rsd, rsd, RISCV_SUB))
 }
 
@@ -278,14 +278,14 @@ mapping clause assembly = C_SUB(rsd, rs2)
   <-> "c.sub" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = C_XOR : (cregbits, cregbits)
+union clause ast = C_XOR : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_XOR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
 
 function clause execute (C_XOR(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPE(rs2, rsd, rsd, RISCV_XOR))
 }
 
@@ -293,14 +293,14 @@ mapping clause assembly = C_XOR(rsd, rs2)
   <-> "c.xor" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = C_OR : (cregbits, cregbits)
+union clause ast = C_OR : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_OR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b10 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01
 
 function clause execute (C_OR(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPE(rs2, rsd, rsd, RISCV_OR))
 }
 
@@ -308,14 +308,14 @@ mapping clause assembly = C_OR(rsd, rs2)
   <-> "c.or" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = C_AND : (cregbits, cregbits)
+union clause ast = C_AND : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_AND(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b11 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01
 
 function clause execute (C_AND(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPE(rs2, rsd, rsd, RISCV_AND))
 }
 
@@ -323,16 +323,16 @@ mapping clause assembly = C_AND(rsd, rs2)
   <-> "c.and" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = C_SUBW : (cregbits, cregbits)
+union clause ast = C_SUBW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SUBW(rsd, rs2)
       if sizeof(xlen) == 64
-  <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
       if sizeof(xlen) == 64
 
 function clause execute (C_SUBW(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPEW(rs2, rsd, rsd, RISCV_SUBW))
 }
 
@@ -342,16 +342,16 @@ mapping clause assembly = C_SUBW(rsd, rs2)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_ADDW : (cregbits, cregbits)
+union clause ast = C_ADDW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
       if sizeof(xlen) == 64
-  <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
+  <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
       if sizeof(xlen) == 64
 
 function clause execute (C_ADDW(rsd, rs2)) = {
-  let rsd = creg2reg_bits(rsd);
-  let rs2 = creg2reg_bits(rs2);
+  let rsd = creg2reg_idx(rsd);
+  let rs2 = creg2reg_idx(rs2);
   execute(RTYPEW(rs2, rsd, rsd, RISCV_ADDW))
 }
 
@@ -373,35 +373,35 @@ mapping clause assembly = C_J(imm)
   <-> "c.j" ^ spc() ^ hex_bits_11(imm)
 
 /* ****************************************************************** */
-union clause ast = C_BEQZ : (bits(8), cregbits)
+union clause ast = C_BEQZ : (bits(8), cregidx)
 
 mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregbits @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
 
 function clause execute (C_BEQZ(imm, rs)) =
-  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_bits(rs), RISCV_BEQ))
+  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ))
 
 mapping clause assembly = C_BEQZ(imm, rs)
   <-> "c.beqz" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm)
 
 /* ****************************************************************** */
-union clause ast = C_BNEZ : (bits(8), cregbits)
+union clause ast = C_BNEZ : (bits(8), cregidx)
 
 mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregbits @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
 
 function clause execute (C_BNEZ(imm, rs)) =
-  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_bits(rs), RISCV_BNE))
+  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE))
 
 mapping clause assembly = C_BNEZ(imm, rs)
   <-> "c.bnez" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm)
 
 /* ****************************************************************** */
-union clause ast = C_SLLI : (bits(6), regbits)
+union clause ast = C_SLLI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
       if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
-  <-> 0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10
+  <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10
       if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
 
 function clause execute (C_SLLI(shamt, rsd)) =
@@ -413,11 +413,11 @@ mapping clause assembly = C_SLLI(shamt, rsd)
       if shamt != 0b000000 & rsd != zreg
 
 /* ****************************************************************** */
-union clause ast = C_LWSP : (bits(6), regbits)
+union clause ast = C_LWSP : (bits(6), regidx)
 
 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
+  <-> 0b010 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
       if rd != zreg
 
 function clause execute (C_LWSP(uimm, rd)) = {
@@ -431,11 +431,11 @@ mapping clause assembly = C_LWSP(uimm, rd)
       if rd != zreg
 
 /* ****************************************************************** */
-union clause ast = C_LDSP : (bits(6), regbits)
+union clause ast = C_LDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd)
       if rd != zreg & sizeof(xlen) == 64
-  <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
+  <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
       if rd != zreg & sizeof(xlen) == 64
 
 function clause execute (C_LDSP(uimm, rd)) = {
@@ -449,10 +449,10 @@ mapping clause assembly = C_LDSP(uimm, rd)
       if rd != zreg & sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_SWSP : (bits(6), regbits)
+union clause ast = C_SWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2)
-  <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regbits @ 0b10
+  <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
 
 function clause execute (C_SWSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -463,11 +463,11 @@ mapping clause assembly = C_SWSP(uimm, rd)
   <-> "c.swsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
 
 /* ****************************************************************** */
-union clause ast = C_SDSP : (bits(6), regbits)
+union clause ast = C_SDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2)
       if sizeof(xlen) == 64
-  <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10
+  <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
       if sizeof(xlen) == 64
 
 function clause execute (C_SDSP(uimm, rs2)) = {
@@ -481,11 +481,11 @@ mapping clause assembly = C_SDSP(uimm, rs2)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = C_JR : (regbits)
+union clause ast = C_JR : (regidx)
 
 mapping clause encdec_compressed = C_JR(rs1)
       if rs1 != zreg
-  <-> 0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10
+  <-> 0b100 @ 0b0 @ rs1 : regidx @ 0b00000 @ 0b10
       if rs1 != zreg
 
 function clause execute (C_JR(rs1)) =
@@ -497,11 +497,11 @@ mapping clause assembly = C_JR(rs1)
       if rs1 != zreg
 
 /* ****************************************************************** */
-union clause ast = C_JALR : (regbits)
+union clause ast = C_JALR : (regidx)
 
 mapping clause encdec_compressed = C_JALR(rs1)
       if rs1 != zreg
-  <-> 0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10
+  <-> 0b100 @ 0b1 @ rs1 : regidx @ 0b00000 @ 0b10
       if rs1 != zreg
 
 function clause execute (C_JALR(rs1)) =
@@ -513,11 +513,11 @@ mapping clause assembly = C_JALR(rs1)
       if rs1 != zreg
 
 /* ****************************************************************** */
-union clause ast = C_MV : (regbits, regbits)
+union clause ast = C_MV : (regidx, regidx)
 
 mapping clause encdec_compressed = C_MV(rd, rs2)
       if rd != zreg & rs2 != zreg
-  <-> 0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10
+  <-> 0b100 @ 0b0 @ rd : regidx @ rs2 : regidx @ 0b10
       if rd != zreg & rs2 != zreg
 
 function clause execute (C_MV(rd, rs2)) =
@@ -540,11 +540,11 @@ function clause execute C_EBREAK() =
 mapping clause assembly = C_EBREAK() <-> "c.ebreak"
 
 /* ****************************************************************** */
-union clause ast = C_ADD : (regbits, regbits)
+union clause ast = C_ADD : (regidx, regidx)
 
 mapping clause encdec_compressed = C_ADD(rsd, rs2)
       if rsd != zreg & rs2 != zreg
-  <-> 0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10
+  <-> 0b100 @ 0b1 @ rsd : regidx @ rs2 : regidx @ 0b10
       if rsd != zreg & rs2 != zreg
 
 function clause execute (C_ADD(rsd, rs2)) =
diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail
index 1744648..49d1e5d 100644
--- a/model/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
@@ -6,7 +6,7 @@ union clause ast = ILLEGAL : word
 
 mapping clause encdec = ILLEGAL(s) <-> s
 
-function clause execute (ILLEGAL(s)) = { handle_illegal(); false }
+function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL }
 
 mapping clause assembly = ILLEGAL(s) <-> "illegal" ^ spc() ^ hex_bits_32(s)
 
@@ -16,7 +16,7 @@ union clause ast = C_ILLEGAL : half
 
 mapping clause encdec_compressed = C_ILLEGAL(s) <-> s
 
-function clause execute C_ILLEGAL(s) = { handle_illegal(); false }
+function clause execute C_ILLEGAL(s) = { handle_illegal(); RETIRE_FAIL }
 
 mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 
@@ -28,7 +28,7 @@ mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 
 function clause ext_execute (_) = {
   handle_illegal();
-  false
+  RETIRE_FAIL
 }
 
 /* End definitions */
diff --git a/model/riscv_insts_helpers.sail b/model/riscv_insts_helpers.sail
index acd103f..ef229f3 100644
--- a/model/riscv_insts_helpers.sail
+++ b/model/riscv_insts_helpers.sail
@@ -8,11 +8,11 @@ function extend_value(is_unsigned, value) = match (value) {
   MemException(e) => MemException(e)
 }
 
-val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
+val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
 function process_load(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
-    MemValue(result) => { X(rd) = result; true },
-    MemException(e)  => { handle_mem_exception(addr, e); false }
+    MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },
+    MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
   }
 
 function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
@@ -29,9 +29,9 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
  * sequential model of SC a bit simpler, at the cost of an explicit
  * call to load_reservation in LR and cancel_reservation in SC.
  */
-val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
+val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
 function process_loadres(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
-    MemValue(result) => { load_reservation(addr); X(rd) = result; true },
-    MemException(e)  => { handle_mem_exception(addr, e); false }
+    MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS },
+    MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
   }
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index b133ac2..4830f93 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -3,7 +3,7 @@
 
 /* ****************************************************************** */
 
-union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
+union clause ast = MUL : (regidx, regidx, regidx, bool, bool, bool)
 
 mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
   (false, true, true)  <-> 0b000,
@@ -27,10 +27,10 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
                  then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
                  else result_wide[(sizeof(xlen) - 1) .. 0];
     X(rd) = result;
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -45,7 +45,7 @@ mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2)
   <-> mul_mnemonic(high, signed1, signed2) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = DIV : (regbits, regbits, regbits, bool)
+union clause ast = DIV : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = DIV(rs2, rs1, rd, s)
   <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011
@@ -60,10 +60,10 @@ function clause execute (DIV(rs2, rs1, rd, s)) = {
     /* check for signed overflow */
     let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
     X(rd) = to_bits(sizeof(xlen), q');
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -76,7 +76,7 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
   <-> "div" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = REM : (regbits, regbits, regbits, bool)
+union clause ast = REM : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = REM(rs2, rs1, rd, s)
   <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011
@@ -90,10 +90,10 @@ function clause execute (REM(rs2, rs1, rd, s)) = {
     let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
     /* signed overflow case returns zero naturally as required due to -1 divisor */
     X(rd) = to_bits(sizeof(xlen), r);
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -101,7 +101,7 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
   <-> "rem" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
-union clause ast = MULW : (regbits, regbits, regbits)
+union clause ast = MULW : (regidx, regidx, regidx)
 
 mapping clause encdec = MULW(rs2, rs1, rd)
       if sizeof(xlen) == 64
@@ -118,10 +118,10 @@ function clause execute (MULW(rs2, rs1, rd)) = {
     let result32 = to_bits(64, rs1_int * rs2_int)[31..0];
     let result : xlenbits = EXTS(result32);
     X(rd) = result;
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -131,7 +131,7 @@ mapping clause assembly = MULW(rs2, rs1, rd)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = DIVW : (regbits, regbits, regbits, bool)
+union clause ast = DIVW : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = DIVW(rs2, rs1, rd, s)
       if sizeof(xlen) == 64
@@ -148,10 +148,10 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = {
     /* check for signed overflow */
     let q': int = if s & q > (2 ^ 31 - 1) then  (0 - 2^31) else q;
     X(rd) = EXTS(to_bits(32, q'));
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
@@ -161,7 +161,7 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
-union clause ast = REMW : (regbits, regbits, regbits, bool)
+union clause ast = REMW : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = REMW(rs2, rs1, rd, s)
       if sizeof(xlen) == 64
@@ -177,10 +177,10 @@ function clause execute (REMW(rs2, rs1, rd, s)) = {
     let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
     /* signed overflow case returns zero naturally as required due to -1 divisor */
     X(rd) = EXTS(to_bits(32, r));
-    true
+    RETIRE_SUCCESS
   } else {
     handle_illegal();
-    false
+    RETIRE_FAIL
   }
 }
 
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
index 7b87826..2af2eeb 100644
--- a/model/riscv_insts_next.sail
+++ b/model/riscv_insts_next.sail
@@ -10,7 +10,7 @@ function clause execute URET() = {
   if   (~ (haveUsrMode()))
   then handle_illegal()
   else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
-  false
+  RETIRE_FAIL
 }
 
 mapping clause assembly = URET() <-> "uret"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 569bc19..ccbc030 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -2,7 +2,7 @@
 /* This file specifies the instructions in the 'Zicsr' extension.     */
 
 /* ****************************************************************** */
-union clause ast = CSR  : (bits(12), regbits, regbits, bool, csrop)
+union clause ast = CSR  : (bits(12), regidx, regidx, bool, csrop)
 
 mapping encdec_csrop : csrop <-> bits(2) = {
   CSRRW <-> 0b01,
@@ -141,7 +141,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
     _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
   };
   if ~ (check_CSR(csr, cur_privilege, isWrite))
-  then { handle_illegal(); false }
+  then { handle_illegal(); RETIRE_FAIL }
   else {
     let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
     if isWrite then {
@@ -153,7 +153,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
       writeCSR(csr, new_val)
     };
     X(rd) = csr_val;
-    true
+    RETIRE_SUCCESS
   }
 }
 
diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail
index 8a7d8f4..58369bf 100644
--- a/model/riscv_jalr_rmem.sail
+++ b/model/riscv_jalr_rmem.sail
@@ -6,5 +6,5 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
   X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
   let newPC : xlenbits = X(rs1) + EXTS(imm);
   nextPC = [newPC with 0 = bitzero];  /* Clear newPC[0] */
-  true
+  RETIRE_SUCCESS
 }
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index f410459..5b37c78 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -12,18 +12,18 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
   match ext_control_check_addr(t) {
     Ext_ControlAddr_Error(e) => {
       ext_handle_control_check_error(e);
-      false
+      RETIRE_FAIL
     },
     Ext_ControlAddr_OK(addr) => {
       let  target = [addr with 0 = bitzero];  /* clear addr[0] */
       if   target[1] & (~ (haveRVC()))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align);
-        false
+        RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();
         set_next_pc(target);
-        true
+        RETIRE_SUCCESS
       }
     }
   }
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index f866fab..b92f234 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -142,7 +142,7 @@ overload X = {rX, wX}
 
 /* register names */
 
-val cast reg_name_abi : regbits -> string
+val cast reg_name_abi : regidx -> string
 
 function reg_name_abi(r) = {
   match (r) {
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index c6b7fc1..4b5c1c5 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -7,12 +7,12 @@ function step(step_no) = {
   ext_pre_step_hook();
 
   minstret_written = false;     /* see note for minstret */
-  let (retired, stepped) : (bool, bool) =
+  let (retired, stepped) : (Retired, bool) =
     match dispatchInterrupt(cur_privilege) {
       Some(intr, priv) => {
         print_bits("Handling interrupt: ", intr);
         handle_interrupt(intr, priv);
-        (false, false)
+        (RETIRE_FAIL, false)
       },
       None() => {
         /* the extension hook interposes on the fetch result */
@@ -21,12 +21,12 @@ function step(step_no) = {
           /* extension error */
           F_Ext_Error(e)   => {
             ext_handle_fetch_check_error(e);
-            (false, false)
+            (RETIRE_FAIL, false)
           },
           /* standard error */
           F_Error(e, addr) => {
             handle_mem_exception(addr, e);
-            (false, false)
+            (RETIRE_FAIL, false)
           },
           /* non-error cases: */
           F_RVC(h) => {
@@ -38,7 +38,7 @@ function step(step_no) = {
               (execute(ext_post_decode_hook(ast)), true)
              } else {
               handle_illegal();
-              (false, true)
+              (RETIRE_FAIL, true)
              }
           },
           F_Base(w) => {
@@ -50,8 +50,14 @@ function step(step_no) = {
         }
       }
     };
+
   tick_pc();
-  if retired then retire_instruction();
+
+  /* update minstret */
+  match retired {
+    RETIRE_SUCCESS => retire_instruction(),
+    RETIRE_FAIL    => ()
+  };
 
   /* for step extensions */
   ext_post_step_hook();
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index fa88da9..1cb595e 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -14,25 +14,25 @@ type word = bits(32)
 
 /* register identifiers */
 
-type regbits  = bits(5)
-type cregbits = bits(3)    /* identifiers in RVC instructions */
-type csreg    = bits(12)   /* CSR addressing */
+type regidx  = bits(5)
+type cregidx = bits(3)    /* identifiers in RVC instructions */
+type csreg   = bits(12)   /* CSR addressing */
 
 /* register file indexing */
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 
-val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
-function regbits_to_regno b = let 'r = unsigned(b) in r
+val cast regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regidx_to_regno b = let 'r = unsigned(b) in r
 
 /* mapping RVC register indices into normal indices */
-val creg2reg_bits : cregbits -> regbits
-function creg2reg_bits(creg) = 0b01 @ creg
+val creg2reg_idx : cregidx -> regidx
+function creg2reg_idx(creg) = 0b01 @ creg
 
 /* some architecture and ABI relevant register identifiers */
-let zreg : regbits = 0b00000  /* x0, zero register  */
-let ra   : regbits = 0b00001  /* x1, return address */
-let sp   : regbits = 0b00010  /* x2, stack pointer  */
+let zreg : regidx = 0b00000  /* x0, zero register  */
+let ra   : regidx = 0b00001  /* x1, return address */
+let sp   : regidx = 0b00010  /* x2, stack pointer  */
 
 /* instruction fields */
 
@@ -89,6 +89,10 @@ function privLevel_to_str (p) =
     Machine    => "M"
   }
 
+/* enum denoting whether an executed instruction retires */
+
+enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
+
 /* memory access types */
 
 enum AccessType = {Read, Write, ReadWrite, Execute}