resolve error in NAPOT match option

riscv · Oct 5, 2024 · 67f737a · 67f737a
1 parent d0c9bb0
commit 67f737a
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
@@ -42,12 +42,16 @@ function step(step_no : int) -> bool = {
           match ext_fetch_hook(fetch()) {
             /* extension error */
             F_Ext_Error(e)   => {
-              ext_handle_fetch_check_error(e);
+              if not(instrDataMatch(cur_privilege, PC, zero_extend(0b0), ANY, INSTR_MATCH)) then {
+                ext_handle_fetch_check_error(e);
+              };
               (RETIRE_FAIL, false)
             },
             /* standard error */
             F_Error(e, addr) => {
-              handle_mem_exception(addr, e);
+              if not(instrDataMatch(cur_privilege, PC, zero_extend(0b0), ANY, INSTR_MATCH)) then {
+                handle_mem_exception(addr, e);
+              };
               (RETIRE_FAIL, false)
             },
             /* non-error cases: */

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
@@ -599,8 +599,8 @@ function instrDataMatch(cur_priv : Privilege, addr : xlenbits, data : xlenbits,
       data_matched = match (matchOpt_of_bits(matchOption)) {
         MOPT_EQUAL => { (tdata2_x.tdata2[i] == tdata2_content) },
         MOPT_NAPOT => {
-          let idx : {'n, (1 <= 'n < xlen). int('n)} = find_first_zero(tdata2_content);
-          tdata2_x.tdata2[i][(xlen - 1) .. (xlen - idx)] == tdata2_content[(xlen - 1) .. (xlen - idx)]
+          let idx : {'n, (1 <= 'n < xlen). int('n)} = find_first_zero(tdata2_x.tdata2[i]);
+          tdata2_x.tdata2[i][(xlen - 1) .. idx] == tdata2_content[(xlen - 1) .. idx]
         },
         MOPT_GE    => { (tdata2_content >=_u tdata2_x.tdata2[i][(xlen - 1) .. 0]) },
         MOPT_LT    => { (tdata2_content <_u  tdata2_x.tdata2[i][(xlen - 1) .. 0]) },
@@ -614,8 +614,8 @@ function instrDataMatch(cur_priv : Privilege, addr : xlenbits, data : xlenbits,
         },
         MOPT_NOT_EQUAL => { (tdata2_x.tdata2[i] != tdata2_content) },
         MOPT_NOT_NAPOT => {
-          let idx : {'n, (1 <= 'n < xlen). int('n)} = find_first_zero(tdata2_content);
-          tdata2_x.tdata2[i][(xlen - 1) .. (xlen - idx)] != tdata2_content[(xlen - 1) .. (xlen - idx)]
+          let idx : {'n, (1 <= 'n < xlen). int('n)} = find_first_zero(tdata2_x.tdata2[i]);
+          tdata2_x.tdata2[i][(xlen - 1) .. idx] != tdata2_content[(xlen - 1) .. idx]
         },
         MOPT_NOT_MASK_LOW => {
           let intemrd_cmpr_val : half_xlenbits = tdata2_content[(half_xlen - 1) .. 0] & tdata2_x.tdata2[i][(xlen - 1) .. half_xlen];