src/ieee754/part_cmp/experiments/formal/proof_gt.py

   1 # Proof of correctness for partitioned equal signal combiner
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import Module, Signal, Elaboratable, Mux
   5 from nmigen.asserts import Assert, AnyConst, Assume
   6 from nmigen.test.utils import FHDLTestCase
   7 from nmigen.cli import rtlil
   8
   9 from ieee754.part_cmp.experiments.gt_combiner import GTCombiner
  10 import unittest
  11
  12
  13 # This defines a module to drive the device under test and assert
  14 # properties about its outputs
  15 class CombinerDriver(Elaboratable):
  16     def __init__(self):
  17         # inputs and outputs
  18         pass
  19
  20     def elaborate(self, platform):
  21         m = Module()
  22         comb = m.d.comb
  23         width = 3
  24
  25         # setup the inputs and outputs of the DUT as anyconst
  26         eqs = Signal(width)
  27         gts = Signal(width)
  28         gates = Signal(width-1)
  29         out = Signal(width)
  30         mux_input = Signal()
  31         comb += [eqs.eq(AnyConst(width)),
  32                  gates.eq(AnyConst(width)),
  33                  gts.eq(AnyConst(width)),
  34                  mux_input.eq(AnyConst(1))]
  35
  36
  37         m.submodules.dut = dut = GTCombiner(width)
  38
  39
  40         # If the mux_input is 0, then this should work exactly as
  41         # described in
  42         # https://libre-riscv.org/3d_gpu/architecture/dynamic_simd/gt/
  43         # except for 2 gate bits, not 3
  44         with m.If(mux_input == 0):
  45             with m.Switch(gates):
  46                 with m.Case(0b11):
  47                     for i in range(out.width):
  48                         comb += Assert(out[i] == gts[i])
  49                 with m.Case(0b10):
  50                     comb += Assert(out[2] == gts[2])
  51                     comb += Assert(out[1] == 0)
  52                     comb += Assert(out[0] == (gts[0] | (eqs[0] & gts[1])))
  53                 with m.Case(0b01):
  54                     comb += Assert(out[2] == 0)
  55                     comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[2])))
  56                     comb += Assert(out[0] == gts[0])
  57                 with m.Case(0b00):
  58                     comb += Assert(out[2] == 0)
  59                     comb += Assert(out[1] == 0)
  60                     comb += Assert(out[0] == (gts[0] | (eqs[0] & (gts[1] | (eqs[1] & gts[2])))))
  61         # With the mux_input set to 1, this should work similarly to
  62         # eq_combiner. It appears this is the case, however the
  63         # ungated inputs are not set to 0 like they are in eq
  64         with m.Else():
  65             for i in range(gts.width):
  66                 comb += Assume(gts[i] == 0)
  67
  68             with m.Switch(gates):
  69                 with m.Case(0b11):
  70                     for i in range(out.width):
  71                         comb += Assert(out[i] == eqs[i])
  72                 with m.Case(0b00):
  73                     comb += Assert(out[0] == (eqs[0] & eqs[1] & eqs[2]))
  74                 with m.Case(0b10):
  75                     comb += Assert(out[0] == (eqs[0] & eqs[1]))
  76                     comb += Assert(out[2] == eqs[2])
  77                 with m.Case(0b01):
  78                     comb += Assert(out[0] == eqs[0])
  79                     comb += Assert(out[1] == (eqs[1] & eqs[2]))
  80
  81
  82
  83         # connect up the inputs and outputs.
  84         comb += dut.eqs.eq(eqs)
  85         comb += dut.gts.eq(gts)
  86         comb += dut.gates.eq(gates)
  87         comb += dut.mux_input.eq(mux_input)
  88         comb += out.eq(dut.outputs)
  89
  90         return m
  91
  92 class GTCombinerTestCase(FHDLTestCase):
  93     def test_gt_combiner(self):
  94         module = CombinerDriver()
  95         self.assertFormal(module, mode="bmc", depth=4)
  96     def test_ilang(self):
  97         dut = GTCombiner(3)
  98         vl = rtlil.convert(dut, ports=dut.ports())
  99         with open("partition_combiner.il", "w") as f:
 100             f.write(vl)
 101
 102
 103 if __name__ == '__main__':
 104     unittest.main()