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_mul_add.partpoints import PartitionPoints
  12 from ieee754.part.formal.proof_partition import GateGenerator
  13 from ieee754.part_cmp.eq_gt_ge import PartitionedEqGtGe
  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 = PartitionedEqGtGe(width, points)
  35         # post-process the output to ripple the LSB
  36         # TODO: remove this once PartitionedEqGtGe 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 PartitionedEqGtGe 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                 a = Signal(input_bit_width, name=f"a_{w}")
  64                 b = Signal(input_bit_width, name=f"b_{w}")
  65                 lsb = Signal(name=f"lsb_{w}")
  66                 comb += a.eq(p_a[:input_bit_width])
  67                 comb += b.eq(p_b[:input_bit_width])
  68                 with m.If(dut.opcode == PartitionedEqGtGe.EQ):
  69                     comb += lsb.eq(a == b)
  70                 with m.Elif(dut.opcode == PartitionedEqGtGe.GT):
  71                     comb += lsb.eq(a > b)
  72                 with m.Elif(dut.opcode == PartitionedEqGtGe.GE):
  73                     comb += lsb.eq(a >= b)
  74                 comb += expected.eq(Repl(lsb, output_bit_width))
  75                 # truncate the output, compare and assert
  76                 comb += Assert(p_output[:output_bit_width] == expected)
  77         # output an example
  78         # make the selected partition not start at the very beginning
  79         comb += Cover((p_offset != 0) & (p_width == 3) & (dut.a != dut.b))
  80         return m
  81
  82
  83 class PartitionedEqTestCase(FHDLTestCase):
  84
  85     def test_formal(self):
  86         traces = [
  87             ('p_offset[2:0]', {'base': 'dec'}),
  88             ('p_width[3:0]', {'base': 'dec'}),
  89             ('p_gates[8:0]', {'base': 'bin'}),
  90             ('dut', {'submodule': 'dut'}, [
  91                 ('gates[6:0]', {'base': 'bin'}),
  92                 'a[63:0]', 'b[63:0]',
  93                 ('output[7:0]', {'base': 'bin'})]),
  94             ('ripple', {'submodule': 'ripple'}, [
  95                 ('output[7:0]', {'base': 'bin'})]),
  96             ('p_output[7:0]', {'base': 'bin'}),
  97             ('expected_3[2:0]', {'base': 'bin'})]
  98         write_gtkw(
  99             'proof_partitioned_eq_gt_ge_cover.gtkw',
 100             os.path.dirname(__file__) +
 101             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace0.vcd',
 102             traces,
 103             module='top',
 104             zoom=-3
 105         )
 106         write_gtkw(
 107             'proof_partitioned_eq_gt_ge_bmc.gtkw',
 108             os.path.dirname(__file__) +
 109             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace.vcd',
 110             traces,
 111             module='top',
 112             zoom=-3
 113         )
 114         module = Driver()
 115         self.assertFormal(module, mode="bmc", depth=1)
 116         self.assertFormal(module, mode="cover", depth=1)
 117
 118
 119 if __name__ == '__main__':
 120     unittest.main()