Enable k-induction for register file proof

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
index 27b4fb977d543dbffdf5ff3092acab70d47acb50..0dcb19647719588fbc354cb4c815638006804dfd 100644 (file)
--- 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()