src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py

   1 import os
   2 import unittest
   3
   4 from nmigen import Elaboratable, Signal, Module, Repl
   5 from nmigen.asserts import Assert, Cover
   6
   7 from nmutil.formaltest import FHDLTestCase
   8 from nmutil.gtkw import write_gtkw
   9 from nmutil.ripple import RippleLSB
  10
  11 from ieee754.part.formal.proof_partition import GateGenerator, make_partitions
  12 from ieee754.part_cmp.eq_gt_ge import PartitionedEqGtGe
  13
  14
  15 class Driver(Elaboratable):
  16     def __init__(self):
  17         # inputs and outputs
  18         pass
  19
  20     @staticmethod
  21     def elaborate(_):
  22         m = Module()
  23         comb = m.d.comb
  24         width = 64
  25         mwidth = 8
  26         # Setup partition points and gates
  27         step = int(width/mwidth)
  28         points, gates = make_partitions(step, mwidth)
  29         # instantiate the DUT
  30         m.submodules.dut = dut = PartitionedEqGtGe(width, points)
  31         # post-process the output to ripple the LSB
  32         # TODO: remove this once PartitionedEqGtGe is conformant
  33         m.submodules.ripple = ripple = RippleLSB(mwidth)
  34         comb += ripple.results_in.eq(dut.output)
  35         comb += ripple.gates.eq(gates)
  36         # instantiate the partitioned gate generator and connect the gates
  37         m.submodules.gen = gen = GateGenerator(mwidth)
  38         comb += gates.eq(gen.gates)
  39         p_offset = gen.p_offset
  40         p_width = gen.p_width
  41         # generate shifted down inputs and outputs
  42         p_output = Signal(mwidth)
  43         p_a = Signal(width)
  44         p_b = Signal(width)
  45         for pos in range(mwidth):
  46             with m.If(p_offset == pos):
  47                 # TODO: change to dut.output once PartitionedEqGtGe is conformant
  48                 comb += p_output.eq(ripple.output[pos:])
  49                 comb += p_a.eq(dut.a[pos * step:])
  50                 comb += p_b.eq(dut.b[pos * step:])
  51         # generate and check expected values for all possible partition sizes
  52         for w in range(1, mwidth+1):
  53             with m.If(p_width == w):
  54                 # calculate the expected output, for the given bit width,
  55                 # truncating the inputs to the partition size
  56                 input_bit_width = w * step
  57                 output_bit_width = w
  58                 expected = Signal(output_bit_width, name=f"expected_{w}")
  59                 a = Signal(input_bit_width, name=f"a_{w}")
  60                 b = Signal(input_bit_width, name=f"b_{w}")
  61                 lsb = Signal(name=f"lsb_{w}")
  62                 comb += a.eq(p_a[:input_bit_width])
  63                 comb += b.eq(p_b[:input_bit_width])
  64                 with m.If(dut.opcode == PartitionedEqGtGe.EQ):
  65                     comb += lsb.eq(a == b)
  66                 with m.Elif(dut.opcode == PartitionedEqGtGe.GT):
  67                     comb += lsb.eq(a > b)
  68                 with m.Elif(dut.opcode == PartitionedEqGtGe.GE):
  69                     comb += lsb.eq(a >= b)
  70                 comb += expected.eq(Repl(lsb, output_bit_width))
  71                 # truncate the output, compare and assert
  72                 comb += Assert(p_output[:output_bit_width] == expected)
  73         # output an example
  74         # make the selected partition not start at the very beginning
  75         comb += Cover((p_offset != 0) & (p_width == 3) & (dut.a != dut.b))
  76         return m
  77
  78
  79 class PartitionedEqTestCase(FHDLTestCase):
  80
  81     def test_formal(self):
  82         traces = [
  83             ('p_offset[2:0]', {'base': 'dec'}),
  84             ('p_width[3:0]', {'base': 'dec'}),
  85             ('p_gates[8:0]', {'base': 'bin'}),
  86             ('dut', {'submodule': 'dut'}, [
  87                 ('gates[6:0]', {'base': 'bin'}),
  88                 'a[63:0]', 'b[63:0]',
  89                 ('output[7:0]', {'base': 'bin'})]),
  90             ('ripple', {'submodule': 'ripple'}, [
  91                 ('output[7:0]', {'base': 'bin'})]),
  92             ('p_output[7:0]', {'base': 'bin'}),
  93             ('expected_3[2:0]', {'base': 'bin'})]
  94         write_gtkw(
  95             'proof_partitioned_eq_gt_ge_cover.gtkw',
  96             os.path.dirname(__file__) +
  97             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace0.vcd',
  98             traces,
  99             module='top',
 100             zoom=-3
 101         )
 102         write_gtkw(
 103             'proof_partitioned_eq_gt_ge_bmc.gtkw',
 104             os.path.dirname(__file__) +
 105             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace.vcd',
 106             traces,
 107             module='top',
 108             zoom=-3
 109         )
 110         module = Driver()
 111         self.assertFormal(module, mode="bmc", depth=1)
 112         self.assertFormal(module, mode="cover", depth=1)
 113
 114
 115 if __name__ == '__main__':
 116     unittest.main()