From c3c7411efd6aa20dc37c3f778180d5cbbd9626de Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 1 Nov 2020 14:02:52 -0300 Subject: [PATCH] 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. --- src/soc/experiment/formal/proof_alu_fsm.py | 11 +++++++++++ 1 file changed, 11 insertions(+) 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 -- 2.30.2