diff --git a/rvfi/checks/unique_check.py b/rvfi/checks/unique_check.py new file mode 100644 index 0000000..ae785f4 --- /dev/null +++ b/rvfi/checks/unique_check.py @@ -0,0 +1,43 @@ +from nmigen import * +from nmigen.asserts import * + +""" +Unique Check +""" + +class UniqueCheck(Elaboratable): + def __init__(self): + self.reset = Signal(1) + self.rvfi_valid = Signal(1) + self.rvfi_order = Signal(64) + self.trig = Signal(1) + self.check = Signal(1) + + def ports(self): + input_ports = [ + self.reset, + self.rvfi_valid, + self.rvfi_order, + self.trig, + self.check + ] + return input_ports + + def elaborate(self, platform): + m = Module() + + insn_order = AnyConst(64) + found_other_insn = Signal(1, reset=0) + + with m.If(self.reset): + m.d.sync += found_other_insn.eq(0) + with m.Else(): + with m.If(self.rvfi_valid & (self.rvfi_order == insn_order) & ~self.trig): + m.d.sync += found_other_insn.eq(1) + with m.If(self.trig): + m.d.comb += Assume(self.rvfi_valid) + m.d.comb += Assume(insn_order == self.rvfi_order) + with m.If(self.check): + m.d.comb += Assert(~found_other_insn) + + return m diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index 8bc3b8b..e9f0b95 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -5,6 +5,7 @@ from ...checks.pc_bwd_check import * from ...checks.reg_check import * from ...checks.causal_check import * from ...checks.liveness_check import * +from ...checks.unique_check import * from minerva.core import * from ...insns.insn_lui import * from ...insns.insn_auipc import * @@ -241,6 +242,25 @@ class LivenessTestCase(FHDLTestCase): def verify(self): self.assertFormal(LivenessSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") +class UniqueSpec(Elaboratable): + def elaborate(self, platform): + m = Module() + + m.submodules.cpu = cpu = Minerva(with_rvfi=True) + m.submodules.unique_spec = unique_spec = UniqueCheck() + + m.d.comb += unique_spec.reset.eq(0) + m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid) + m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order) + m.d.comb += unique_spec.trig.eq(1) + m.d.comb += unique_spec.check.eq(1) + + return m + +class UniqueTestCase(FHDLTestCase): + def verify(self): + self.assertFormal(UniqueSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") + print('*' * 80) print('*' + ' ' * 78 + '*') print('* Verifying the Minerva core ... *') @@ -265,6 +285,9 @@ CausalTestCase().verify() print("Verifying liveness checks ...") LivenessTestCase().verify() +print("Verifying uniqueness checks ...") +UniqueTestCase().verify() + print('*' * 80) print('*' + ' ' * 78 + '*') print('* All verification tasks successful! *')