src/ieee754/part_shift/formal/proof_shift_scalar.py

   1 # Proof of correctness for partitioned scalar 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_scalar import PartitionedScalarShift
  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 ShifterDriver(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         shifterwidth = 5
  36         mwidth = 3
  37
  38         # setup the inputs and outputs of the DUT as anyconst
  39         data = Signal(width)
  40         out = Signal(width)
  41         shifter = Signal(shifterwidth)
  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 += [data.eq(AnyConst(width)),
  50                  shifter.eq(AnyConst(shifterwidth)),
  51                  gates.eq(AnyConst(mwidth-1))]
  52
  53         m.submodules.dut = dut = PartitionedScalarShift(width, points)
  54
  55         data_intervals = self.get_intervals(data, points)
  56         out_intervals = self.get_intervals(out, points)
  57
  58         comb += [dut.data.eq(data),
  59                  dut.shifter.eq(shifter),
  60                  out.eq(dut.output)]
  61
  62         expected = Signal(width)
  63
  64         with m.Switch(points.as_sig()):
  65             with m.Case(0b00):
  66                 comb += Assert(
  67                     out[0:24] == (data[0:24] << (shifter & 0x1f)) & 0xffffff)
  68
  69             with m.Case(0b01):
  70                 comb += Assert(out[0:8] ==
  71                                (data[0:8] << (shifter & 0x7)) & 0xFF)
  72                 comb += Assert(out[8:24] ==
  73                                (data[8:24] << (shifter & 0xf)) & 0xffff)
  74
  75             with m.Case(0b10):
  76                 comb += Assert(out[16:24] ==
  77                                (data[16:24] << (shifter & 0x7)) & 0xff)
  78                 comb += Assert(out[0:16] ==
  79                                (data[0:16] << (shifter & 0xf)) & 0xffff)
  80
  81             with m.Case(0b11):
  82                 comb += Assert(out[0:8] ==
  83                                (data[0:8] << (shifter & 0x7)) & 0xFF)
  84                 comb += Assert(out[8:16] ==
  85                                (data[8:16] << (shifter & 0x7)) & 0xff)
  86                 comb += Assert(out[16:24] ==
  87                                (data[16:24] << (shifter & 0x7)) & 0xff)
  88         return m
  89
  90 class PartitionedScalarShiftTestCase(FHDLTestCase):
  91     def test_shift(self):
  92         module = ShifterDriver()
  93         self.assertFormal(module, mode="bmc", depth=4)
  94     def test_ilang(self):
  95         width = 24
  96         mwidth = 3
  97         gates = Signal(mwidth-1)
  98         points = PartitionPoints()
  99         step = int(width/mwidth)
 100         for i in range(mwidth-1):
 101             points[(i+1)*step] = gates[i]
 102         print(points)
 103         dut = PartitionedScalarShift(width, points)
 104         vl = rtlil.convert(dut, ports=[gates, dut.data,
 105                                        dut.shifter,
 106                                        dut.output])
 107         with open("scalar_shift.il", "w") as f:
 108             f.write(vl)
 109
 110 if __name__ == "__main__":
 111     unittest.main()