1 """Formal verification of partitioned operations
3 The approach is to take an arbitrary partition, by choosing its start point
4 and size at random. Use ``Assume`` to ensure it is a whole unbroken partition
5 (start and end points are one, with only zeros in between). Shift inputs and
6 outputs down to zero. Loop over all possible partition sizes and, if it's the
7 right size, compute the expected value, compare with the result, and assert.
9 We are turning the for-loops around (on their head), such that we start from
10 the *lengths* (and positions) and perform the ``Assume`` on the resultant
13 In other words, we have patterns as follows (assuming 32-bit words)::
20 * for 8-bit the partition bit is 1 and the previous is also 1
22 * for 16-bit the partition bit at the offset must be 0 and be surrounded by 1
24 * for 24-bit the partition bits at the offset and at offset+1 must be 0 and at
25 offset+2 and offset-1 must be 1
27 * for 32-bit all 3 bits must be 0 and be surrounded by 1 (guard bits are added
28 at each end for this purpose)
35 from nmigen
import Elaboratable
, Signal
, Module
, Const
36 from nmigen
.asserts
import Assert
, Cover
38 from nmutil
.formaltest
import FHDLTestCase
39 from nmutil
.gtkw
import write_gtkw
41 from ieee754
.part_mul_add
.partpoints
import PartitionPoints
44 class PartitionedPattern(Elaboratable
):
45 """ Generate a unique pattern, depending on partition size.
47 * 1-byte partitions: 0x11
48 * 2-byte partitions: 0x21 0x22
49 * 3-byte partitions: 0x31 0x32 0x33
53 Useful as a test vector for testing the formal prover
56 def __init__(self
, width
, partition_points
):
58 self
.partition_points
= PartitionPoints(partition_points
)
59 self
.mwidth
= len(self
.partition_points
)+1
60 self
.output
= Signal(self
.width
, reset_less
=True)
62 def elaborate(self
, platform
):
66 # Add a guard bit at each end
67 positions
= [0] + list(self
.partition_points
.keys()) + [self
.width
]
68 gates
= [Const(1)] + list(self
.partition_points
.values()) + [Const(1)]
69 # Begin counting at one
70 last_start
= positions
[0]
71 last_end
= positions
[1]
72 comb
+= self
.output
[last_start
:last_end
].eq(1)
73 # Build an incrementing cascade
74 for i
in range(1, self
.mwidth
):
77 # Propagate from the previous byte, adding one to it
79 comb
+= self
.output
[start
:end
].eq(
80 self
.output
[last_start
:last_end
] + 1)
82 # Unless it's a partition boundary, if so start again
83 comb
+= self
.output
[start
:end
].eq(1)
89 # This defines a module to drive the device under test and assert
90 # properties about its outputs
91 class Driver(Elaboratable
):
102 # Setup partition points and gates
103 points
= PartitionPoints()
104 gates
= Signal(mwidth
-1)
105 step
= int(width
/mwidth
)
106 for i
in range(mwidth
-1):
107 points
[(i
+1)*step
] = gates
[i
]
108 # Instantiate the partitioned pattern producer
109 m
.submodules
.dut
= dut
= PartitionedPattern(width
, points
)
110 # Directly check some cases
111 with m
.If(gates
== 0):
112 comb
+= Assert(dut
.output
== 0x0807060504030201)
113 with m
.If(gates
== 0b1100101):
114 comb
+= Assert(dut
.output
== 0x0101030201020101)
115 with m
.If(gates
== 0b0001000):
116 comb
+= Assert(dut
.output
== 0x0403020104030201)
117 with m
.If(gates
== 0b0100001):
118 comb
+= Assert(dut
.output
== 0x0201050403020101)
119 with m
.If(gates
== 0b1000001):
120 comb
+= Assert(dut
.output
== 0x0106050403020101)
121 with m
.If(gates
== 0b0000001):
122 comb
+= Assert(dut
.output
== 0x0706050403020101)
123 # Make it interesting, by having three partitions
124 comb
+= Cover(sum(gates
) == 3)
128 class PartitionTestCase(FHDLTestCase
):
129 def test_formal(self
):
130 traces
= ['output[63:0]']
132 'test_formal_cover.gtkw',
133 os
.path
.dirname(__file__
) +
134 '/proof_partition_formal/engine_0/trace0.vcd',
140 'test_formal_bmc.gtkw',
141 os
.path
.dirname(__file__
) +
142 '/proof_partition_formal/engine_0/trace.vcd',
148 self
.assertFormal(module
, mode
="bmc", depth
=1)
149 self
.assertFormal(module
, mode
="cover", depth
=1)
152 if __name__
== '__main__':