Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
383
compensated for by the symmetry-breaking of POR, as evidenced by the faster
times to reach the bug. The deepest bound was 260 which occurred at FIFO
depth 129.
It is interesting to note that encoding the transition systems to SMT using
the theory of arrays was always slower for bounded model checking, but was
noticeably faster for checking RIS and POR conditions. Perhaps this is because
the state comparison is easier for the solver to reason about using array extensionality [23].
We have demonstrated that these techniques work well for packet movers.
In part, this is because packet movers are often well-constrained by their environmental assumptions, and their behavior is largely independent of incoming
data values. Furthermore, we typically expect the POR and RIS conditions to
hold for a correct packet-mover implementation, so a failure in a condition could
identify a bug.
6 Related Work
Various techniques have been employed to accelerate bounded model checking.
The authors of [19] use BDDs to accelerate BMC, and the techniques introduced in [35,36] exploit the structure of BMC queries to help the SAT solver.
The authors of [18] take advantage of structural information with an SMT framework tailored for BMC. Our technique is similar in that we speed up bounded
model checking by adding constraints to the transition system, but we obtain
constraints using partial order reduction analysis.
Wang et al. [37] pioneered partial order reduction for symbolic software model
checking, guaranteeing optimal reduction for two threads. Their follow-up paper,
[21], extended this framework to find the optimal reduction for any number of
threads. We adapted their symbolic POR technique for synchronous hardware
model checking, and developed reduced instruction sets to improve the efficacy of
POR in this new domain. Bhattacharya et al. used a SAT solver to directly check
guarded independence conditions (as opposed to checking syntactic properties)
for asynchronous rule-based languages [3]. We also check conditions directly, but
in a synchronous setting.
The techniques developed by McMillan, temporal case splitting and path splitting [28], provide a framework for splitting on possible values at a given timestep.
These approaches deal with system executions, but still rely on breaking data
symmetries for performance. In contrast, our techniques focus on mitigating path
symmetries.
The work of Bengtsson et al. [2] extended POR to timed automata using
a local-time desynchronization of clocks, followed by resynchronization with an
added global clock. Similarly, our techniques adapt POR by modifying the system. However, our approach targets a different domain, and only modifies the
original system by adding constraints.
383
compensated for by the symmetry-breaking of POR, as evidenced by the faster
times to reach the bug. The deepest bound was 260 which occurred at FIFO
depth 129.
It is interesting to note that encoding the transition systems to SMT using
the theory of arrays was always slower for bounded model checking, but was
noticeably faster for checking RIS and POR conditions. Perhaps this is because
the state comparison is easier for the solver to reason about using array extensionality [23].
We have demonstrated that these techniques work well for packet movers.
In part, this is because packet movers are often well-constrained by their environmental assumptions, and their behavior is largely independent of incoming
data values. Furthermore, we typically expect the POR and RIS conditions to
hold for a correct packet-mover implementation, so a failure in a condition could
identify a bug.
6 Related Work
Various techniques have been employed to accelerate bounded model checking.
The authors of [19] use BDDs to accelerate BMC, and the techniques introduced in [35,36] exploit the structure of BMC queries to help the SAT solver.
The authors of [18] take advantage of structural information with an SMT framework tailored for BMC. Our technique is similar in that we speed up bounded
model checking by adding constraints to the transition system, but we obtain
constraints using partial order reduction analysis.
Wang et al. [37] pioneered partial order reduction for symbolic software model
checking, guaranteeing optimal reduction for two threads. Their follow-up paper,
[21], extended this framework to find the optimal reduction for any number of
threads. We adapted their symbolic POR technique for synchronous hardware
model checking, and developed reduced instruction sets to improve the efficacy of
POR in this new domain. Bhattacharya et al. used a SAT solver to directly check
guarded independence conditions (as opposed to checking syntactic properties)
for asynchronous rule-based languages [3]. We also check conditions directly, but
in a synchronous setting.
The techniques developed by McMillan, temporal case splitting and path splitting [28], provide a framework for splitting on possible values at a given timestep.
These approaches deal with system executions, but still rely on breaking data
symmetries for performance. In contrast, our techniques focus on mitigating path
symmetries.
The work of Bengtsson et al. [2] extended POR to timed automata using
a local-time desynchronization of clocks, followed by resynchronization with an
added global clock. Similarly, our techniques adapt POR by modifying the system. However, our approach targets a different domain, and only modifies the
original system by adding constraints.