src/ieee754/part_cmp/formal/proof_eq_gt_ge.py

   1 # Proof of correctness for partitioned equals module
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import Module, Signal, Elaboratable, Mux, Cat
   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_mul_add.partpoints import PartitionPoints
  10 from ieee754.part_cmp.eq_gt_ge import PartitionedEqGtGe
  11 import unittest
  12
  13
  14 # This defines a module to drive the device under test and assert
  15 # properties about its outputs
  16 class EqualsDriver(Elaboratable):
  17     def __init__(self):
  18         # inputs and outputs
  19         pass
  20
  21     def get_intervals(self, signal, points):
  22         start = 0
  23         interval = []
  24         keys = list(points.keys()) + [signal.width]
  25         for key in keys:
  26             end = key
  27             interval.append(signal[start:end])
  28             start = end
  29         return interval
  30
  31     def elaborate(self, platform):
  32         m = Module()
  33         comb = m.d.comb
  34         width = 24
  35         mwidth = 3
  36
  37         # setup the inputs and outputs of the DUT as anyconst
  38         a = Signal(width)
  39         b = Signal(width)
  40         points = PartitionPoints()
  41         gates = Signal(mwidth-1)
  42         opcode = Signal(2)
  43         for i in range(mwidth-1):
  44             points[i*8+8] = gates[i]
  45         out = Signal(mwidth)
  46
  47         comb += [a.eq(AnyConst(width)),
  48                  b.eq(AnyConst(width)),
  49                  opcode.eq(AnyConst(opcode.width)),
  50                  gates.eq(AnyConst(mwidth-1))]
  51
  52         m.submodules.dut = dut = PartitionedEqGtGe(width, points)
  53
  54         a_intervals = self.get_intervals(a, points)
  55         b_intervals = self.get_intervals(b, points)
  56
  57         with m.If(opcode == 0b00):
  58             with m.Switch(gates):
  59                 with m.Case(0b00):
  60                     comb += Assert(out[0] == (a == b))
  61                     comb += Assert(out[1] == 0)
  62                     comb += Assert(out[2] == 0)
  63                 with m.Case(0b01):
  64                     comb += Assert(out[0] == (a_intervals[0] == b_intervals[0]))
  65                     comb += Assert(out[1] == ((a_intervals[1] == \
  66                                     b_intervals[1]) &
  67                                               (a_intervals[2] == \
  68                                     b_intervals[2])))
  69                     comb += Assert(out[2] == 0)
  70                 with m.Case(0b10):
  71                     comb += Assert(out[0] == ((a_intervals[0] == \
  72                                     b_intervals[0]) &
  73                                               (a_intervals[1] == \
  74                                     b_intervals[1])))
  75                     comb += Assert(out[1] == 0)
  76                     comb += Assert(out[2] == (a_intervals[2] == b_intervals[2]))
  77                 with m.Case(0b11):
  78                     for i in range(mwidth-1):
  79                         comb += Assert(out[i] == \
  80                                     (a_intervals[i] == b_intervals[i]))
  81         with m.If(opcode == 0b01):
  82             with m.Switch(gates):
  83                 with m.Case(0b00):
  84                     comb += Assert(out == (a > b))
  85                 with m.Case(0b01):
  86                     comb += Assert(out[0] == (a_intervals[0] > b_intervals[0]))
  87
  88                     comb += Assert(out[1] == (Cat(*a_intervals[1:3]) > \
  89                                               Cat(*b_intervals[1:3])))
  90                     comb += Assert(out[2] == 0)
  91                 with m.Case(0b10):
  92                     comb += Assert(out[0] == (Cat(*a_intervals[0:2]) > \
  93                                               Cat(*b_intervals[0:2])))
  94                     comb += Assert(out[1] == 0)
  95                     comb += Assert(out[2] == (a_intervals[2] > b_intervals[2]))
  96                 with m.Case(0b11):
  97                     for i in range(mwidth-1):
  98                         comb += Assert(out[i] == (a_intervals[i] > \
  99                                                   b_intervals[i]))
 100         with m.If(opcode == 0b10):
 101             with m.Switch(gates):
 102                 with m.Case(0b00):
 103                     comb += Assert(out == (a >= b))
 104                 with m.Case(0b01):
 105                     comb += Assert(out[0] == (a_intervals[0] >= b_intervals[0]))
 106
 107                     comb += Assert(out[1] == (Cat(*a_intervals[1:3]) >= \
 108                                               Cat(*b_intervals[1:3])))
 109                     comb += Assert(out[2] == 0)
 110                 with m.Case(0b10):
 111                     comb += Assert(out[0] == (Cat(*a_intervals[0:2]) >= \
 112                                               Cat(*b_intervals[0:2])))
 113                     comb += Assert(out[1] == 0)
 114                     comb += Assert(out[2] == (a_intervals[2] >= b_intervals[2]))
 115                 with m.Case(0b11):
 116                     for i in range(mwidth-1):
 117                         comb += Assert(out[i] == \
 118                                        (a_intervals[i] >= b_intervals[i]))
 119
 120
 121
 122         comb += [dut.a.eq(a),
 123                  dut.b.eq(b),
 124                  dut.opcode.eq(opcode),
 125                  out.eq(dut.output)]
 126         return m
 127
 128 class PartitionedEqTestCase(FHDLTestCase):
 129     def test_eq(self):
 130         module = EqualsDriver()
 131         self.assertFormal(module, mode="bmc", depth=4)
 132
 133 if __name__ == "__main__":
 134     unittest.main()
 135