Fix minstret off-by-one when mcountinhibit is set

This fixes a small bug in `mcounthinhibit`. In the current code if you set `mcountinhibit=1` then it inhibits the count of that CSR write, whereas the spec says that it should only apply to future instructions:

> Any CSR write takes effect after the writing instruction has otherwise completed.

- From the priviledged spec, section 3.1.10 Hardware Performance Monitor.

4 files changed, 18 insertions, 12 deletions

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 08c7a19..5fd0f4f 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -217,9 +217,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
 
     /* machine mode counters */
     (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
-    (0xB02,  _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_written = true; Some(value) },
+    (0xB02,  _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; Some(value) },
     (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) },
-    (0xB82, 32) => { minstret[63 .. 32] = value; minstret_written = true; Some(value) },
+    (0xB82, 32) => { minstret[63 .. 32] = value; minstret_increment = false; Some(value) },
 
     /* trigger/debug */
     (0x7a0,  _) => { tselect = value; Some(tselect) },
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 8d19ebf..a8a3b1e 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -73,7 +73,13 @@ function step(step_no : int) -> bool = {
   /* for step extensions */
   ext_pre_step_hook();
 
-  minstret_written = false;     /* see note for minstret */
+  // This records whether or not minstret should be incremented when the
+  // instruction is retired. Since retirement occurs before CSR writes we
+  // initialise it based on mcountinhibit here, before it is potentially
+  // changed. This is also set to false if minstret is written.
+  // See the note near the minstret declaration for more information.
+  minstret_increment = mcountinhibit.IR() == 0b0;
+
   let (retired, stepped) : (Retired, bool) =
     match dispatchInterrupt(cur_privilege) {
       Some(intr, priv) => {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 6681367..6ec39d1 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -594,7 +594,7 @@ function init_sys() -> unit = {
   mcounteren->bits() = EXTZ(0b0);
 
   minstret           = EXTZ(0b0);
-  minstret_written   = false;
+  minstret_increment = true;
 
   init_pmp();
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 3ee24a4..aed6eac 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -490,7 +490,7 @@ register mepc : xlenbits
  * When misa.C is writable, it zeroes only xepc[0].
  */
 function legalize_xepc(v : xlenbits) -> xlenbits =
-  /* allow writing xepc[1] only if misa.C is enabled or could be enabled 
+  /* allow writing xepc[1] only if misa.C is enabled or could be enabled
      XXX specification says this legalization should be done on read */
   if   (sys_enable_writable_misa() & sys_enable_rvc()) | misa.C() == 0b1
   then [v with 0 = bitzero]
@@ -557,17 +557,17 @@ register mtime : bits(64)
  * simulation loop, we need to execute an instruction to find out
  * whether it retired, and hence can only increment instret after
  * execution.  To avoid doing this in the case minstret was explicitly
- * written to, we track writes to it in a separate model-internal
- * register.
+ * written to, we track whether it should increment in a separate
+ * model-internal register.
  */
 register minstret : bits(64)
-register minstret_written : bool
+
+// Should minstret be incremented when the instruction is retired.
+register minstret_increment : bool
 
 function retire_instruction() -> unit = {
-  if   minstret_written == true
-  then minstret_written = false
-  else if mcountinhibit.IR() == 0b0
-       then minstret = minstret + 1
+  if minstret_increment
+    then minstret = minstret + 1;
 }
 
 /* informational registers */