From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 1 Jun 2020 17:48:13 +0000 (-0400)
Subject: Enable k-induction for register file proof
X-Git-Tag: div_pipeline~679
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e404911c91db8a9ef96f388ba44984c7d9ff933b;p=soc.git

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 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()