52c688b54f5d3797cf841ea8c06a24fa277b85a9
1 # Proof of correctness for partitioned equals module
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_mul_add
.partpoints
import PartitionPoints
10 from ieee754
.part_cmp
.equal_ortree
import PartitionedEq
14 # This defines a module to drive the device under test and assert
15 # properties about its outputs
16 class EqualsDriver(Elaboratable
):
21 def get_intervals(self
, signal
, points
):
24 keys
= list(points
.keys()) + [signal
.width
]
27 interval
.append(signal
[start
:end
])
31 def elaborate(self
, platform
):
37 # setup the inputs and outputs of the DUT as anyconst
40 points
= PartitionPoints()
41 gates
= Signal(mwidth
-1)
42 for i
in range(mwidth
-1):
43 points
[i
*4+4] = gates
[i
]
46 comb
+= [a
.eq(AnyConst(width
)),
47 b
.eq(AnyConst(width
)),
48 gates
.eq(AnyConst(mwidth
-1))]
50 m
.submodules
.dut
= dut
= PartitionedEq(width
, points
)
52 a_intervals
= self
.get_intervals(a
, points
)
53 b_intervals
= self
.get_intervals(b
, points
)
57 comb
+= Assert(out
== (a
== b
))
59 comb
+= Assert(out
[1] == ((a_intervals
[1] == b_intervals
[1]) &
60 (a_intervals
[2] == b_intervals
[2]) &
61 (a_intervals
[3] == b_intervals
[3])))
62 comb
+= Assert(out
[0] == (a_intervals
[0] == b_intervals
[0]))
64 comb
+= Assert(out
[2] == ((a_intervals
[2] == b_intervals
[2]) &
65 (a_intervals
[3] == b_intervals
[3])))
66 comb
+= Assert(out
[0] == ((a_intervals
[0] == b_intervals
[0]) &
67 (a_intervals
[1] == b_intervals
[1])))
69 comb
+= Assert(out
[2] == ((a_intervals
[2] == b_intervals
[2]) &
70 (a_intervals
[3] == b_intervals
[3])))
71 comb
+= Assert(out
[0] == (a_intervals
[0] == b_intervals
[0]))
72 comb
+= Assert(out
[1] == (a_intervals
[1] == b_intervals
[1]))
74 comb
+= Assert(out
[0] == ((a_intervals
[0] == b_intervals
[0]) &
75 (a_intervals
[1] == b_intervals
[1]) &
76 (a_intervals
[2] == b_intervals
[2])))
77 comb
+= Assert(out
[3] == (a_intervals
[3] == b_intervals
[3]))
79 comb
+= Assert(out
[1] == ((a_intervals
[1] == b_intervals
[1]) &
80 (a_intervals
[2] == b_intervals
[2])))
81 comb
+= Assert(out
[3] == (a_intervals
[3] == b_intervals
[3]))
82 comb
+= Assert(out
[0] == (a_intervals
[0] == b_intervals
[0]))
84 comb
+= Assert(out
[0] == ((a_intervals
[0] == b_intervals
[0]) &
85 (a_intervals
[1] == b_intervals
[1])))
86 comb
+= Assert(out
[3] == (a_intervals
[3] == b_intervals
[3]))
87 comb
+= Assert(out
[2] == (a_intervals
[2] == b_intervals
[2]))
89 for i
in range(mwidth
-1):
90 comb
+= Assert(out
[i
] == (a_intervals
[i
] == b_intervals
[i
]))
99 class PartitionedEqTestCase(FHDLTestCase
):
101 module
= EqualsDriver()
102 self
.assertFormal(module
, mode
="bmc", depth
=4)
104 if __name__
== "__main__":