switch to exact version of cython
[ieee754fpu.git] / 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.formal.proof_partition import GateGenerator, make_partitions
12 from ieee754.part_cmp.experiments.equal_ortree import PartitionedEq
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 = PartitionedEq(width, points)
31 # post-process the output to ripple the LSB
32 # TODO: remove this once PartitionedEq 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 PartitionedEq 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 comb += expected[0].eq(
60 p_a[:input_bit_width] == p_b[:input_bit_width])
61 comb += expected[1:].eq(Repl(expected[0], output_bit_width-1))
62 # truncate the output, compare and assert
63 comb += Assert(p_output[:output_bit_width] == expected)
64 # output an example
65 # make the selected partition not start at the very beginning
66 comb += Cover((p_offset != 0) & (p_width == 3) & (dut.a != dut.b))
67 return m
68
69
70 class PartitionedEqTestCase(FHDLTestCase):
71
72 def test_formal(self):
73 style = {
74 'dec': {'base': 'dec'},
75 'bin': {'base': 'bin'}
76 }
77 traces = [
78 ('p_offset[2:0]', 'dec'),
79 ('p_width[3:0]', 'dec'),
80 ('p_gates[8:0]', 'bin'),
81 ('dut', {'submodule': 'dut'}, [
82 ('gates[6:0]', 'bin'),
83 'a[63:0]', 'b[63:0]',
84 ('output[7:0]', 'bin')]),
85 ('ripple', {'submodule': 'ripple'}, [
86 ('output[7:0]', 'bin')]),
87 ('p_output[7:0]', 'bin'),
88 ('expected_3[2:0]', '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, style,
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, style,
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()