Add PC backward checks

rvfi/checks/pc_bwd_check.py

@@ -0,0 +1,57 @@
+from nmigen import *
+from nmigen.asserts import *
+
+"""
+PC Backward Check
+"""
+
+class PcBwdCheck(Elaboratable):
+    def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid):
+        # Core-specific constants
+        self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
+
+        # Address validity and equality
+        self.rvformal_addr_valid = rvformal_addr_valid
+        self.rvformal_addr_eq = lambda a, b: (self.rvformal_addr_valid(a) == self.rvformal_addr_valid(b)) & ((~self.rvformal_addr_valid(a)) | (a == b))
+
+        # Input ports
+        self.reset = Signal(1)
+        self.check = Signal(1)
+        self.rvfi_valid = Signal(1)
+        self.rvfi_order = Signal(64)
+        self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
+    def ports(self):
+        input_ports = [
+            self.reset,
+            self.check,
+            self.rvfi_valid,
+            self.rvfi_order,
+            self.rvfi_pc_rdata,
+            self.rvfi_pc_wdata
+        ]
+        return input_ports
+    def elaborate(self, platform):
+        m = Module()
+
+        insn_order = AnyConst(64)
+        expect_pc = Signal(self.RISCV_FORMAL_XLEN)
+        expect_pc_valid = Signal(1, reset=0)
+
+        pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
+        m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
+
+        with m.If(self.reset):
+            m.d.sync += expect_pc_valid.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(expect_pc_valid):
+                    m.d.comb += Assert(self.rvformal_addr_eq(expect_pc, pc_wdata))
+            with m.Else():
+                with m.If(self.rvfi_valid & (self.rvfi_order == insn_order + 1)):
+                    m.d.sync += expect_pc.eq(self.rvfi_pc_rdata)
+                    m.d.sync += expect_pc_valid.eq(1)
+
+        return m

rvfi/cores/minerva/test/test_pc_backward.py

@@ -0,0 +1,25 @@
+from nmigen import *
+from nmigen.test.utils import *
+from ..core import *
+from ....checks.pc_bwd_check import *
+
+class PcBwdSpec(Elaboratable):
+    def elaborate(self, platform):
+        m = Module()
+
+        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
+        m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(1))
+
+        m.d.comb += pc_bwd_spec.reset.eq(0)
+        m.d.comb += pc_bwd_spec.check.eq(1)
+
+        m.d.comb += pc_bwd_spec.rvfi_valid.eq(cpu.rvfi.valid)
+        m.d.comb += pc_bwd_spec.rvfi_order.eq(cpu.rvfi.order)
+        m.d.comb += pc_bwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
+        m.d.comb += pc_bwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)
+
+        return m
+
+class PcBwdTestCase(FHDLTestCase):
+    def verify(self):
+        self.assertFormal(PcBwdSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

rvfi/cores/minerva/verify.py

@@ -2,6 +2,7 @@ import unittest
 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_units_divider import *
 from .test.test_units_multiplier import *
 
@@ -52,5 +53,8 @@ AndTestCase().verify()
 print("Verifying PC forward checks ...")
 PcFwdTestCase().verify()
 
+print("Verifying PC backward checks ...")
+PcBwdTestCase().verify()
+
 print("Testing multiplier and divider ...")
 unittest.main()