src/ieee754/part_shift/formal/proof_shift_dynamic.py

   1 # Proof of correctness for partitioned dynamic shifter
   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_shift.part_shift_dynamic import \
  11     PartitionedDynamicShift
  12 import unittest
  13
  14
  15 # This defines a module to drive the device under test and assert
  16 # properties about its outputs
  17 class ShifterDriver(Elaboratable):
  18     def __init__(self):
  19         # inputs and outputs
  20         pass
  21
  22     def get_intervals(self, signal, points):
  23         start = 0
  24         interval = []
  25         keys = list(points.keys()) + [signal.width]
  26         for key in keys:
  27             end = key
  28             interval.append(signal[start:end])
  29             start = end
  30         return interval
  31
  32     def elaborate(self, platform):
  33         m = Module()
  34         comb = m.d.comb
  35         width = 24
  36         mwidth = 3
  37
  38         # setup the inputs and outputs of the DUT as anyconst
  39         a = Signal(width)
  40         b = Signal(width)
  41         out = Signal(width)
  42         points = PartitionPoints()
  43         gates = Signal(mwidth-1)
  44         step = int(width/mwidth)
  45         for i in range(mwidth-1):
  46             points[(i+1)*step] = gates[i]
  47         print(points)
  48
  49         comb += [a.eq(AnyConst(width)),
  50                  b.eq(AnyConst(width)),
  51                  gates.eq(AnyConst(mwidth-1))]
  52
  53         m.submodules.dut = dut = PartitionedDynamicShift(width, points)
  54
  55         a_intervals = self.get_intervals(a, points)
  56         b_intervals = self.get_intervals(b, points)
  57         out_intervals = self.get_intervals(out, points)
  58
  59         comb += [dut.a.eq(a),
  60                  dut.b.eq(b),
  61                  out.eq(dut.output)]
  62
  63
  64         with m.Switch(points.as_sig()):
  65             with m.Case(0b00):
  66                 comb += Assume(b < 24)
  67                 comb += Assert(out == (a<<b[0:5]) & 0xffffff)
  68             with m.Case(0b01):
  69                 comb += Assume(b_intervals[0] <= 8)
  70                 comb += Assert(out_intervals[0] ==
  71                                (a_intervals[0]<<b_intervals[0]) & 0xff)
  72                 comb += Assume(b_intervals[1] <= 16)
  73                 comb += Assert(Cat(out_intervals[1:3]) ==
  74                                (Cat(a_intervals[1:3])
  75                                 <<b_intervals[1]) & 0xffff)
  76             with m.Case(0b10):
  77                 comb += Assume(b_intervals[0] <= 16)
  78                 comb += Assert(Cat(out_intervals[0:2]) ==
  79                                (Cat(a_intervals[0:2])
  80                                 <<b_intervals[0]) & 0xffff)
  81                 comb += Assume(b_intervals[2] <= 16)
  82                 comb += Assert(out_intervals[2] ==
  83                                (a_intervals[2]<<b_intervals[2]) & 0xff)
  84             with m.Case(0b11):
  85                 for i, o in enumerate(out_intervals):
  86                     comb += Assume(b_intervals[i] < 8)
  87                     comb += Assert(o ==
  88                                    (a_intervals[i] << b_intervals[i]) & 0xff)
  89
  90         return m
  91
  92 class PartitionedDynamicShiftTestCase(FHDLTestCase):
  93     def test_shift(self):
  94         module = ShifterDriver()
  95         self.assertFormal(module, mode="bmc", depth=4)
  96     def test_ilang(self):
  97         width = 64
  98         mwidth = 8
  99         gates = Signal(mwidth-1)
 100         points = PartitionPoints()
 101         step = int(width/mwidth)
 102         for i in range(mwidth-1):
 103             points[(i+1)*step] = gates[i]
 104         print(points)
 105         dut = PartitionedDynamicShift(width, points)
 106         vl = rtlil.convert(dut, ports=[gates, dut.a, dut.b, dut.output])
 107         with open("dynamic_shift.il", "w") as f:
 108             f.write(vl)
 109
 110
 111 if __name__ == "__main__":
 112     unittest.main()
 113