review changes cbo.*

model/riscv_insts_zicbom.sail

@@ -52,47 +52,51 @@ function process_clean_inval(rs1, cbop) = {
   match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) {
     Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) => {
-      let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
-        TR_Address(paddr, _) => {
-          // "A cache-block management instruction is permitted to access the
-          // specified cache block whenever a load instruction or store instruction
-          // is permitted to access the corresponding physical addresses. If
-          // neither a load instruction nor store instruction is permitted to
-          // access the physical addresses, but an instruction fetch is permitted
-          // to access the physical addresses, whether a cache-block management
-          // instruction is permitted to access the cache block is UNSPECIFIED."
-          //
-          // In this implementation we currently don't allow access for fetches.
-          let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size);
-          let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size);
-          match (exc_read, exc_write) {
-            // Access is permitted if read OR write are allowed. If neither
-            // are allowed then we always report a store exception.
-            (Some(exc_read), Some(exc_write)) => Some(exc_write),
-            _ => None(),
+      if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), cacheBlockSize_to_matchSize(cache_block_size_exp), STORE_MATCH))
+      then { RETIRE_FAIL }
+      else {
+        let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
+          TR_Address(paddr, _) => {
+            // "A cache-block management instruction is permitted to access the
+            // specified cache block whenever a load instruction or store instruction
+            // is permitted to access the corresponding physical addresses. If
+            // neither a load instruction nor store instruction is permitted to
+            // access the physical addresses, but an instruction fetch is permitted
+            // to access the physical addresses, whether a cache-block management
+            // instruction is permitted to access the cache block is UNSPECIFIED."
+            //
+            // In this implementation we currently don't allow access for fetches.
+            let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size);
+            let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size);
+            match (exc_read, exc_write) {
+              // Access is permitted if read OR write are allowed. If neither
+              // are allowed then we always report a store exception.
+              (Some(exc_read), Some(exc_write)) => Some(exc_write),
+              _ => None(),
+            }
+          },
+          TR_Failure(e, _) => Some(e)
+        };
+        // "If access to the cache block is not permitted, a cache-block management
+        //  instruction raises a store page fault or store guest-page fault exception
+        //  if address translation does not permit any access or raises a store access
+        //  fault exception otherwise."
+        match res {
+          // The model has no caches so there's no action required.
+          None() => RETIRE_SUCCESS,
+          Some(e) => {
+            let e : ExceptionType = match e {
+              E_Load_Access_Fault() => E_SAMO_Access_Fault(),
+              E_SAMO_Access_Fault() => E_SAMO_Access_Fault(),
+              E_Load_Page_Fault() => E_SAMO_Page_Fault(),
+              E_SAMO_Page_Fault() => E_SAMO_Page_Fault(),
+              // No other exceptions should be generated since we're not checking
+              // for fetch access and it's can't be misaligned.
+              _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"),
+            };
+            handle_mem_exception(vaddr, e);
+            RETIRE_FAIL
           }
-        },
-        TR_Failure(e, _) => Some(e)
-      };
-      // "If access to the cache block is not permitted, a cache-block management
-      //  instruction raises a store page fault or store guest-page fault exception
-      //  if address translation does not permit any access or raises a store access
-      //  fault exception otherwise."
-      match res {
-        // The model has no caches so there's no action required.
-        None() => RETIRE_SUCCESS,
-        Some(e) => {
-          let e : ExceptionType = match e {
-            E_Load_Access_Fault() => E_SAMO_Access_Fault(),
-            E_SAMO_Access_Fault() => E_SAMO_Access_Fault(),
-            E_Load_Page_Fault() => E_SAMO_Page_Fault(),
-            E_SAMO_Page_Fault() => E_SAMO_Page_Fault(),
-            // No other exceptions should be generated since we're not checking
-            // for fetch access and it's can't be misaligned.
-            _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"),
-          };
-          handle_mem_exception(vaddr, e);
-          RETIRE_FAIL
         }
       }
     }

model/riscv_sys_control.sail

@@ -527,7 +527,7 @@ function check_trigger_firing(cur_priv : Privilege) -> bool = {
   var ITrigFired         : bool = false;
   var ETrigFired         : bool = false;
   var MCtrlTrigFired     : bool = false;
-  var fired_trigger_idx  : vector(2, dec, {'n, (0 <= 'n < 7). int('n)}) = [0, 0];
+  var fired_trigger_idx  : vector(2, dec, {'n, (0 <= 'n < N_TRIGGERS). int('n)}) = [0, 0];
   var InstrCount         : InstructionCount  = Mk_InstructionCount(zero_extend(0b0));
   var IEtrigger          : InterruptTrigger  = Mk_InterruptTrigger(zero_extend(0b0));
   var MCtrl6             : MatchControlType6 = Mk_MatchControlType6(zero_extend(0b0));
@@ -657,7 +657,7 @@ function init_sys() -> unit = {
   vtype[vsew]      = 0b000;
   vtype[vlmul]     = 0b000;
 
-  foreach (i from 0 to 6) {
+  foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) {
     tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)] = 0xf;
   };
 

model/riscv_sys_regs.sail

@@ -817,7 +817,6 @@ mapping clause csr_name_map = 0x7a3  <-> "tdata3"
 /*  Legalize TSELECT */
 function legalize_tselect(o : xlenbits, v : xlenbits) -> xlenbits = {
   let t : xlenbits = o;
-  // TODO: Avoid hardcoded value
   if (unsigned(v) <= (sizeof(N_TRIGGERS) - 1)) then { v } else { t }
 }