Improve store-conditional speculative failures and exception priority

1. Move `speculate_conditional()` to the same place as `match_reservation()`. I am not 100% sure about this change because I'm not sure what rmem is (and it has a comment about allowing it to fail very early), but it doesn't make sense to me that SC could spuriously fail in a place where it shouldn't be allowed in the sequential model.

Codasip uses `speculate_conditional()` to force spurious SC failures into the model (so it matches the DUT), and this is the right place for that use.

2. Do an explicit access check before checking the reservation. Without this you never get an access fault for accesses to memory that doesn't exist or doesn't support LR/SC.

3. Move `cancel_reservation()` to the end of the function. This doesn't change any functionality, I think it's just clearer and makes it obvious that the omission of `cancel_reservation()` in the `MemException(e)` branch was not a mistake.

model/riscv_insts_aext.sail

@@ -115,52 +115,58 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   // This is checked during decoding.
   assert(width_bytes <= xlen_bytes);
 
-  if speculate_conditional () == false then {
-    /* should only happen in rmem
-     * rmem: allow SC to fail very early
-     */
-    X(rd) = zero_extend(0b1); RETIRE_SUCCESS
-  } else {
-    /* normal non-rmem case
-      * rmem: SC is allowed to succeed (but might fail later)
-      */
-    /* Get the address, X(rs1) (no offset).
-      * Extensions might perform additional checks on address validity.
-      */
-    match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
-      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
-      Ext_DataAddr_OK(vaddr) => {
-        if not(is_aligned(virtaddr_bits(vaddr), width))
-        then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
-        else {
-          match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
-                                                      * both result in a SAMO exception */
-            TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-            TR_Address(addr, _) => {
-              // Check reservation with physical address.
-              if not(match_reservation(physaddr_bits(addr))) then {
-                /* cannot happen in rmem */
-                X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
-              } else {
-                let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
-                match eares {
-                  MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-                  MemValue(_) => {
-                    let rs2_val = X(rs2);
-                    match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
-                      MemValue(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
-                      MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
-                      MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+  /* Get the address, X(rs1) (no offset).
+    * Extensions might perform additional checks on address validity.
+    */
+  let res : Retired = match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) => {
+      if not(is_aligned(virtaddr_bits(vaddr), width))
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else {
+        match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
+                                                    * both result in a SAMO exception */
+          TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+          TR_Address(addr, _) => {
+            // Explicitly do access checks first in case the memory does
+            // not exist or doesn't support LR/SC. Without this check we
+            // may get a spurious failure (see below) for LR/SC to memory
+            // that should cause an access fault.
+            let typ = Write(default_write_acc);
+            let priv = effectivePrivilege(typ, mstatus, cur_privilege);
+            match phys_access_check(typ, priv, pbmt, addr, width_bytes, true) {
+              Some(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+              None() => {
+                if not(speculate_conditional()) | not(match_reservation(physaddr_bits(addr))) then {
+                  // Spurious failure (this is allowed), or the reservation
+                  // address does not match.
+                  X(rd) = zero_extend(0b1); RETIRE_SUCCESS
+                } else {
+                  match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
+                    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                    MemValue(_) => {
+                      let rs2_val = X(rs2);
+                      match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
+                        MemValue(true)  => { X(rd) = zero_extend(0b0); RETIRE_SUCCESS },
+                        MemValue(false) => { X(rd) = zero_extend(0b1); RETIRE_SUCCESS },
+                        MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                      }
                     }
                   }
                 }
-              }
+              },
             }
           }
         }
       }
     }
-  }
+  };
+  // The spec says "Regardless of success or failure, executing an SC
+  // instruction invalidates any reservation held by this hart", however
+  // "failure" here does not include failure due to exceptions.
+  // See https://github.com/riscv/riscv-isa-manual/issues/1010
+  if res == RETIRE_SUCCESS then cancel_reservation();
+  res
 }
 
 mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)