src/nmutil/formal/test_clz.py

   1 from nmigen import Module, Signal, Elaboratable, Mux, Const
   2 from nmigen.asserts import Assert, AnyConst, Assume
   3 from nmutil.formaltest import FHDLTestCase
   4 from nmigen.cli import rtlil
   5
   6 from nmutil.clz import CLZ
   7 import unittest
   8
   9
  10 # This defines a module to drive the device under test and assert
  11 # properties about its outputs
  12 class Driver(Elaboratable):
  13     def __init__(self):
  14         # inputs and outputs
  15         pass
  16
  17     def elaborate(self, platform):
  18         m = Module()
  19         comb = m.d.comb
  20         width = 10
  21
  22         m.submodules.dut = dut = CLZ(width)
  23         sig_in = Signal.like(dut.sig_in)
  24         count = Signal.like(dut.lz)
  25
  26         m.d.comb += [
  27             sig_in.eq(AnyConst(width)),
  28             dut.sig_in.eq(sig_in),
  29             count.eq(dut.lz)]
  30
  31         result = Const(width)
  32         for i in range(width):
  33             print(result)
  34             result_next = Signal.like(count, name="count_%d" % i)
  35             with m.If(sig_in[i] == 1):
  36                 comb += result_next.eq(width-i-1)
  37             with m.Else():
  38                 comb += result_next.eq(result)
  39             result = result_next
  40
  41         result_sig = Signal.like(count)
  42         comb += result_sig.eq(result)
  43
  44         comb += Assert(result_sig == count)
  45
  46         # setup the inputs and outputs of the DUT as anyconst
  47
  48         return m
  49
  50
  51 class CLZTestCase(FHDLTestCase):
  52     def test_proof(self):
  53         module = Driver()
  54         self.assertFormal(module, mode="bmc", depth=4)
  55
  56     def test_ilang(self):
  57         dut = Driver()
  58         vl = rtlil.convert(dut, ports=[])
  59         with open("clz.il", "w") as f:
  60             f.write(vl)
  61
  62
  63 if __name__ == '__main__':
  64     unittest.main()