Prioritized model checking

With the number of transistors doubling every 18 months as predicted by Moore's Law, engineers have created digital designs with such high complexity that they are having difficulty verifying its correct operation. Despite using more and faster simulators, costly design flaws are still being found in production designs.; Formal verification techniques, such as model checking, have been offered as a method for complete verification. In its simplest form, a model checker generates the set of reachable states from the reset state of the design, usually using breadth-first search. As the states are being generated, each state is checked against a set of specification. Because each additional bit can potentially double the size of the state space, model checkers suffer from the state explosion problem, where there are simply too many states that can be represented and stored. Since most model checkers are used to look for design flaws, the breadth-first search used in model checkers can explore many unneeded states before finding bugs in the design.; This research proposes a set of heuristics that reduces the number of states needed to find the bug. First, the set of states that can lead to the violation of specification are computed to enlarge the set of states that can potentially cause design flaws. This Target Enlargement increases the probability that the error states can be found. Second, heuristics are developed to estimate the distance of the state being explored to the largest enlarged target. One heuristic is to use Hamming distance, and the other heuristic, called Tracks , uses approximations of the set of states that can lead to violations of specification and estimates the distance to error states. Finally, designers can give hints, called Guideposts, to influence the search and explore states that are more likely to contain design flaws.; On a set of realistic designs that contain genuine flaws, these heuristics have dramatically reduced the number of states needed to find bugs, by as much as three orders in magnitude. Consequently, it is an additional tool for the designers to combat the increase in complexity driven by Moore's Law.