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