From 89a69474346f0da92e9a18e216a72d84f528085d Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 20 Sep 2020 19:32:46 -0300 Subject: [PATCH] Add induction proof for the FSM Shifter --- src/soc/experiment/formal/proof_alu_fsm.py | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/soc/experiment/formal/proof_alu_fsm.py b/src/soc/experiment/formal/proof_alu_fsm.py index 07b347c8..bb83c918 100644 --- a/src/soc/experiment/formal/proof_alu_fsm.py +++ b/src/soc/experiment/formal/proof_alu_fsm.py @@ -44,6 +44,10 @@ class Driver(Elaboratable): Assume(Stable(dut.p.data_i.shift)), Assume(Stable(dut.p.valid_i)), ] + # force reading the output in a reasonable time, + # necessary to pass induction + with m.If(Past(dut.n.valid_o) & ~Past(dut.n.ready_i)): + comb += Assume(dut.n.ready_i) # capture transferred input data with m.If(dut.p.ready_o & dut.p.valid_i): sync += [ @@ -126,8 +130,16 @@ class ALUFSMTestCase(FHDLTestCase): module='top.dut', zoom=-6.3 ) + write_gtkw( + 'test_formal_induct_alu_fsm.gtkw', + os.path.dirname(__file__) + + '/proof_alu_fsm_formal/engine_0/trace_induct.vcd', + traces, + module='top.dut', + zoom=-6.3 + ) module = Driver() - self.assertFormal(module, mode="bmc", depth=16) + self.assertFormal(module, mode="prove", depth=18) self.assertFormal(module, mode="cover", depth=32) @staticmethod -- 2.30.2