Add non-rvfi upcnt

Currently limited to checking low half, but seems to work.
Support global code (useful for doing things like `if (condition) assume(condition);` that would otherwise make for a messy `assume(condition)` without the `if`.

Author: KrystalDelusion

src/csrs/behavior.py

@@ -18,6 +18,9 @@ def regs(self, csr_width: str, csr_has_rvfi: bool) -> NamedSet[BehavioralReg]: p
     def global_assumptions(self) -> list[str]:
         return []
 
+    def global_code(self, csr_has_rvfi: bool) -> Optional[str]:
+        return None
+
     @property
     def check_assumptions(self) -> list[str]:
         return []
@@ -66,7 +69,7 @@ def check_assumptions(self) -> list[str]:
 
     @property
     def check_condition(self) -> str:
-        return "csr_written && csr_read_valid && csr_insn_under_test"
+        return "csr_read_valid && csr_insn_under_test"
 
     def check(self, csr_has_rvfi: bool) -> str:
         if csr_has_rvfi:
@@ -84,7 +87,6 @@ def check(self, csr_has_rvfi: bool) -> str:
         else:
             return dedent("""
                 assume(csr_mode_shadow <= 2'b 01);
-                assume(rvfi.rd_addr != 0);
                 case (csr_mode_shadow)
                     2'b 00 /* None */,
                     2'b 01 /* RW   */: begin
@@ -101,13 +103,17 @@ def assign_condition(self) -> str:
 
 class UpcntValue(Behavior):
     def regs(self, csr_width: str, csr_has_rvfi: bool) -> NamedSet[BehavioralReg]:
-        regs = NamedSet([
-            BehavioralReg("csr_read_shadowed", "1", "1"),
-        ])
         if csr_has_rvfi:
-            regs.add(BehavioralReg("rdata_shadow", csr_width, "csr_insn_rdata"))
+            regs = NamedSet([
+                BehavioralReg("csr_read_lo", "1", "1"),
+                BehavioralReg("rdata_shadow", csr_width, "csr_insn_rdata"),
+            ])
         else:
-            regs.add(BehavioralReg("rdata_shadow", csr_width, "rvfi.rd_wdata"))
+            regs = NamedSet([
+                BehavioralReg("csr_read_hi", "1", "csr_hi"),
+                BehavioralReg("csr_read_lo", "1", "csr_lo"),
+                BehavioralReg("rdata_shadow", csr_width, "rvfi.rd_wdata"),
+            ])
         return regs
 
     @property
@@ -116,7 +122,7 @@ def global_assumptions(self) -> list[str]:
 
     @property
     def check_assumptions(self) -> list[str]:
-        return ["csr_read_shadowed"]
+        return ["csr_read_lo"]
 
     @property
     def check_condition(self) -> str:
@@ -128,7 +134,9 @@ def check(self, csr_has_rvfi: bool) -> str:
                 assert(csr_insn_rdata > rdata_shadow);""")
         else:
             return dedent("""
-                assume(0);""")
+                // currently only tests low half when not using rvfi signal
+                assume(csr_lo);
+                assert(rvfi.rd_wdata > rdata_shadow[31:0]);""")
 
     @property
     def assign_assumptions(self) -> list[str]:

src/csrs/csr.py

@@ -107,7 +107,11 @@ def _v_process(self, xlen: int) -> str:
             reset = f"{reg.name} = {reg.default_value};"
             v_str += f"reg {reg.bitrange()} {reset}\n"
             resets.append(reset)
-            assigns.append(f"{reg.name} = {reg.spec_value};")
+            if not self.has_rvfi and reg_width == "64" and reg.spec_value == "rvfi.rd_wdata":
+                assigns.append(f"if (csr_hi) {reg.name}[63:32] = {reg.spec_value};")
+                assigns.append(f"if (csr_lo) {reg.name}[31: 0] = {reg.spec_value};")
+            else:
+                assigns.append(f"{reg.name} = {reg.spec_value};")
         reset_str = "\n                    ".join(resets)
         assign_str = "\n                            ".join(assigns)
 
@@ -125,6 +129,10 @@ def _v_process(self, xlen: int) -> str:
 
         check_str = indent(self.behavior.check(self.has_rvfi), "                            ")
 
+        global_code = self.behavior.global_code(self.has_rvfi)
+        if global_code:
+            global_assumes_str += "\n" + indent(global_code, "                    ")
+
         v_str += dedent(f"""
             // test
             always @(posedge clock) begin