diff --git a/README.md b/README.md index f554d74..1f55f2b 100644 --- a/README.md +++ b/README.md @@ -37,7 +37,7 @@ This should run in the order of a few hours. - [x] Register checks - [x] Causal checks - [ ] Liveness checks -- [ ] Uniqueness checks +- [x] Uniqueness checks ## Scope diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index 5bb601e..c31cfad 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -489,9 +489,12 @@ class LivenessSpec(Elaboratable): m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) m.d.comb += cpu.dbus.err.eq(0) - m.d.comb += liveness_spec.reset.eq(AnySeq(1)) - m.d.comb += liveness_spec.trig.eq(AnySeq(1)) - m.d.comb += liveness_spec.check.eq(AnySeq(1)) + cycle = Signal(8, reset=0) + with m.If(cycle != 0xFF): + m.d.sync += cycle.eq(cycle + 1) + m.d.comb += liveness_spec.reset.eq(cycle < 1) + m.d.comb += liveness_spec.trig.eq(cycle == 11) + m.d.comb += liveness_spec.check.eq(cycle == 49) m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid) m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order) @@ -517,8 +520,8 @@ class LivenessSpec(Elaboratable): class LivenessTestCase(FHDLTestCase): def verify(self): - self.assertFormal(LivenessSpec(), mode="cover", depth=20) - self.assertFormal(LivenessSpec(), mode="bmc", depth=20) + self.assertFormal(LivenessSpec(), mode="cover", depth=50) + self.assertFormal(LivenessSpec(), mode="bmc", depth=50) class UniqueSpec(Elaboratable): def elaborate(self, platform): @@ -552,9 +555,12 @@ class UniqueSpec(Elaboratable): m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) m.d.comb += cpu.dbus.err.eq(0) - m.d.comb += unique_spec.reset.eq(AnySeq(1)) - m.d.comb += unique_spec.trig.eq(AnySeq(1)) - m.d.comb += unique_spec.check.eq(AnySeq(1)) + cycle = Signal(8) + with m.If(cycle != 0xFF): + m.d.sync += cycle.eq(cycle + 1) + m.d.comb += unique_spec.reset.eq(cycle < 1) + m.d.comb += unique_spec.trig.eq(cycle == 11) + m.d.comb += unique_spec.check.eq(cycle == 24) m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid) m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order) @@ -563,8 +569,8 @@ class UniqueSpec(Elaboratable): class UniqueTestCase(FHDLTestCase): def verify(self): - self.assertFormal(UniqueSpec(), mode="cover", depth=20) - self.assertFormal(UniqueSpec(), mode="bmc", depth=20) + self.assertFormal(UniqueSpec(), mode="cover", depth=25) + self.assertFormal(UniqueSpec(), mode="bmc", depth=25) print('*' * 80) print('*' + ' ' * 78 + '*')