From: Jean THOMAS <git0@pub.jeanthomas.me>
Date: Mon, 22 Jun 2020 15:51:31 +0000 (+0200)
Subject: Remove code for hybrid formal proof, unused
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50137744eb14c218ff52592efae89e121e040590;p=gram.git

Remove code for hybrid formal proof, unused
---

diff --git a/gram/test/utils/formal.py b/gram/test/utils/formal.py
index dfbd63e..cc3b87a 100644
--- a/gram/test/utils/formal.py
+++ b/gram/test/utils/formal.py
@@ -66,14 +66,6 @@ class FHDLTestCase(unittest.TestCase):
         if os.path.exists(os.path.join(spec_dir, spec_name)):
             shutil.rmtree(os.path.join(spec_dir, spec_name))
 
-        if mode == "hybrid":
-            # A mix of BMC and k-induction, as per personal
-            # communication with Clifford Wolf.
-            script = "setattr -unset init w:* a:nmigen.sample_reg %d"
-            mode   = "bmc"
-        else:
-            script = ""
-
         config = textwrap.dedent("""\
         [options]
         mode {mode}
@@ -86,7 +78,6 @@ class FHDLTestCase(unittest.TestCase):
         [script]
         read_ilang top.il
         prep
-        {script}
 
         [file top.il]
         {rtlil}