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

Add bounded fairness constraints for liveness check

Browse Source
This commit is contained in:
Donald Sebastian Leung 2020-09-15 17:12:58 +08:00
parent e3b124f4eb
commit ee19bc49e7
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -497,6 +497,22 @@ class LivenessSpec(Elaboratable):
m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order) m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += liveness_spec.rvfi_halt.eq(cpu.rvfi.halt) m.d.comb += liveness_spec.rvfi_halt.eq(cpu.rvfi.halt)
# Bounded fairness constraints
ibus_wait = Signal(2, reset=0)
dbus_wait = Signal(2, reset=0)
with m.If(cpu.ibus.cyc & cpu.ibus.stb & ~(cpu.ibus.ack | cpu.ibus.err)):
m.d.sync += ibus_wait.eq(ibus_wait + 1)
with m.Else():
m.d.sync += ibus_wait.eq(0)
with m.If(cpu.dbus.cyc & cpu.dbus.stb & ~(cpu.dbus.ack | cpu.dbus.err)):
m.d.sync += dbus_wait.eq(dbus_wait + 1)
with m.Else():
m.d.sync += dbus_wait.eq(0)
m.d.comb += Assume((ibus_wait < 2) & (dbus_wait < 2))
with m.If(liveness_spec.reset):
m.d.sync += ibus_wait.eq(0)
m.d.sync += dbus_wait.eq(0)
return m return m
class LivenessTestCase(FHDLTestCase): class LivenessTestCase(FHDLTestCase):