Joint work with Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix.
Our experience with semi-exhaustive verification shows a severe
degradation in usability for the corner-case bugs, where the tuning effort
becomes much higher and recovery from dead-ends is more and more difficult.
Moreover, when there are no bugs at all, shifting semi-exhaustive traversal
to exhaustive traversal is very expensive, if not impossible. This makes the
output of semi-exhaustive verification on non-buggy designs very ambiguous.
Furthermore, since after the design fixes each falsification task needs to
converge to full verification, there is a strong need for an algorithm that
can handle efficiently both verification and falsification.
We address these shortcomings with an enhanced reachability algorithm that is more robust in
detecting corner-case bugs and that can potentially converge to exhaustive
reachability. Our approach is similar to that of Cabodi et al. in
partitioning the frontiers during the traversal, but differs in two
respects. First, our partitioning algorithm trades quality for time
resulting in a significantly faster traversal. Second, the subfrontiers are
processed according to some priority function resulting in a mixed BFS/DFS
traversal. It is this last feature that makes our algorithm suitable for
both falsification and verification.