Symbolic model checking is an increasingly popular debugging tool based on Binary Decision Diagrams (BDDs). The size of the diagrams, however, often prevents its application to large designs. The lack of flexibility of the conventional breadth-first approach to state search is often responsible for the excessive growth of the BDDs. In this paper we show that the use of hints to guide the exploration of the state space may result in orders-of-magnitude reductions in time and space requirements. We apply hints to invariant checking. The hints address the problems posed by difficult image computations, and are effective in both proving and refuting invariants. We show that good hints can often be found with the help of simple heuristics by someone who understands to circuit well enough to devise simulation stimuli or verification properties for it. We present an algorithm for guided traversal and discuss its efficient implementation.
展开▼
