4 from nmigen
import Elaboratable
, Signal
, Module
, Repl
5 from nmigen
.asserts
import Assert
, Cover
7 from nmutil
.formaltest
import FHDLTestCase
8 from nmutil
.gtkw
import write_gtkw
9 from nmutil
.ripple
import RippleLSB
11 from ieee754
.part
.formal
.proof_partition
import GateGenerator
, make_partitions
12 from ieee754
.part_cmp
.experiments
.equal_ortree
import PartitionedEq
15 class Driver(Elaboratable
):
26 # Setup partition points and gates
27 step
= int(width
/mwidth
)
28 points
, gates
= make_partitions(step
, mwidth
)
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
41 # generate shifted down inputs and outputs
42 p_output
= Signal(mwidth
)
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
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
)
65 # make the selected partition not start at the very beginning
66 comb
+= Cover((p_offset
!= 0) & (p_width
== 3) & (dut
.a
!= dut
.b
))
70 class PartitionedEqTestCase(FHDLTestCase
):
72 def test_formal(self
):
74 'dec': {'base': 'dec'},
75 'bin': {'base': 'bin'}
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'),
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')]
90 'proof_partitioned_eq_cover.gtkw',
91 os
.path
.dirname(__file__
) +
92 '/proof_partitioned_eq_formal/engine_0/trace0.vcd',
98 'proof_partitioned_eq_bmc.gtkw',
99 os
.path
.dirname(__file__
) +
100 '/proof_partitioned_eq_formal/engine_0/trace.vcd',
106 self
.assertFormal(module
, mode
="bmc", depth
=1)
107 self
.assertFormal(module
, mode
="cover", depth
=1)
110 if __name__
== '__main__':