Merge Retire_Failure into ExecutionResult

There's really no reason to have two levels of unions here so I added `Retire_Success` into `Retire_Failure` and then used that directly as `ExecutionResult`. This is definitely simpler and it also removes the weird case of WFI which was included in `Retire_Failure` when it isn't really failing to retire (especially if `wfi_is_nop()` is true).

I left the `RETIRE_SUCCESS` to make the commit smaller, but it does mean there is some stylistic inconsistency. We can fix that with a simple search and replace in future.

Author: Timmmm

README.md

@@ -181,7 +181,8 @@ mapping clause assembly = ITYPE(imm, rs1, rd, op)
 ```
 union clause ast = SRET : unit
 
-mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
+mapping clause encdec = SRET()
+  <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SRET() = {
   let sret_illegal : bool = match cur_privilege {
@@ -190,9 +191,9 @@ function clause execute SRET() = {
     Machine    => not(currentlyEnabled(Ext_S))
   };
   if   sret_illegal
-  then { handle_illegal(); RETIRE_FAIL }
+  then Illegal_Instruction()
   else if not(ext_check_xret_priv (Supervisor))
-  then { ext_fail_xret_priv(); RETIRE_FAIL }
+  then Ext_XRET_Priv_Failure()
   else {
     set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
     RETIRE_SUCCESS

model/CMakeLists.txt

@@ -176,13 +176,13 @@ foreach (xlen IN ITEMS 32 64)
                 "riscv_vmem_types.sail"
                 ${sail_regs_srcs}
                 ${sail_sys_srcs}
+                "riscv_inst_retire.sail"
                 "riscv_platform.sail"
                 "riscv_mem.sail"
                 ${sail_vm_srcs}
                 # Shared/common code for the cryptography extension.
                 "riscv_types_kext.sail"
                 "riscv_zvk_utils.sail"
-                "riscv_inst_retire.sail"
             )
 
             if (variant STREQUAL "rvfi")

model/riscv_inst_retire.sail

@@ -6,16 +6,21 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-/* Reasons an instruction retire might fail or be incomplete. */
+// Return value from `execute()` function.
+union ExecutionResult = {
+  // Successfully retired.
+  Retire_Success                 : unit,
 
-union Retire_Failure = {
-  // standard reasons
-  Illegal_Instruction            : unit,
+  // WFI executed, which may or may not retire
+  // depending on the configuration.
   Wait_For_Interrupt             : unit,
+
+  // Did not retire for a standard reason.
+  Illegal_Instruction            : unit,
   Trap                           : (Privilege, ctl_result, xlenbits),
   Memory_Exception               : (virtaddr, ExceptionType),
 
-  // reasons from external extensions
+  // Did not retire for custom reason.
   Ext_CSR_Check_Failure          : unit,
   Ext_ControlAddr_Check_Failure  : ext_control_addr_error,
   Ext_DataAddr_Check_Failure     : ext_data_addr_error,
@@ -27,4 +32,4 @@ union Retire_Failure = {
 // RETIRE_SUCCESS enum value so that we don't have to immediately
 // update all the places RETIRE_SUCCESS was used.
 
-let RETIRE_SUCCESS : ExecutionResult(Retire_Failure) = RETIRE_OK()
+let RETIRE_SUCCESS : ExecutionResult = Retire_Success()

model/riscv_insts_aext.sail

@@ -74,19 +74,19 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
     * Extensions might perform additional checks on address validity.
     */
   match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
+    Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) => {
       /* "LR faults like a normal load, even though it's in the AMO major opcode space."
         * - Andrew Waterman, isa-dev, 10 Jul 2018.
         */
       if not(is_aligned(bits_of(vaddr), width))
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
+      then Memory_Exception(vaddr, E_Load_Addr_Align())
       else match translateAddr(vaddr, Read(Data)) {
-        TR_Failure(e, _)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+        TR_Failure(e, _)    => Memory_Exception(vaddr, e),
         TR_Address(addr, _) =>
           match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
             Ok(result) => { load_reservation(bits_of(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
-            Err(e)     => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+            Err(e)     => Memory_Exception(vaddr, e),
           },
       }
     }
@@ -123,28 +123,28 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       * Extensions might perform additional checks on address validity.
       */
     match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
-      Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
+      Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
       Ext_DataAddr_OK(vaddr) => {
         if not(is_aligned(bits_of(vaddr), width))
-        then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
+        then Memory_Exception(vaddr, E_SAMO_Addr_Align())
         else {
           match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
                                                       * both result in a SAMO exception */
-            TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+            TR_Failure(e, _) => Memory_Exception(vaddr, e),
             TR_Address(addr, _) => {
               // Check reservation with physical address.
               if not(match_reservation(bits_of(addr))) then {
                 /* cannot happen in rmem */
                 X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
               } else {
                 match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
-                  Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+                  Err(e) => Memory_Exception(vaddr, e),
                   Ok(_)  => {
                     let rs2_val = X(rs2);
                     match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
                       Ok(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
                       Ok(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
-                      Err(e)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+                      Err(e)    => Memory_Exception(vaddr, e),
                     }
                   }
                 }
@@ -193,19 +193,19 @@ 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(), ReadWrite(Data, Data), width_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
+    Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) => {
       if not(is_aligned(bits_of(vaddr), width))
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
+      then Memory_Exception(vaddr, E_SAMO_Addr_Align())
       else match translateAddr(vaddr, ReadWrite(Data, Data)) {
-        TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+        TR_Failure(e, _) => Memory_Exception(vaddr, e),
         TR_Address(addr, _) => {
           let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
           match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
-            Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+            Err(e) => Memory_Exception(vaddr, e),
             Ok(_) => {
               match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
-                Err(e)     => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+                Err(e)     => Memory_Exception(vaddr, e),
                 Ok(loaded) => {
                   let result : bits('width_bytes * 8) =
                     match op {
@@ -222,7 +222,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) {
                     Ok(true)  => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS },
                     Ok(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
-                    Err(e)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+                    Err(e)    => Memory_Exception(vaddr, e),
                   }
                 }
               }

model/riscv_insts_base.sail

@@ -62,12 +62,12 @@ function clause execute (JAL(imm, rd)) = {
   let target = PC + sign_extend(imm);
   /* Extensions get the first checks on the prospective target address. */
   match ext_control_check_pc(target) {
-    Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)),
+    Ext_ControlAddr_Error(e) => Ext_ControlAddr_Check_Failure(e),
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
       let target_bits = bits_of(target);
       if bit_to_bool(target_bits[1]) & not(currentlyEnabled(Ext_Zca)) then {
-        RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align()))
+        Memory_Exception(target, E_Fetch_Addr_Align())
       } else {
         X(rd) = get_next_pc();
         set_next_pc(target_bits);
@@ -121,11 +121,11 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
     let target = PC + sign_extend(imm);
     /* Extensions get the first checks on the prospective target address. */
     match ext_control_check_pc(target) {
-      Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)),
+      Ext_ControlAddr_Error(e) => Ext_ControlAddr_Check_Failure(e),
       Ext_ControlAddr_OK(target) => {
         let target_bits = bits_of(target);
         if bit_to_bool(target_bits[1]) & not(currentlyEnabled(Ext_Zca)) then {
-          RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align()))
+          Memory_Exception(target, E_Fetch_Addr_Align())
         } else {
           set_next_pc(target_bits);
           RETIRE_SUCCESS
@@ -305,16 +305,16 @@ 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_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
+    Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) => {
       if   check_misaligned(vaddr, width)
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
+      then Memory_Exception(vaddr, E_Load_Addr_Align())
       else match translateAddr(vaddr, Read(Data)) {
-        TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+        TR_Failure(e, _) => Memory_Exception(vaddr, e),
         TR_Address(paddr, _) =>
           match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
             Ok(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
-            Err(e)     => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+            Err(e)     => Memory_Exception(vaddr, e),
           },
       }
     },
@@ -361,21 +361,21 @@ 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_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
+    Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
+      then Memory_Exception(vaddr, E_SAMO_Addr_Align())
       else match translateAddr(vaddr, Write(Data)) {
-        TR_Failure(e, _)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+        TR_Failure(e, _)    => Memory_Exception(vaddr, e),
         TR_Address(paddr, _) => {
           match mem_write_ea(paddr, width_bytes, aq, rl, false) {
-            Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
+            Err(e) => Memory_Exception(vaddr, e),
             Ok(_)  => {
               let rs2_val = X(rs2);
               match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) {
                 Ok(true)  => RETIRE_SUCCESS,
                 Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                Err(e)    => RETIRE_FAIL(Memory_Exception(vaddr, e))
+                Err(e)    => Memory_Exception(vaddr, e)
               }
             }
           }
@@ -584,7 +584,7 @@ function clause execute ECALL() = {
                     },
              excinfo = (None() : option(xlenbits)),
              ext     = None() };
-  RETIRE_FAIL(Trap(cur_privilege, CTL_TRAP(t), PC))
+  Trap(cur_privilege, CTL_TRAP(t), PC)
 }
 
 mapping clause assembly = ECALL() <-> "ecall"
@@ -597,9 +597,9 @@ mapping clause encdec = MRET()
 
 function clause execute MRET() = {
   if   cur_privilege != Machine
-  then RETIRE_FAIL(Illegal_Instruction())
+  then Illegal_Instruction()
   else if not(ext_check_xret_priv(Machine))
-  then RETIRE_FAIL(Ext_XRET_Priv_Failure())
+  then Ext_XRET_Priv_Failure()
   else {
     set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC));
     RETIRE_SUCCESS
@@ -621,9 +621,9 @@ function clause execute SRET() = {
     Machine    => not(currentlyEnabled(Ext_S))
   };
   if   sret_illegal
-  then RETIRE_FAIL(Illegal_Instruction())
+  then Illegal_Instruction()
   else if not(ext_check_xret_priv (Supervisor))
-  then RETIRE_FAIL(Ext_XRET_Priv_Failure())
+  then Ext_XRET_Priv_Failure()
   else {
     set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
     RETIRE_SUCCESS
@@ -639,7 +639,7 @@ mapping clause encdec = EBREAK()
   <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute EBREAK() =
-  RETIRE_FAIL(Memory_Exception(Virtaddr(PC), E_Breakpoint()))
+  Memory_Exception(Virtaddr(PC), E_Breakpoint())
 
 mapping clause assembly = EBREAK() <-> "ebreak"
 
@@ -651,11 +651,11 @@ mapping clause encdec = WFI()
 
 function clause execute WFI() =
   match cur_privilege {
-    Machine    => RETIRE_FAIL(Wait_For_Interrupt()),
+    Machine    => Wait_For_Interrupt(),
     Supervisor => if   mstatus[TW] == 0b1
-                  then RETIRE_FAIL(Illegal_Instruction())
-                  else RETIRE_FAIL(Wait_For_Interrupt()),
-    User       => RETIRE_FAIL(Illegal_Instruction())
+                  then Illegal_Instruction()
+                  else Wait_For_Interrupt(),
+    User       => Illegal_Instruction()
   }
 
 mapping clause assembly = WFI() <-> "wfi"
@@ -673,9 +673,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
   // is 9 but we always set it to 16 for RV64.
   let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None();
   match cur_privilege {
-    User       => RETIRE_FAIL(Illegal_Instruction()),
+    User       => Illegal_Instruction(),
     Supervisor => match mstatus[TVM] {
-                    0b1 => RETIRE_FAIL(Illegal_Instruction()),
+                    0b1 => Illegal_Instruction(),
                     0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS },
                   },
     Machine    => { flush_TLB(asid, addr); RETIRE_SUCCESS }

model/riscv_insts_begin.sail

@@ -14,7 +14,7 @@
 scattered union ast
 
 /* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> ExecutionResult(Retire_Failure)
+val execute : ast -> ExecutionResult
 scattered function execute
 
 val assembly : ast <-> string