From b38f19411af02f810b4895591abdb0121ba715eb Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Thu, 17 Sep 2020 13:08:04 +0800
Subject: [PATCH] Make uniqueness checks pass
---
README.md | 2 +-
rvfi/cores/minerva/verify.py | 26 ++++++++++++++++----------
2 files changed, 17 insertions(+), 11 deletions(-)
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 + '*')