From ee19bc49e724e29823a116806475c3de1b38bf68 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Tue, 15 Sep 2020 17:12:58 +0800
Subject: [PATCH] Add bounded fairness constraints for liveness check
---
rvfi/cores/minerva/verify.py | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index e82cd13..5bb601e 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -497,6 +497,22 @@ class LivenessSpec(Elaboratable):
m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
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
class LivenessTestCase(FHDLTestCase):