From 878e4c6776203e12abb4cf4e78f6d251121418c1 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay 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