From a6b4891a381829312e3cb7c7e180dcc0913c3f8b Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Thu, 20 Aug 2020 12:00:31 +0800
Subject: [PATCH] Add causal checks
---
rvfi/checks/causal_check.py | 49 ++++++++++++++++++++++++++
rvfi/cores/minerva/test/test_causal.py | 25 +++++++++++++
rvfi/cores/minerva/verify.py | 4 +++
3 files changed, 78 insertions(+)
create mode 100644 rvfi/checks/causal_check.py
create mode 100644 rvfi/cores/minerva/test/test_causal.py
diff --git a/rvfi/checks/causal_check.py b/rvfi/checks/causal_check.py
new file mode 100644
index 0000000..3e19f6a
--- /dev/null
+++ b/rvfi/checks/causal_check.py
@@ -0,0 +1,49 @@
+from nmigen import *
+from nmigen.asserts import *
+
+"""
+Causal Check
+"""
+
+class CausalCheck(Elaboratable):
+ def __init__(self):
+ # Input ports
+ self.reset = Signal(1)
+ self.check = Signal(1)
+ self.rvfi_valid = Signal(1)
+ self.rvfi_rd_addr = Signal(5)
+ self.rvfi_order = Signal(64)
+ self.rvfi_rs1_addr = Signal(5)
+ self.rvfi_rs2_addr = Signal(5)
+ def ports(self):
+ input_ports = [
+ self.reset,
+ self.check,
+ self.rvfi_valid,
+ self.rvfi_rd_addr,
+ self.rvfi_order,
+ self.rvfi_rs1_addr,
+ self.rvfi_rs2_addr
+ ]
+ return input_ports
+ def elaborate(self, platform):
+ m = Module()
+
+ insn_order = AnyConst(64)
+ register_index = AnyConst(5)
+ found_non_causal = Signal(1, reset=0)
+
+ with m.If(self.reset):
+ m.d.sync += found_non_causal.eq(0)
+ with m.Else():
+ with m.If(self.check):
+ m.d.comb += Assume(register_index != 0)
+ m.d.comb += Assume(self.rvfi_valid)
+ m.d.comb += Assume(register_index == self.rvfi_rd_addr)
+ m.d.comb += Assume(insn_order == self.rvfi_order)
+ m.d.comb += Assert(~found_non_causal)
+ with m.Else():
+ with m.If(self.rvfi_valid & (self.rvfi_order > insn_order) & ((register_index == self.rvfi_rs1_addr) | (register_index == self.rvfi_rs2_addr))):
+ m.d.sync += found_non_causal.eq(1)
+
+ return m
diff --git a/rvfi/cores/minerva/test/test_causal.py b/rvfi/cores/minerva/test/test_causal.py
new file mode 100644
index 0000000..9c1ed42
--- /dev/null
+++ b/rvfi/cores/minerva/test/test_causal.py
@@ -0,0 +1,25 @@
+from nmigen import *
+from ..core import *
+from nmigen.test.utils import *
+from ....checks.causal_check import *
+
+class CausalSpec(Elaboratable):
+ def elaborate(self, platform):
+ m = Module()
+
+ m.submodules.cpu = cpu = Minerva(with_rvfi=True)
+ m.submodules.causal_spec = causal_spec = CausalCheck()
+
+ m.d.comb += causal_spec.reset.eq(0)
+ m.d.comb += causal_spec.check.eq(1)
+ m.d.comb += causal_spec.rvfi_valid.eq(cpu.rvfi.valid)
+ m.d.comb += causal_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
+ m.d.comb += causal_spec.rvfi_order.eq(cpu.rvfi.order)
+ m.d.comb += causal_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
+ m.d.comb += causal_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
+
+ return m
+
+class CausalTestCase(FHDLTestCase):
+ def verify(self):
+ self.assertFormal(CausalSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index 44279bc..944e770 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -4,6 +4,7 @@ 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_causal import *
from .test.test_units_divider import *
from .test.test_units_multiplier import *
@@ -60,5 +61,8 @@ PcBwdTestCase().verify()
print("Verifying register checks ...")
RegTestCase().verify()
+print("Verifying causal checks ...")
+CausalTestCase().verify()
+
print("Testing multiplier and divider ...")
unittest.main()