rename proof_clz.py -> test_clz.py so it's run by pytest

[nmutil.git] / src / nmutil / formal / proof_clz.py

diff --git a/src/nmutil/formal/proof_clz.py b/src/nmutil/formal/proof_clz.py
deleted file mode 100644 (file)
index 2bfcfe6..0000000
--- a/src/nmutil/formal/proof_clz.py
+++ /dev/null
@@ -1,64 +0,0 @@
-from nmigen import Module, Signal, Elaboratable, Mux, Const
-from nmigen.asserts import Assert, AnyConst, Assume
-from nmutil.formaltest import FHDLTestCase
-from nmigen.cli import rtlil
-
-from nmutil.clz import CLZ
-import unittest
-
-
-# This defines a module to drive the device under test and assert
-# properties about its outputs
-class Driver(Elaboratable):
-    def __init__(self):
-        # inputs and outputs
-        pass
-
-    def elaborate(self, platform):
-        m = Module()
-        comb = m.d.comb
-        width = 10
-
-        m.submodules.dut = dut = CLZ(width)
-        sig_in = Signal.like(dut.sig_in)
-        count = Signal.like(dut.lz)
-
-        m.d.comb += [
-            sig_in.eq(AnyConst(width)),
-            dut.sig_in.eq(sig_in),
-            count.eq(dut.lz)]
-
-        result = Const(width)
-        for i in range(width):
-            print(result)
-            result_next = Signal.like(count, name="count_%d" % i)
-            with m.If(sig_in[i] == 1):
-                comb += result_next.eq(width-i-1)
-            with m.Else():
-                comb += result_next.eq(result)
-            result = result_next
-
-        result_sig = Signal.like(count)
-        comb += result_sig.eq(result)
-
-        comb += Assert(result_sig == count)
-
-        # setup the inputs and outputs of the DUT as anyconst
-
-        return m
-
-
-class CLZTestCase(FHDLTestCase):
-    def test_proof(self):
-        module = Driver()
-        self.assertFormal(module, mode="bmc", depth=4)
-
-    def test_ilang(self):
-        dut = Driver()
-        vl = rtlil.convert(dut, ports=[])
-        with open("clz.il", "w") as f:
-            f.write(vl)
-
-
-if __name__ == '__main__':
-    unittest.main()