From 878e4c6776203e12abb4cf4e78f6d251121418c1 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 16 Nov 2021 20:07:41 -0800
Subject: [PATCH] add formal tests for BitwiseLut

---
 .gitignore                  |  2 +
 src/nmutil/test/test_lut.py | 77 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 78 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 77d4f5d..8248bf2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,3 +9,5 @@ __pycache__
 .eggs
 *.egg-info
 *.gtkw
+/sim_test_out
+/formal_test_temp
\ No newline at end of file
diff --git a/src/nmutil/test/test_lut.py b/src/nmutil/test/test_lut.py
index 2863e83..d36cb4e 100644
--- a/src/nmutil/test/test_lut.py
+++ b/src/nmutil/test/test_lut.py
@@ -3,8 +3,14 @@
 
 from contextlib import contextmanager
 import unittest
-
 from hashlib import sha256
+import shutil
+import subprocess
+from nmigen.back import rtlil
+import textwrap
+from nmigen.hdl.ast import AnyConst, Assert, Signal
+from nmigen.hdl.dsl import Module
+from nmigen.hdl.ir import Fragment
 from nmutil.get_test_path import get_test_path
 from nmutil.lut import BitwiseMux, BitwiseLut
 from nmigen.sim import Simulator, Delay
@@ -23,6 +29,43 @@ def do_sim(test_case, dut, traces=()):
         yield sim
 
 
+# copied from ieee754fpu/src/ieee754/partitioned_signal_tester.py
+def formal(test_case, hdl, *, base_path="formal_test_temp"):
+    hdl = Fragment.get(hdl, platform="formal")
+    path = get_test_path(test_case, base_path)
+    shutil.rmtree(path, ignore_errors=True)
+    path.mkdir(parents=True)
+    sby_name = "config.sby"
+    sby_file = path / sby_name
+
+    sby_file.write_text(textwrap.dedent(f"""\
+    [options]
+    mode prove
+    depth 1
+    wait on
+
+    [engines]
+    smtbmc
+
+    [script]
+    read_rtlil top.il
+    prep
+
+    [file top.il]
+    {rtlil.convert(hdl)}
+    """), encoding="utf-8")
+    sby = shutil.which('sby')
+    assert sby is not None
+    with subprocess.Popen(
+        [sby, sby_name],
+        cwd=path, text=True, encoding="utf-8",
+        stdin=subprocess.DEVNULL, stdout=subprocess.PIPE
+    ) as p:
+        stdout, stderr = p.communicate()
+        if p.returncode != 0:
+            test_case.fail(f"Formal failed:\n{stdout}")
+
+
 def hash_256(v):
     return int.from_bytes(
         sha256(bytes(v, encoding='utf-8')).digest(),
@@ -61,6 +104,21 @@ class TestBitwiseMux(unittest.TestCase):
             sim.add_process(process)
             sim.run()
 
+    def test_formal(self):
+        width = 2
+        dut = BitwiseMux(width)
+        m = Module()
+        m.submodules.dut = dut
+        m.d.comb += dut.sel.eq(AnyConst(width))
+        m.d.comb += dut.f.eq(AnyConst(width))
+        m.d.comb += dut.t.eq(AnyConst(width))
+        for i in range(width):
+            with m.If(dut.sel[i]):
+                m.d.comb += Assert(dut.t[i] == dut.output[i])
+            with m.Else():
+                m.d.comb += Assert(dut.f[i] == dut.output[i])
+        formal(self, m)
+
 
 class TestBitwiseLut(unittest.TestCase):
     def test(self):
@@ -121,6 +179,23 @@ class TestBitwiseLut(unittest.TestCase):
             sim.add_process(process)
             sim.run()
 
+    def test_formal(self):
+        dut = BitwiseLut(3, 16)
+        m = Module()
+        m.submodules.dut = dut
+        m.d.comb += dut.inputs[0].eq(AnyConst(dut.width))
+        m.d.comb += dut.inputs[1].eq(AnyConst(dut.width))
+        m.d.comb += dut.inputs[2].eq(AnyConst(dut.width))
+        m.d.comb += dut.lut.eq(AnyConst(dut.lut.width))
+        for i in range(dut.width):
+            lut_index = Signal(dut.input_count, name=f"lut_index_{i}")
+            for j in range(dut.input_count):
+                m.d.comb += lut_index[j].eq(dut.inputs[j][i])
+            for j in range(dut.lut.width):
+                with m.If(lut_index == j):
+                    m.d.comb += Assert(dut.lut[j] == dut.output[i])
+        formal(self, m)
+
 
 if __name__ == "__main__":
     unittest.main()
-- 
2.30.2