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()