534e9e549d53cfc0bf4cb78f7093e62f5a9f1c36
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)
36 from nmigen
import Elaboratable
, Signal
, Module
, Const
, Repl
37 from nmigen
.asserts
import Assert
, Cover
38 from nmigen
.hdl
.ast
import Assume
40 from nmutil
.formaltest
import FHDLTestCase
41 from nmutil
.gtkw
import write_gtkw
43 from ieee754
.part_mul_add
.partpoints
import PartitionPoints
44 from ieee754
.part
.partsig
import PartitionedSignal
47 class PartitionedPattern(Elaboratable
):
48 """ Generate a unique pattern, depending on partition size.
50 * 1-byte partitions: 0x11
51 * 2-byte partitions: 0x21 0x22
52 * 3-byte partitions: 0x31 0x32 0x33
56 Useful as a test vector for testing the formal prover
59 def __init__(self
, width
, partition_points
):
61 self
.partition_points
= PartitionPoints(partition_points
)
62 self
.mwidth
= len(self
.partition_points
)+1
63 self
.output
= Signal(self
.width
, reset_less
=True)
65 def elaborate(self
, platform
):
69 # Add a guard bit at each end
70 positions
= [0] + list(self
.partition_points
.keys()) + [self
.width
]
71 gates
= [Const(1)] + list(self
.partition_points
.values()) + [Const(1)]
72 # Begin counting at one
73 last_start
= positions
[0]
74 last_end
= positions
[1]
75 last_middle
= (last_start
+last_end
)//2
76 comb
+= self
.output
[last_start
:last_middle
].eq(1)
77 # Build an incrementing cascade
78 for i
in range(1, self
.mwidth
):
81 middle
= (start
+ end
) // 2
82 # Propagate from the previous byte, adding one to it.
84 comb
+= self
.output
[start
:middle
].eq(
85 self
.output
[last_start
:last_middle
] + 1)
87 # ... unless it's a partition boundary. If so, start again.
88 comb
+= self
.output
[start
:middle
].eq(1)
91 # Mirror the nibbles on the last byte
92 last_start
= positions
[-2]
93 last_end
= positions
[-1]
94 last_middle
= (last_start
+last_end
)//2
95 comb
+= self
.output
[last_middle
:last_end
].eq(
96 self
.output
[last_start
:last_middle
])
97 for i
in range(self
.mwidth
, 0, -1):
98 start
= positions
[i
-1]
100 middle
= (start
+ end
) // 2
101 # Propagate from the previous byte.
102 with m
.If(~gates
[i
]):
103 comb
+= self
.output
[middle
:end
].eq(
104 self
.output
[last_middle
:last_end
])
106 # ... unless it's a partition boundary.
107 # If so, mirror the nibbles again.
108 comb
+= self
.output
[middle
:end
].eq(
109 self
.output
[start
:middle
])
116 def make_partitions(step
, mwidth
):
117 """Make equally spaced partition points
119 :param step: smallest partition width
120 :param mwidth: maximum number of partitions
121 :returns: partition points, and corresponding gates"""
122 gates
= Signal(mwidth
- 1)
123 points
= PartitionPoints()
124 for i
in range(mwidth
-1):
125 points
[(i
+ 1) * step
] = gates
[i
]
129 # This defines a module to drive the device under test and assert
130 # properties about its outputs
131 class Driver(Elaboratable
):
142 # Setup partition points and gates
143 step
= int(width
/mwidth
)
144 points
, gates
= make_partitions(step
, mwidth
)
145 # Instantiate the partitioned pattern producer
146 m
.submodules
.dut
= dut
= PartitionedPattern(width
, points
)
147 # Directly check some cases
148 with m
.If(gates
== 0):
149 comb
+= Assert(dut
.output
== 0x_88_87_86_85_84_83_82_81)
150 with m
.If(gates
== 0b1100101):
151 comb
+= Assert(dut
.output
== 0x_11_11_33_32_31_22_21_11)
152 with m
.If(gates
== 0b0001000):
153 comb
+= Assert(dut
.output
== 0x_44_43_42_41_44_43_42_41)
154 with m
.If(gates
== 0b0100001):
155 comb
+= Assert(dut
.output
== 0x_22_21_55_54_53_52_51_11)
156 with m
.If(gates
== 0b1000001):
157 comb
+= Assert(dut
.output
== 0x_11_66_65_64_63_62_61_11)
158 with m
.If(gates
== 0b0000001):
159 comb
+= Assert(dut
.output
== 0x_77_76_75_74_73_72_71_11)
160 # Choose a partition offset and width at random.
161 p_offset
= Signal(range(mwidth
))
162 p_width
= Signal(range(mwidth
+1))
163 p_finish
= Signal(range(mwidth
+1))
164 comb
+= p_finish
.eq(p_offset
+ p_width
)
165 # Partition must not be empty, and fit within the signal.
166 comb
+= Assume(p_width
!= 0)
167 comb
+= Assume(p_offset
+ p_width
<= mwidth
)
169 # Build the corresponding partition
170 # Use Assume to constraint the pattern to conform to the given offset
171 # and width. For each gate bit it is:
172 # 1) one, if on the partition boundary
173 # 2) zero, if it's inside the partition
174 # 3) don't care, otherwise
175 p_gates
= Signal(mwidth
+1)
176 for i
in range(mwidth
+1):
177 with m
.If(i
== p_offset
):
178 # Partitions begin with 1
179 comb
+= Assume(p_gates
[i
] == 1)
180 with m
.If((i
> p_offset
) & (i
< p_finish
)):
181 # The interior are all zeros
182 comb
+= Assume(p_gates
[i
] == 0)
183 with m
.If(i
== p_finish
):
185 comb
+= Assume(p_gates
[i
] == 1)
186 # Check some possible partitions generating a given pattern
187 with m
.If(p_gates
== 0b0100110):
188 comb
+= Assert(((p_offset
== 1) & (p_width
== 1)) |
189 ((p_offset
== 2) & (p_width
== 3)))
190 # Remove guard bits at each end and assign to the DUT gates
191 comb
+= gates
.eq(p_gates
[1:])
192 # Generate shifted down outputs:
193 p_output
= Signal(width
)
194 positions
= [0] + list(points
.keys()) + [width
]
195 for i
in range(mwidth
):
196 with m
.If(p_offset
== i
):
197 comb
+= p_output
.eq(dut
.output
[positions
[i
]:])
198 # Some checks on the shifted down output, irrespective of offset:
199 with m
.If(p_width
== 2):
200 comb
+= Assert(p_output
[:16] == 0x_22_21)
201 with m
.If(p_width
== 4):
202 comb
+= Assert(p_output
[:32] == 0x_44_43_42_41)
204 with m
.If(p_offset
== 0):
205 comb
+= Assert(p_output
== dut
.output
)
207 # Make it interesting, by having four partitions.
208 # Make the selected partition not start at the very beginning.
209 comb
+= Cover((sum(gates
) == 3) & (p_offset
!= 0) & (p_width
== 3))
210 # Generate and check expected values for all possible partition sizes.
211 # Here, we assume partition sizes are multiple of the smaller size.
212 for w
in range(1, mwidth
+1):
213 with m
.If(p_width
== w
):
214 # calculate the expected output, for the given bit width
216 expected
= Signal(bit_width
, name
=f
"expected_{w}")
218 # lower nibble is the position
219 comb
+= expected
[b
*8:b
*8+4].eq(b
+1)
220 # upper nibble is the partition width
221 comb
+= expected
[b
*8+4:b
*8+8].eq(w
)
222 # truncate the output, compare and assert
223 comb
+= Assert(p_output
[:bit_width
] == expected
)
227 class GateGenerator(Elaboratable
):
228 """Produces partition gates at random
230 `p_offset`, `p_width` and `p_finish` describe the selected partition
232 def __init__(self
, mwidth
):
234 """Number of partitions"""
235 self
.gates
= Signal(mwidth
-1)
236 """Generated partition gates"""
237 self
.p_offset
= Signal(range(mwidth
))
238 """Generated partition start point"""
239 self
.p_width
= Signal(range(mwidth
+1))
240 """Generated partition width"""
241 self
.p_finish
= Signal(range(mwidth
+1))
242 """Generated partition end point"""
244 def elaborate(self
, _
):
249 p_offset
= self
.p_offset
250 p_width
= self
.p_width
251 p_finish
= self
.p_finish
252 comb
+= p_finish
.eq(p_offset
+ p_width
)
253 # Partition must not be empty, and fit within the signal.
254 comb
+= Assume(p_width
!= 0)
255 comb
+= Assume(p_offset
+ p_width
<= mwidth
)
257 # Build the corresponding partition
258 # Use Assume to constraint the pattern to conform to the given offset
259 # and width. For each gate bit it is:
260 # 1) one, if on the partition boundary
261 # 2) zero, if it's inside the partition
262 # 3) don't care, otherwise
263 p_gates
= Signal(mwidth
+1)
264 for i
in range(mwidth
+1):
265 with m
.If(i
== p_offset
):
266 # Partitions begin with 1
267 comb
+= Assume(p_gates
[i
] == 1)
268 with m
.If((i
> p_offset
) & (i
< p_finish
)):
269 # The interior are all zeros
270 comb
+= Assume(p_gates
[i
] == 0)
271 with m
.If(i
== p_finish
):
273 comb
+= Assume(p_gates
[i
] == 1)
274 # Remove guard bits at each end, before assigning to the output gates
275 comb
+= gates
.eq(p_gates
[1:])
279 class GeneratorDriver(Elaboratable
):
290 # Setup partition points and gates
291 step
= int(width
/mwidth
)
292 points
, gates
= make_partitions(step
, mwidth
)
293 # Instantiate the partitioned pattern producer and the DUT
294 m
.submodules
.dut
= dut
= PartitionedPattern(width
, points
)
295 m
.submodules
.gen
= gen
= GateGenerator(mwidth
)
296 comb
+= gates
.eq(gen
.gates
)
297 # Generate shifted down outputs
298 p_offset
= gen
.p_offset
299 p_width
= gen
.p_width
300 p_output
= Signal(width
)
301 for i
in range(mwidth
):
302 with m
.If(p_offset
== i
):
303 comb
+= p_output
.eq(dut
.output
[i
*step
:])
304 # Generate and check expected values for all possible partition sizes.
305 for w
in range(1, mwidth
+1):
306 with m
.If(p_width
== w
):
307 # calculate the expected output, for the given bit width
309 expected
= Signal(bit_width
, name
=f
"expected_{w}")
311 # lower nibble is the position
312 comb
+= expected
[b
*8:b
*8+4].eq(b
+1)
313 # upper nibble is the partition width
314 comb
+= expected
[b
*8+4:b
*8+8].eq(w
)
315 # truncate the output, compare and assert
316 comb
+= Assert(p_output
[:bit_width
] == expected
)
318 # Make it interesting, by having four partitions.
319 # Make the selected partition not start at the very beginning.
320 comb
+= Cover((sum(gates
) == 3) & (p_offset
!= 0) & (p_width
== 3))
324 class OpDriver(Elaboratable
):
325 """Checks operations on partitioned signals"""
326 def __init__(self
, op
, width
=64, mwidth
=8, nops
=2, part_out
=True):
328 """Operation to perform"""
330 """Partition full width"""
332 """Maximum number of equally sized partitions"""
334 """Number of input operands"""
335 self
.part_out
= part_out
336 """True if output is partition-like"""
337 def elaborate(self
, _
):
343 part_out
= self
.part_out
344 # setup partition points and gates
345 step
= int(width
/mwidth
)
346 points
, gates
= make_partitions(step
, mwidth
)
347 # setup inputs and outputs
349 for i
in range(nops
):
350 inp
= PartitionedSignal(points
, width
, name
=f
"i_{i+1}")
359 output
= Signal(out_width
)
360 # perform the operation on the partitioned signals
361 result
= self
.op(*operands
)
362 if isinstance(result
, PartitionedSignal
):
363 comb
+= output
.eq(result
.sig
)
364 # TODO: remove when all operations return PartitionedSignal
366 comb
+= output
.eq(result
)
367 # instantiate the partitioned gate generator and connect the gates
368 m
.submodules
.gen
= gen
= GateGenerator(mwidth
)
369 comb
+= gates
.eq(gen
.gates
)
370 p_offset
= gen
.p_offset
371 p_width
= gen
.p_width
372 # generate shifted down inputs and outputs
374 for i
in range(nops
):
375 p_i
= Signal(width
, name
=f
"p_{i+1}")
376 p_operands
.append(p_i
)
377 for pos
in range(mwidth
):
378 with m
.If(p_offset
== pos
):
379 comb
+= p_i
.eq(operands
[i
].sig
[pos
* step
:])
380 p_output
= Signal(out_width
)
381 for pos
in range(mwidth
):
382 with m
.If(p_offset
== pos
):
383 comb
+= p_output
.eq(output
[pos
* out_step
:])
384 # generate and check expected values for all possible partition sizes
385 all_operands_non_zero
= Signal()
386 for w
in range(1, mwidth
+1):
387 with m
.If(p_width
== w
):
388 # calculate the expected output, for the given bit width,
389 # truncating the inputs to the partition size
390 input_bit_width
= w
* step
391 output_bit_width
= w
* out_step
392 expected
= Signal(output_bit_width
, name
=f
"expected_{w}")
393 trunc_operands
= list()
394 for i
in range(nops
):
395 t_i
= Signal(input_bit_width
, name
=f
"t{w}_{i+1}")
396 trunc_operands
.append(t_i
)
397 comb
+= t_i
.eq(p_operands
[i
][:input_bit_width
])
399 # for partition-like outputs, calculate the LSB
400 # and replicate it on the partition
401 lsb
= Signal(name
=f
"lsb_{w}")
402 comb
+= lsb
.eq(self
.op(*trunc_operands
))
403 comb
+= expected
.eq(Repl(lsb
, output_bit_width
))
405 # otherwise, just take the operation result
406 comb
+= expected
.eq(self
.op(*trunc_operands
))
407 # truncate the output, compare and assert
408 comb
+= Assert(p_output
[:output_bit_width
] == expected
)
409 # ensure a test case with all non-zero operands
410 non_zero_op
= Signal(nops
)
411 for i
in range(nops
):
412 comb
+= non_zero_op
[i
].eq(trunc_operands
[i
].any())
413 comb
+= all_operands_non_zero
.eq(non_zero_op
.all())
415 comb
+= Cover((p_offset
!= 0) & (p_width
== 3) & (sum(output
) > 1) &
416 (p_output
!= 0) & all_operands_non_zero
)
420 class PartitionTestCase(FHDLTestCase
):
421 def test_formal(self
):
423 'dec': {'base': 'dec'},
424 'bin': {'base': 'bin'}
427 ('p_offset[2:0]', 'dec'),
428 ('p_width[3:0]', 'dec'),
429 ('p_finish[3:0]', 'dec'),
430 ('p_gates[8:0]', 'bin'),
431 ('dut', {'submodule': 'dut'}, [
432 ('gates[6:0]', 'bin'),
434 'p_output[63:0]', 'expected_3[21:0]']
436 'proof_partition_cover.gtkw',
437 os
.path
.dirname(__file__
) +
438 '/proof_partition_formal/engine_0/trace0.vcd',
444 'proof_partition_bmc.gtkw',
445 os
.path
.dirname(__file__
) +
446 '/proof_partition_formal/engine_0/trace.vcd',
452 self
.assertFormal(module
, mode
="bmc", depth
=1)
453 self
.assertFormal(module
, mode
="cover", depth
=1)
455 def test_generator(self
):
457 'dec': {'base': 'dec'},
458 'bin': {'base': 'bin'}
461 ('p_offset[2:0]', 'dec'),
462 ('p_width[3:0]', 'dec'),
463 ('p_finish[3:0]', 'dec'),
464 ('p_gates[8:0]', 'bin'),
465 ('dut', {'submodule': 'dut'}, [
466 ('gates[6:0]', 'bin'),
468 'p_output[63:0]', 'expected_3[21:0]',
469 'a_3[23:0]', 'b_3[32:0]', 'expected_3[2:0]']
471 'proof_partition_generator_cover.gtkw',
472 os
.path
.dirname(__file__
) +
473 '/proof_partition_generator/engine_0/trace0.vcd',
479 'proof_partition_generator_bmc.gtkw',
480 os
.path
.dirname(__file__
) +
481 '/proof_partition_generator/engine_0/trace.vcd',
486 module
= GeneratorDriver()
487 self
.assertFormal(module
, mode
="bmc", depth
=1)
488 self
.assertFormal(module
, mode
="cover", depth
=1)
490 def test_partsig_eq(self
):
492 'dec': {'base': 'dec'},
493 'bin': {'base': 'bin'}
496 ('p_offset[2:0]', 'dec'),
497 ('p_width[3:0]', 'dec'),
498 ('p_gates[8:0]', 'bin'),
499 'i_1[63:0]', 'i_2[63:0]',
500 ('eq_1', {'submodule': 'eq_1'}, [
501 ('gates[6:0]', 'bin'),
502 'a[63:0]', 'b[63:0]',
503 ('output[7:0]', 'bin')]),
504 'p_1[63:0]', 'p_2[63:0]',
505 ('p_output[7:0]', 'bin'),
506 't3_1[23:0]', 't3_2[23:0]', 'lsb_3',
507 ('expected_3[2:0]', 'bin')]
509 'proof_partsig_eq_cover.gtkw',
510 os
.path
.dirname(__file__
) +
511 '/proof_partition_partsig_eq/engine_0/trace0.vcd',
517 'proof_partsig_eq_bmc.gtkw',
518 os
.path
.dirname(__file__
) +
519 '/proof_partition_partsig_eq/engine_0/trace.vcd',
524 module
= OpDriver(operator
.eq
)
525 self
.assertFormal(module
, mode
="bmc", depth
=1)
526 self
.assertFormal(module
, mode
="cover", depth
=1)
528 def test_partsig_ne(self
):
529 module
= OpDriver(operator
.ne
)
530 self
.assertFormal(module
, mode
="bmc", depth
=1)
532 def test_partsig_gt(self
):
533 module
= OpDriver(operator
.gt
)
534 self
.assertFormal(module
, mode
="bmc", depth
=1)
536 def test_partsig_ge(self
):
537 module
= OpDriver(operator
.ge
)
538 self
.assertFormal(module
, mode
="bmc", depth
=1)
540 def test_partsig_lt(self
):
541 module
= OpDriver(operator
.lt
)
542 self
.assertFormal(module
, mode
="bmc", depth
=1)
544 def test_partsig_le(self
):
545 module
= OpDriver(operator
.le
)
546 self
.assertFormal(module
, mode
="bmc", depth
=1)
548 def test_partsig_all(self
):
550 'dec': {'base': 'dec'},
551 'bin': {'base': 'bin'}
554 ('p_offset[2:0]', 'dec'),
555 ('p_width[3:0]', 'dec'),
556 ('p_gates[8:0]', 'bin'),
558 ('eq_1', {'submodule': 'eq_1'}, [
559 ('gates[6:0]', 'bin'),
560 'a[63:0]', 'b[63:0]',
561 ('output[7:0]', 'bin')]),
563 ('p_output[7:0]', 'bin'),
564 't3_1[23:0]', 'lsb_3',
565 ('expected_3[2:0]', 'bin')]
567 'proof_partsig_all_cover.gtkw',
568 os
.path
.dirname(__file__
) +
569 '/proof_partition_partsig_all/engine_0/trace0.vcd',
578 module
= OpDriver(op_all
, nops
=1)
579 self
.assertFormal(module
, mode
="bmc", depth
=1)
580 self
.assertFormal(module
, mode
="cover", depth
=1)
582 def test_partsig_any(self
):
587 module
= OpDriver(op_any
, nops
=1)
588 self
.assertFormal(module
, mode
="bmc", depth
=1)
590 def test_partsig_xor(self
):
595 module
= OpDriver(op_xor
, nops
=1)
596 # yices2 is slow on this test for some reason
598 self
.assertFormal(module
, mode
="bmc", depth
=1, solver
="z3")
600 def test_partsig_add(self
):
602 'dec': {'base': 'dec'},
603 'bin': {'base': 'bin'}
606 ('p_offset[2:0]', 'dec'),
607 ('p_width[3:0]', 'dec'),
608 ('p_gates[8:0]', 'bin'),
609 'i_1[63:0]', 'i_2[63:0]',
610 ('add_1', {'submodule': 'add_1'}, [
611 ('gates[6:0]', 'bin'),
612 'a[63:0]', 'b[63:0]',
614 'p_1[63:0]', 'p_2[63:0]',
616 't3_1[23:0]', 't3_2[23:0]',
619 'proof_partsig_add_cover.gtkw',
620 os
.path
.dirname(__file__
) +
621 '/proof_partition_partsig_add/engine_0/trace0.vcd',
627 module
= OpDriver(operator
.add
, part_out
=False)
628 self
.assertFormal(module
, mode
="bmc", depth
=1)
629 self
.assertFormal(module
, mode
="cover", depth
=1)
631 def test_partsig_sub(self
):
632 module
= OpDriver(operator
.sub
, part_out
=False)
633 self
.assertFormal(module
, mode
="bmc", depth
=1)
635 def test_partsig_neg(self
):
637 'dec': {'base': 'dec'},
638 'bin': {'base': 'bin'}
641 ('p_offset[2:0]', 'dec'),
642 ('p_width[3:0]', 'dec'),
643 ('p_gates[8:0]', 'bin'),
645 ('add_1', {'submodule': 'add_1'}, [
646 ('gates[6:0]', 'bin'),
647 'a[63:0]', 'b[63:0]',
654 'proof_partsig_neg_bmc.gtkw',
655 os
.path
.dirname(__file__
) +
656 '/proof_partition_partsig_neg/engine_0/trace.vcd',
662 module
= OpDriver(operator
.neg
, nops
=1, part_out
=False)
663 self
.assertFormal(module
, mode
="bmc", depth
=1)
665 def test_partsig_and(self
):
666 module
= OpDriver(operator
.and_
, part_out
=False)
667 self
.assertFormal(module
, mode
="bmc", depth
=1)
669 def test_partsig_or(self
):
670 module
= OpDriver(operator
.or_
, part_out
=False)
671 self
.assertFormal(module
, mode
="bmc", depth
=1)
673 def test_partsig_logical_xor(self
):
674 module
= OpDriver(operator
.xor
, part_out
=False)
675 self
.assertFormal(module
, mode
="bmc", depth
=1)
677 def test_partsig_not(self
):
678 module
= OpDriver(operator
.inv
, nops
=1, part_out
=False)
679 self
.assertFormal(module
, mode
="bmc", depth
=1)
681 def test_partsig_implies(self
):
683 def op_implies(a
, b
):
686 module
= OpDriver(op_implies
, part_out
=False)
687 # yices2 is slow on this test for some reason
689 self
.assertFormal(module
, mode
="bmc", depth
=1, solver
="z3")
692 if __name__
== '__main__':