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         comb += expected.eq(data << shifter)
  64
  65         with m.Switch(points.as_sig()):
  66             with m.Case(0b00):
  67                 comb += Assert(out[0:24] == (data[0:24] << shifter) & 0xffffff)
  68
  69             with m.Case(0b01):
  70                 comb += Assert(out[0:8] == expected[0:8])
  71                 comb += Assert(out[8:24] == (data[8:24] << shifter) & 0xffff)
  72
  73             with m.Case(0b10):
  74                 comb += Assert(out[16:24] == (data[16:24] << shifter) & 0xff)
  75                 comb += Assert(out[0:16] == (data[0:16] << shifter) & 0xffff)
  76
  77             with m.Case(0b11):
  78                 comb += Assert(out[0:8] == expected[0:8])
  79                 comb += Assert(out[8:16] == (data[8:16] << shifter) & 0xff)
  80                 comb += Assert(out[16:24] == (data[16:24] << shifter) & 0xff)
  81         return m
  82
  83 class PartitionedScalarShiftTestCase(FHDLTestCase):
  84     def test_shift(self):
  85         module = ShifterDriver()
  86         self.assertFormal(module, mode="bmc", depth=4)
  87
  88 if __name__ == "__main__":
  89     unittest.main()