src/nmutil/formal/proof_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
  27         m.d.comb += [
  28             sig_in.eq(AnyConst(width)),
  29             dut.sig_in.eq(sig_in),
  30             count.eq(dut.lz)]
  31
  32         result = Const(width)
  33         for i in range(width):
  34             print(result)
  35             result_next = Signal.like(count, name="count_%d" % i)
  36             with m.If(sig_in[i] == 1):
  37                 comb += result_next.eq(width-i-1)
  38             with m.Else():
  39                 comb += result_next.eq(result)
  40             result = result_next
  41
  42         result_sig = Signal.like(count)
  43         comb += result_sig.eq(result)
  44
  45         comb += Assert(result_sig == count)
  46
  47         # setup the inputs and outputs of the DUT as anyconst
  48
  49         return m
  50
  51 class CLZTestCase(FHDLTestCase):
  52     def test_proof(self):
  53         module = Driver()
  54         self.assertFormal(module, mode="bmc", depth=4)
  55     def test_ilang(self):
  56         dut = Driver()
  57         vl = rtlil.convert(dut, ports=[])
  58         with open("clz.il", "w") as f:
  59             f.write(vl)
  60
  61 if __name__ == '__main__':
  62     unittest.main()