From: Jacob Lifshay Date: Tue, 10 May 2022 01:41:54 +0000 (-0700) Subject: rename proof_clz.py -> test_clz.py so it's run by pytest X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ad8942d98f70aa237f2f2f86dbb0caa720ddf0c;p=nmutil.git 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 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 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()