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

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()

diff --git a/src/nmutil/formal/test_clz.py b/src/nmutil/formal/test_clz.py
new file mode 100644 (file)
index 0000000..2bfcfe6
--- /dev/null
+++ b/src/nmutil/formal/test_clz.py
@@ -0,0 +1,64 @@
+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()