1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen
import Module
, Signal
, Elaboratable
, Mux
5 from nmigen
.asserts
import Assert
, AnyConst
, Assume
6 from nmigen
.test
.utils
import FHDLTestCase
7 from nmigen
.cli
import rtlil
9 from ieee754
.part_cmp
.experiments
.gt_combiner
import GTCombiner
13 # This defines a module to drive the device under test and assert
14 # properties about its outputs
15 class CombinerDriver(Elaboratable
):
20 def elaborate(self
, platform
):
25 # setup the inputs and outputs of the DUT as anyconst
28 gates
= Signal(width
-1)
31 comb
+= [eqs
.eq(AnyConst(width
)),
32 gates
.eq(AnyConst(width
)),
33 gts
.eq(AnyConst(width
)),
34 mux_input
.eq(AnyConst(1))]
37 m
.submodules
.dut
= dut
= GTCombiner(width
)
40 # If the mux_input is 0, then this should work exactly as
42 # https://libre-riscv.org/3d_gpu/architecture/dynamic_simd/gt/
43 # except for 2 gate bits, not 3
44 with m
.If(mux_input
== 0):
47 for i
in range(out
.width
):
48 comb
+= Assert(out
[i
] == gts
[i
])
50 comb
+= Assert(out
[2] == gts
[2])
51 comb
+= Assert(out
[1] == 0)
52 comb
+= Assert(out
[0] == (gts
[0] |
(eqs
[0] & gts
[1])))
54 comb
+= Assert(out
[2] == 0)
55 comb
+= Assert(out
[1] == (gts
[1] |
(eqs
[1] & gts
[2])))
56 comb
+= Assert(out
[0] == gts
[0])
58 comb
+= Assert(out
[2] == 0)
59 comb
+= Assert(out
[1] == 0)
60 comb
+= Assert(out
[0] == (gts
[0] |
(eqs
[0] & (gts
[1] |
(eqs
[1] & gts
[2])))))
61 # With the mux_input set to 1, this should work similarly to
62 # eq_combiner. It appears this is the case, however the
63 # ungated inputs are not set to 0 like they are in eq
65 for i
in range(gts
.width
):
66 comb
+= Assume(gts
[i
] == 0)
70 for i
in range(out
.width
):
71 comb
+= Assert(out
[i
] == eqs
[i
])
73 comb
+= Assert(out
[0] == (eqs
[0] & eqs
[1] & eqs
[2]))
75 comb
+= Assert(out
[0] == (eqs
[0] & eqs
[1]))
76 comb
+= Assert(out
[2] == eqs
[2])
78 comb
+= Assert(out
[0] == eqs
[0])
79 comb
+= Assert(out
[1] == (eqs
[1] & eqs
[2]))
83 # connect up the inputs and outputs.
84 comb
+= dut
.eqs
.eq(eqs
)
85 comb
+= dut
.gts
.eq(gts
)
86 comb
+= dut
.gates
.eq(gates
)
87 comb
+= dut
.mux_input
.eq(mux_input
)
88 comb
+= out
.eq(dut
.outputs
)
92 class GTCombinerTestCase(FHDLTestCase
):
93 def test_gt_combiner(self
):
94 module
= CombinerDriver()
95 self
.assertFormal(module
, mode
="bmc", depth
=4)
98 vl
= rtlil
.convert(dut
, ports
=dut
.ports())
99 with
open("partition_combiner.il", "w") as f
:
103 if __name__
== '__main__':