From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 1 Nov 2020 17:02:52 +0000 (-0300)
Subject: Add a check for liveness.
X-Git-Tag: 24jan2021_ls180~119
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3c7411efd6aa20dc37c3f778180d5cbbd9626de;p=soc.git

Add a check for liveness.

There was already a check for the correctness of the results, but there
was no guarantee that any result would be produced at all.
---

diff --git a/src/soc/experiment/formal/proof_alu_fsm.py b/src/soc/experiment/formal/proof_alu_fsm.py
index 51bc26d5..97f36a8f 100644
--- a/src/soc/experiment/formal/proof_alu_fsm.py
+++ b/src/soc/experiment/formal/proof_alu_fsm.py
@@ -36,6 +36,8 @@ class Driver(Elaboratable):
         # transaction count for each port
         write_cnt = Signal(4)
         read_cnt = Signal(4)
+        # liveness counter
+        live_cnt = Signal(5)
         # keep data and valid stable, until accepted
         with m.If(Past(dut.p.valid_i) & ~Past(dut.p.ready_o)):
             comb += [
@@ -70,6 +72,15 @@ class Driver(Elaboratable):
         # Whenever the unit is busy (not ready) the read and write counters
         # will differ by exactly one unit.
         m.d.comb += Assert((read_cnt + ~dut.p.ready_o) & 0xF == write_cnt)
+        # Check for liveness. It will ensure that the FSM is not stuck, and
+        # will eventually produce some result.
+        # In this case, the delay between ready_o being negated and valid_o
+        # being asserted has to be less than 16 cycles.
+        with m.If(~dut.p.ready_o & ~dut.n.valid_o):
+            m.d.sync += live_cnt.eq(live_cnt + 1)
+        with m.Else():
+            m.d.sync += live_cnt.eq(0)
+        m.d.comb += Assert(live_cnt < 16)
         # check coverage as output data is accepted
         with m.If(dut.n.ready_i & dut.n.valid_o):
             # increment read counter