M-Labs
/
riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Make uniqueness checks pass

This commit is contained in:
Donald Sebastian Leung 2020-09-17 13:08:04 +08:00
parent e50d35ead5
commit b38f19411a
2 changed files with 17 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@ -37,7 +37,7 @@ This should run in the order of a few hours.
- [x] Register checks - [x] Register checks
- [x] Causal checks - [x] Causal checks
- [ ] Liveness checks - [ ] Liveness checks
- [ ] Uniqueness checks - [x] Uniqueness checks
## Scope ## Scope

26
rvfi/cores/minerva/verify.py
View File

@ -489,9 +489,12 @@ class LivenessSpec(Elaboratable):
m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0) m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += liveness_spec.reset.eq(AnySeq(1)) cycle = Signal(8, reset=0)
m.d.comb += liveness_spec.trig.eq(AnySeq(1)) with m.If(cycle != 0xFF):
m.d.comb += liveness_spec.check.eq(AnySeq(1)) 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_valid.eq(cpu.rvfi.valid)
m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order) m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
@ -517,8 +520,8 @@ class LivenessSpec(Elaboratable):
class LivenessTestCase(FHDLTestCase): class LivenessTestCase(FHDLTestCase):
def verify(self): def verify(self):
self.assertFormal(LivenessSpec(), mode="cover", depth=20) self.assertFormal(LivenessSpec(), mode="cover", depth=50)
self.assertFormal(LivenessSpec(), mode="bmc", depth=20) self.assertFormal(LivenessSpec(), mode="bmc", depth=50)
class UniqueSpec(Elaboratable): class UniqueSpec(Elaboratable):
def elaborate(self, platform): 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.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0) m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += unique_spec.reset.eq(AnySeq(1)) cycle = Signal(8)
m.d.comb += unique_spec.trig.eq(AnySeq(1)) with m.If(cycle != 0xFF):
m.d.comb += unique_spec.check.eq(AnySeq(1)) 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_valid.eq(cpu.rvfi.valid)
m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order) m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)
@ -563,8 +569,8 @@ class UniqueSpec(Elaboratable):
class UniqueTestCase(FHDLTestCase): class UniqueTestCase(FHDLTestCase):
def verify(self): def verify(self):
self.assertFormal(UniqueSpec(), mode="cover", depth=20) self.assertFormal(UniqueSpec(), mode="cover", depth=25)
self.assertFormal(UniqueSpec(), mode="bmc", depth=20) self.assertFormal(UniqueSpec(), mode="bmc", depth=25)
print('*' * 80) print('*' * 80)
print('*' + ' ' * 78 + '*') print('*' + ' ' * 78 + '*')