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[-1] == (a == b))
  61                 with m.Case(0b01):
  62                     comb += Assert(out[2] == ((a_intervals[1] == \
  63                                     b_intervals[1]) &
  64                                               (a_intervals[2] == \
  65                                     b_intervals[2])))
  66                     comb += Assert(out[0] == (a_intervals[0] == b_intervals[0]))
  67                 with m.Case(0b10):
  68                     comb += Assert(out[1] == ((a_intervals[0] == \
  69                                     b_intervals[0]) &
  70                                               (a_intervals[1] == \
  71                                     b_intervals[1])))
  72                     comb += Assert(out[2] == (a_intervals[2] == b_intervals[2]))
  73                 with m.Case(0b11):
  74                     for i in range(mwidth-1):
  75                         comb += Assert(out[i] == \
  76                                     (a_intervals[i] == b_intervals[i]))
  77         with m.If(opcode == 0b01):
  78             with m.Switch(gates):
  79                 with m.Case(0b00):
  80                     comb += Assert(out[-1] == (a > b))
  81                 with m.Case(0b01):
  82                     comb += Assert(out[0] == (a_intervals[0] > b_intervals[0]))
  83
  84                     comb += Assert(out[1] == 0)
  85                     comb += Assert(out[2] == (Cat(*a_intervals[1:3]) > \
  86                                     Cat(*b_intervals[1:3])))
  87                 with m.Case(0b10):
  88                     comb += Assert(out[0] == 0)
  89                     comb += Assert(out[1] == (Cat(*a_intervals[0:2]) > \
  90                                     Cat(*b_intervals[0:2])))
  91                     comb += Assert(out[2] == (a_intervals[2] > b_intervals[2]))
  92                 with m.Case(0b11):
  93                     for i in range(mwidth-1):
  94                         comb += Assert(out[i] == (a_intervals[i] > \
  95                                     b_intervals[i]))
  96         with m.If(opcode == 0b10):
  97             with m.Switch(gates):
  98                 with m.Case(0b00):
  99                     comb += Assert(out[-1] == (a >= b))
 100                 with m.Case(0b01):
 101                     comb += Assert(out[0] == (a_intervals[0] >= b_intervals[0]))
 102
 103                     comb += Assert(out[1] == 0)
 104                     comb += Assert(out[2] == (Cat(*a_intervals[1:3]) >= \
 105                                     Cat(*b_intervals[1:3])))
 106                 with m.Case(0b10):
 107                     comb += Assert(out[0] == 0)
 108                     comb += Assert(out[1] == (Cat(*a_intervals[0:2]) >= \
 109                                     Cat(*b_intervals[0:2])))
 110                     comb += Assert(out[2] == (a_intervals[2] >= b_intervals[2]))
 111                 with m.Case(0b11):
 112                     for i in range(mwidth-1):
 113                         comb += Assert(out[i] == \
 114                                     (a_intervals[i] >= b_intervals[i]))
 115
 116
 117
 118         comb += [dut.a.eq(a),
 119                  dut.b.eq(b),
 120                  dut.opcode.eq(opcode),
 121                  out.eq(dut.output)]
 122         return m
 123
 124 class PartitionedEqTestCase(FHDLTestCase):
 125     def test_eq(self):
 126         module = EqualsDriver()
 127         self.assertFormal(module, mode="bmc", depth=4)
 128
 129 if __name__ == "__main__":
 130     unittest.main()
 131