382
M. Mann and C. Barrett
correct circular pointer FIFOs in parallel with a non-deterministic arbiter and
credit counters for managing data flow. The reset state of the credit counter has
one too many credits, so data can be pushed to a full FIFO. The single FIFOs
have two actions each: one for pushing data, and one for popping data. For the
arbitrated circuits, there is a separate action for pushing data onto each FIFO as
well as a single request action which is enabled whenever any FIFO is non-empty.
There is an inherent symmetry in all of these designs. Consider any of the FIFOs.
There are two main actions: pushing data (which is enabled if the FIFO is not
full); and popping data (which is enabled if the FIFO is not empty). In a state
where both are enabled, pushing data followed by popping results in the same
state as popping and then pushing the same data. Furthermore, the actions can
be performed simultaneously, but requiring that they are performed separately
should not change the reachable states (depending on the implementation), so
RIS is applicable.
Our experiments vary both the parameterizable data width and depth of the
packet movers, by sweeping all powers of two between 2 and 128. All benchmarks
contain injected bugs and reach the bug at a deep bound relative to the depth.
We used a timeout of 4 hours. We use our prototype flow for checking the
conditions and CoSA for bounded model checking.
6 For condition (3), we had
to write one guard which is true whenever the scoreboard counter is greater
than zero to handle an edge case. This same guard was used for every design,
but an appropriate invariant relating the scoreboard counter to the internal
state of the system being verified would also have worked. The open-source shift
register FIFO required one more guard about the number of stored elements.
We obtained both guards by observing counterexamples.
Table 1 compares the number of solved instances (49 total per row) within
the timeout and the average runtime of commonly solved instances in seconds.
Columns marked “PR” used the POR and RIS constraints. We additionally use
the following abbreviations: “com” for commercial, “cp” for circular pointer, “sr”
for shift register and “arb” for arbitrated. In Fig. 4 we plot the actual runtime on
a log-scale for all the benchmarks with and without POR and RIS. The dotted
lines show 10x and 100x improvements.
Analysis. There is a cluster of points in the bottom left of Fig. 4 which are solved
extremely quickly by both approaches, but slightly faster without POR and RIS.
These are results on benchmarks with very small parameter values, where the
bug occurs at a low depth, and so the POR and RIS results are dominated by
the time taken to check the conditions. However, as the parameter sizes, and
runtimes, increase, it is clear that POR and RIS can result in exponential speed
ups.
Recall that one concern is that RIS could extend the bound needed to reach
the bug. In the shift register and arbitrated FIFO systems, it extended the bound
by a few steps. However, for the bug in the open-source circular pointer FIFO,
it doubled the bound needed to reach the bug. Regardless, this was more than
6 Note: CoSA’s bounded model checking performance is comparable to commercial
model checkers on these benchmarks.
M. Mann and C. Barrett
correct circular pointer FIFOs in parallel with a non-deterministic arbiter and
credit counters for managing data flow. The reset state of the credit counter has
one too many credits, so data can be pushed to a full FIFO. The single FIFOs
have two actions each: one for pushing data, and one for popping data. For the
arbitrated circuits, there is a separate action for pushing data onto each FIFO as
well as a single request action which is enabled whenever any FIFO is non-empty.
There is an inherent symmetry in all of these designs. Consider any of the FIFOs.
There are two main actions: pushing data (which is enabled if the FIFO is not
full); and popping data (which is enabled if the FIFO is not empty). In a state
where both are enabled, pushing data followed by popping results in the same
state as popping and then pushing the same data. Furthermore, the actions can
be performed simultaneously, but requiring that they are performed separately
should not change the reachable states (depending on the implementation), so
RIS is applicable.
Our experiments vary both the parameterizable data width and depth of the
packet movers, by sweeping all powers of two between 2 and 128. All benchmarks
contain injected bugs and reach the bug at a deep bound relative to the depth.
We used a timeout of 4 hours. We use our prototype flow for checking the
conditions and CoSA for bounded model checking.
6 For condition (3), we had
to write one guard which is true whenever the scoreboard counter is greater
than zero to handle an edge case. This same guard was used for every design,
but an appropriate invariant relating the scoreboard counter to the internal
state of the system being verified would also have worked. The open-source shift
register FIFO required one more guard about the number of stored elements.
We obtained both guards by observing counterexamples.
Table 1 compares the number of solved instances (49 total per row) within
the timeout and the average runtime of commonly solved instances in seconds.
Columns marked “PR” used the POR and RIS constraints. We additionally use
the following abbreviations: “com” for commercial, “cp” for circular pointer, “sr”
for shift register and “arb” for arbitrated. In Fig. 4 we plot the actual runtime on
a log-scale for all the benchmarks with and without POR and RIS. The dotted
lines show 10x and 100x improvements.
Analysis. There is a cluster of points in the bottom left of Fig. 4 which are solved
extremely quickly by both approaches, but slightly faster without POR and RIS.
These are results on benchmarks with very small parameter values, where the
bug occurs at a low depth, and so the POR and RIS results are dominated by
the time taken to check the conditions. However, as the parameter sizes, and
runtimes, increase, it is clear that POR and RIS can result in exponential speed
ups.
Recall that one concern is that RIS could extend the bound needed to reach
the bug. In the shift register and arbitrated FIFO systems, it extended the bound
by a few steps. However, for the bug in the open-source circular pointer FIFO,
it doubled the bound needed to reach the bug. Regardless, this was more than
6 Note: CoSA’s bounded model checking performance is comparable to commercial
model checkers on these benchmarks.