From 9fde9f97862adf6674aa3ae2d2ee5e705a29d2f3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= <jf@jfng.fr>
Date: Mon, 25 Jul 2022 15:26:24 +0200
Subject: [PATCH] Add liveness check.

---
 cores/microwatt/checks.pfv        | 11 ++++---
 cores/microwatt/microwatt/core.py | 24 ++++++++++++++
 power_fv/check/all.py             |  1 +
 power_fv/check/liveness.py        | 55 +++++++++++++++++++++++++++++++
 4 files changed, 86 insertions(+), 5 deletions(-)
 create mode 100644 power_fv/check/liveness.py

diff --git a/cores/microwatt/checks.pfv b/cores/microwatt/checks.pfv
index b80afe9..d9ca600 100644
--- a/cores/microwatt/checks.pfv
+++ b/cores/microwatt/checks.pfv
@@ -1,8 +1,9 @@
-check unique --depth=15 --skip=12
-check cia    --depth=15
-check gpr    --depth=15
-check causal --depth=15
-check insn   --depth=17 --exclude=brh,brw,setbc,setbcr,setnbc,setnbcr
+check unique   --depth=15 --skip=12
+check cia      --depth=15
+check gpr      --depth=15
+check causal   --depth=15
+check liveness --depth=20 --skip=12 --bus-fairness
+check insn     --depth=17 --exclude=brh,brw,setbc,setbcr,setnbc,setnbcr
 
 check microwatt:storage:data --depth=15
 
diff --git a/cores/microwatt/microwatt/core.py b/cores/microwatt/microwatt/core.py
index 1d1aeeb..b5cc828 100644
--- a/cores/microwatt/microwatt/core.py
+++ b/cores/microwatt/microwatt/core.py
@@ -17,6 +17,9 @@ class MicrowattWrapper(Elaboratable):
     @classmethod
     def add_check_arguments(cls, parser):
         group = parser.add_argument_group(title="microwatt options")
+        group.add_argument(
+            "--bus-fairness", action="store_true",
+            help="add bus fairness constraints")
         group.add_argument(
             "--ex1-bypass", choices=("true","false"), default="true",
             help="(default: %(default)s)")
@@ -148,6 +151,7 @@ class MicrowattWrapper(Elaboratable):
         keep_wb_fanout(self.wb_insn)
         keep_wb_fanout(self.wb_data)
 
+        self.bus_fairness  = bus_fairness;
         self._toplevel_src = self.MICROWATT_TOPLEVEL.format(**kwargs)
 
     def elaborate(self, platform):
@@ -266,6 +270,26 @@ class MicrowattWrapper(Elaboratable):
                 Assume(self.pfv.msr.w_mask.te[1].implies(~self.pfv.msr.w_data.te[1])),
             ]
 
+        if self.bus_fairness:
+            ibus_wait = Signal(2)
+            dbus_wait = Signal(2)
+
+            with m.If(self.wb_insn.cyc & self.wb_insn.stb & ~self.wb_insn.ack):
+                m.d.comb += Assume(self.wb_insn.stall)
+                m.d.sync += ibus_wait.eq(ibus_wait + 1)
+            with m.Else():
+                m.d.sync += ibus_wait.eq(0)
+
+            with m.If(self.wb_data.cyc & self.wb_data.stb & ~self.wb_data.ack):
+                m.d.comb += Assume(self.wb_data.stall)
+                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)),
+            ]
+
         return m
 
 
diff --git a/power_fv/check/all.py b/power_fv/check/all.py
index f638bf6..8c793a2 100644
--- a/power_fv/check/all.py
+++ b/power_fv/check/all.py
@@ -2,4 +2,5 @@ from .unique import *
 from .cia import *
 from .gpr import *
 from .causal import *
+from .liveness import *
 from .insn.all import *
diff --git a/power_fv/check/liveness.py b/power_fv/check/liveness.py
new file mode 100644
index 0000000..bf728ac
--- /dev/null
+++ b/power_fv/check/liveness.py
@@ -0,0 +1,55 @@
+from amaranth import *
+from amaranth.asserts import *
+
+from power_fv.check import PowerFVCheck
+from power_fv.check._timer import Timer
+
+
+__all__ = ["LivenessCheck"]
+
+
+class LivenessCheck(PowerFVCheck, name=("liveness",)):
+    """Liveness check.
+
+    Checks that a core does not hang for the duration of the bounded-model check.
+    """
+
+    def testbench(self):
+        return LivenessTestbench(self)
+
+
+class LivenessTestbench(Elaboratable):
+    def __init__(self, check):
+        if not isinstance(check, LivenessCheck):
+            raise TypeError("Check must be an instance of LivenessCheck, not {!r}"
+                            .format(check))
+        self.check = check
+        self.name  = "liveness_tb"
+
+    def elaborate(self, platform):
+        m = Module()
+
+        m.submodules.t_pre  = t_pre  = Timer(self.check.skip  - 1)
+        m.submodules.t_post = t_post = Timer(self.check.depth - 1)
+        m.submodules.dut    = dut    = self.check.dut
+
+        curr_order   = AnyConst(dut.pfv.order.shape())
+        next_order   = curr_order + 1
+        next_retired = Signal()
+
+        with m.If(Rose(t_pre.zero)):
+            m.d.comb += [
+                Assume(dut.pfv.stb),
+                Assume(curr_order == dut.pfv.order),
+            ]
+
+        with m.Elif(t_pre.zero):
+            with m.If(dut.pfv.stb & (dut.pfv.order == next_order)):
+                m.d.sync += next_retired.eq(1)
+
+        with m.If(t_post.zero):
+            m.d.comb += Assert(next_retired)
+
+        m.d.comb += Assert(~Past(t_post.zero))
+
+        return m