Add register checks

rvfi/checks/reg_check.py

@@ -0,0 +1,62 @@
+from nmigen import *
+from nmigen.asserts import *
+
+"""
+Register Check
+"""
+
+class RegCheck(Elaboratable):
+    def __init__(self, RISCV_FORMAL_XLEN):
+        # Core-specific constants
+        self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
+
+        # Input ports
+        self.reset = Signal(1)
+        self.check = Signal(1)
+        self.rvfi_valid = Signal(1)
+        self.rvfi_order = Signal(64)
+        self.rvfi_rs1_addr = Signal(5)
+        self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_rs2_addr = Signal(5)
+        self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_rd_addr = Signal(5)
+        self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
+    def ports(self):
+        input_ports = [
+            self.reset,
+            self.check,
+            self.rvfi_valid,
+            self.rvfi_order,
+            self.rvfi_rs1_addr,
+            self.rvfi_rs1_rdata,
+            self.rvfi_rs2_addr,
+            self.rvfi_rs2_rdata,
+            self.rvfi_rd_addr,
+            self.rvfi_rd_wdata
+        ]
+        return input_ports
+    def elaborate(self, platform):
+        m = Module()
+
+        insn_order = AnyConst(64)
+        register_index = AnyConst(5)
+        register_shadow = Signal(self.RISCV_FORMAL_XLEN, reset=0)
+        register_written = Signal(1, reset=0)
+
+        with m.If(self.reset):
+            m.d.sync += register_shadow.eq(0)
+            m.d.sync += register_written.eq(0)
+        with m.Else():
+            with m.If(self.check):
+                m.d.comb += Assume(self.rvfi_valid)
+                m.d.comb += Assume(insn_order == self.rvfi_order)
+                with m.If(register_written & (register_index == self.rvfi_rs1_addr)):
+                    m.d.comb += Assert(register_shadow == self.rvfi_rs1_rdata)
+                with m.If(register_written & (register_index == self.rvfi_rs2_addr)):
+                    m.d.comb += Assert(register_shadow == self.rvfi_rs2_rdata)
+            with m.Else():
+                with m.If(self.rvfi_valid & (self.rvfi_order < insn_order) & (register_index == self.rvfi_rd_addr)):
+                    m.d.sync += register_shadow.eq(self.rvfi_rd_wdata)
+                    m.d.sync += register_written.eq(1)
+
+        return m

rvfi/cores/minerva/test/test_register.py

@@ -0,0 +1,28 @@
+from nmigen import *
+from ..core import *
+from nmigen.test.utils import *
+from ....checks.reg_check import *
+
+class RegSpec(Elaboratable):
+    def elaborate(self, platform):
+        m = Module()
+
+        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
+        m.submodules.reg_spec = reg_spec = RegCheck(RISCV_FORMAL_XLEN=32)
+
+        m.d.comb += reg_spec.reset.eq(0)
+        m.d.comb += reg_spec.check.eq(1)
+        m.d.comb += reg_spec.rvfi_valid.eq(cpu.rvfi.valid)
+        m.d.comb += reg_spec.rvfi_order.eq(cpu.rvfi.order)
+        m.d.comb += reg_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
+        m.d.comb += reg_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
+        m.d.comb += reg_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
+        m.d.comb += reg_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
+        m.d.comb += reg_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
+        m.d.comb += reg_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)
+
+        return m
+
+class RegTestCase(FHDLTestCase):
+    def verify(self):
+        self.assertFormal(RegSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

rvfi/cores/minerva/verify.py

@@ -3,6 +3,7 @@ from .test.test_cache import *
 from .test.test_instructions import *
 from .test.test_pc_forward import *
 from .test.test_pc_backward import *
+from .test.test_register import *
 from .test.test_units_divider import *
 from .test.test_units_multiplier import *
 
@@ -56,5 +57,8 @@ PcFwdTestCase().verify()
 print("Verifying PC backward checks ...")
 PcBwdTestCase().verify()
 
+print("Verifying register checks ...")
+RegTestCase().verify()
+
 print("Testing multiplier and divider ...")
 unittest.main()