From 73400e4c529c10703aba6660fdb3b43dde9a461b Mon Sep 17 00:00:00 2001
From: Michael Nolan <mtnolan2640@gmail.com>
Date: Tue, 28 Jan 2020 18:19:19 -0500
Subject: [PATCH 1/1] Use nmigen's built in formal runner instead of mine

---
 src/ieee754/fpmax/formal/proof.sby          | 13 -------
 src/ieee754/fpmax/formal/proof_fmax_mod.py  | 42 +++++++--------------
 src/ieee754/fsgnj/formal/proof_fsgnj_mod.py | 38 ++++++-------------
 3 files changed, 24 insertions(+), 69 deletions(-)
 delete mode 100644 src/ieee754/fpmax/formal/proof.sby

diff --git a/src/ieee754/fpmax/formal/proof.sby b/src/ieee754/fpmax/formal/proof.sby
deleted file mode 100644
index 6c26b0f6..00000000
--- a/src/ieee754/fpmax/formal/proof.sby
+++ /dev/null
@@ -1,13 +0,0 @@
-[options]
-mode bmc
-depth 5
-
-[engines]
-smtbmc yices
-
-[script]
-read_ilang proof.il
-prep -top top
-
-[files]
-proof.il
diff --git a/src/ieee754/fpmax/formal/proof_fmax_mod.py b/src/ieee754/fpmax/formal/proof_fmax_mod.py
index 37538315..70081196 100644
--- a/src/ieee754/fpmax/formal/proof_fmax_mod.py
+++ b/src/ieee754/fpmax/formal/proof_fmax_mod.py
@@ -1,15 +1,14 @@
 # Proof of correctness for FPMAX module
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
-from nmigen import Module, Signal, Elaboratable, Cat, Mux
-from nmigen.asserts import Assert, Assume, AnyConst
-from nmigen.cli import rtlil
+from nmigen import Module, Signal, Elaboratable, Mux
+from nmigen.asserts import Assert, AnyConst
+from nmigen.test.utils import FHDLTestCase
 
 from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
 from ieee754.fpmax.fpmax import FPMAXPipeMod
 from ieee754.pipeline import PipelineSpec
-import subprocess
-import os
+import unittest
 
 
 # This defines a module to drive the device under test and assert
@@ -98,27 +97,12 @@ class FPMAXDriver(Elaboratable):
         return []
 
 
-def run_test(bits=32):
-    m = FPMAXDriver(PipelineSpec(bits, 2, 1))
-
-    il = rtlil.convert(m, ports=m.ports())
-    with open("proof.il", "w") as f:
-        f.write(il)
-    filedir = os.path.dirname(os.path.realpath(__file__))
-    sbyfile = os.path.join(filedir, 'proof.sby')
-    p = subprocess.Popen(['sby', '-f', sbyfile],
-                         stdout=subprocess.PIPE,
-                         stderr=subprocess.PIPE)
-    if p.wait() == 0:
-        out, _ = p.communicate()
-        print("Proof successful!")
-        print(out.decode('utf-8'))
-    else:
-        print("Proof failed")
-        out, err = p.communicate()
-        print(out.decode('utf-8'))
-        print(err.decode('utf-8'))
-
-
-if __name__ == "__main__":
-    run_test(bits=32)
+class FPMAXTestCase(FHDLTestCase):
+    def test_max(self):
+        for bits in [16, 32, 64]:
+            module = FPMAXDriver(PipelineSpec(bits, 2, 1))
+            self.assertFormal(module, mode="bmc", depth=4)
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py b/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
index 8c3fe9c1..b960a85c 100644
--- a/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
+++ b/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
@@ -3,13 +3,12 @@
 
 from nmigen import Module, Signal, Elaboratable
 from nmigen.asserts import Assert, Assume
-from nmigen.cli import rtlil
+from nmigen.test.utils import FHDLTestCase
 
 from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
 from ieee754.fsgnj.fsgnj import FSGNJPipeMod
 from ieee754.pipeline import PipelineSpec
-import subprocess
-import os
+import unittest
 
 # This defines a module to drive the device under test and assert
 # properties about its outputs
@@ -83,27 +82,12 @@ class FSGNJDriver(Elaboratable):
         return [self.a, self.b, self.z, self.opc, self.muxid]
 
 
-def run_test(bits=32):
-    m = FSGNJDriver(PipelineSpec(bits, 2, 2))
-
-    il = rtlil.convert(m, ports=m.ports())
-    with open("proof.il", "w") as f:
-        f.write(il)
-    dirs = os.path.split(__file__)[0]
-    p = subprocess.Popen(['sby', '-f', '%s/proof.sby' % dirs],
-                         stdout=subprocess.PIPE,
-                         stderr=subprocess.PIPE)
-    if p.wait() == 0:
-        out, _ = p.communicate()
-        print("Proof successful!")
-    else:
-        print("Proof failed")
-        out, err = p.communicate()
-        print(out.decode('utf-8'))
-        print(err.decode('utf-8'))
-
-
-if __name__ == "__main__":
-    run_test(bits=32)
-    run_test(bits=16)
-    run_test(bits=64)
+class FPMAXTestCase(FHDLTestCase):
+    def test_max(self):
+        for bits in [16, 32, 64]:
+            module = FSGNJDriver(PipelineSpec(bits, 2, 2))
+            self.assertFormal(module, mode="bmc", depth=4)
+
+
+if __name__ == '__main__':
+    unittest.main()
-- 
2.30.2