Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
381
prove condition (6) for every atomic instruction in less than a second. Intuitively,
this makes sense because the enabledness conditions do not involve data or mem.
Thus, none of the datapath falls in the cone of influence, leaving only control
logic for IC3 to reason about. The remaining conditions, (3) and (5), are proven
in less than three seconds. Since all the conditions pass, we apply the POR and
RIS constraints, which reduces the time to hit the bug from 1437s to 46s in
CoSA, including the time to check the conditions.
5.2 Packet Movers
We now evaluate our approach on data integrity properties for a variety of
packet-mover circuits. Data integrity is a safety property that ensures no packets
are dropped or corrupted. In practice, data integrity is often checked by instantiating a monitor, called a scoreboard. It provides the necessary infrastructure
for formal verification. In our case, it non-deterministically tags a magic packet
and checks that this packet exits the system when it should. Crucially, the scoreboard is a reusable module which can check data integrity of arbitrary packet
movers.
Notice that existing symmetry reduction techniques will not be very effective
for this scoreboard setup. For example, consider a circular pointer FIFO which
maintains two incrementing pointers that index a memory for reading and writing, respectively. We cannot use scalarsets to break symmetries in the memory
addresses because the pointers index the memory and are involved in arithmetic,
breaking the syntactic requirements for scalarsets [28]. Furthermore, sequential
memory abstraction [9] could reduce the size of the memory, but does not address the path symmetry. In addition, both these symmetry reduction techniques
are focused on proofs, not bug-finding.
We evaluate our approach on two commercial library components from a
major hardware company. We also implemented simpler, open-source versions of
these designs. Our open-source benchmarks include: i) a circular pointer FIFO
which assumes power-of-two depth but is instantiated with a non-power-of-two
depth (one greater than the provided parameter); ii) a shift register FIFO which
does not properly add data to the last register in the pipeline; and iii) 2-5
Design
# #Solved #Solved PR Time Time PR
com 1
49
35
47
103.8 20.3
com 2
49
25
34
470.8
4.9
cp
49
35
47
230.3 18.9
sr
49
25
33
912.6
5.6
arb n=2
49
35
42
89.1
20.5
arb n=3
49
35
42
94.0
21.9
arb n=4
49
35
42
101.3 35.5
arb n=5
49
35
42
111.7 31.8
Table 1: Number Solved and Average Runtime
R
Fig. 4: Runtime Comparison
381
prove condition (6) for every atomic instruction in less than a second. Intuitively,
this makes sense because the enabledness conditions do not involve data or mem.
Thus, none of the datapath falls in the cone of influence, leaving only control
logic for IC3 to reason about. The remaining conditions, (3) and (5), are proven
in less than three seconds. Since all the conditions pass, we apply the POR and
RIS constraints, which reduces the time to hit the bug from 1437s to 46s in
CoSA, including the time to check the conditions.
5.2 Packet Movers
We now evaluate our approach on data integrity properties for a variety of
packet-mover circuits. Data integrity is a safety property that ensures no packets
are dropped or corrupted. In practice, data integrity is often checked by instantiating a monitor, called a scoreboard. It provides the necessary infrastructure
for formal verification. In our case, it non-deterministically tags a magic packet
and checks that this packet exits the system when it should. Crucially, the scoreboard is a reusable module which can check data integrity of arbitrary packet
movers.
Notice that existing symmetry reduction techniques will not be very effective
for this scoreboard setup. For example, consider a circular pointer FIFO which
maintains two incrementing pointers that index a memory for reading and writing, respectively. We cannot use scalarsets to break symmetries in the memory
addresses because the pointers index the memory and are involved in arithmetic,
breaking the syntactic requirements for scalarsets [28]. Furthermore, sequential
memory abstraction [9] could reduce the size of the memory, but does not address the path symmetry. In addition, both these symmetry reduction techniques
are focused on proofs, not bug-finding.
We evaluate our approach on two commercial library components from a
major hardware company. We also implemented simpler, open-source versions of
these designs. Our open-source benchmarks include: i) a circular pointer FIFO
which assumes power-of-two depth but is instantiated with a non-power-of-two
depth (one greater than the provided parameter); ii) a shift register FIFO which
does not properly add data to the last register in the pipeline; and iii) 2-5
Design
# #Solved #Solved PR Time Time PR
com 1
49
35
47
103.8 20.3
com 2
49
25
34
470.8
4.9
cp
49
35
47
230.3 18.9
sr
49
25
33
912.6
5.6
arb n=2
49
35
42
89.1
20.5
arb n=3
49
35
42
94.0
21.9
arb n=4
49
35
42
101.3 35.5
arb n=5
49
35
42
111.7 31.8
Table 1: Number Solved and Average Runtime
R
Fig. 4: Runtime Comparison