From e404911c91db8a9ef96f388ba44984c7d9ff933b Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 1 Jun 2020 13:48:13 -0400 Subject: [PATCH] Enable k-induction for register file proof --- src/soc/regfile/formal/proof_regfile.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py index 27b4fb97..0dcb1964 100644 --- a/src/soc/regfile/formal/proof_regfile.py +++ b/src/soc/regfile/formal/proof_regfile.py @@ -60,8 +60,6 @@ class Driver(Register): comb += Assume(register_written == 0) - with m.If(Past(rst)): - pass with m.Else(): comb += Assume(rst == 0) @@ -108,7 +106,7 @@ class TestCase(FHDLTestCase): def test_formal(self): for writethrough in [False, True]: module = Driver(writethrough) - self.assertFormal(module, mode="bmc", depth=10) + self.assertFormal(module, mode="prove", depth=10) def test_ilang(self): dut = Driver() -- 2.30.2