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