Add liveness check.

cores/microwatt/checks.pfv

@@ -2,6 +2,7 @@ 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

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
 
 

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 *

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