In practice, model checkers are most useful when they find bugs, not when they prove a property. However, because large portions of the state space of the design actually satisfy the specification, model checkers devote much effort verifying correct portions of the design. In this paper, we enhance the bug-finding capability of a model checker by using heuristics to search the states that are most likely to lead to an error, first. Reductions of 1 to 3 orders of magnitude in the number of states needed to find bugs in industrial designs have been observed. Consequently, these heuristics can extend the capability of model checkers to find bugs in designs.

Modern, high performance microprocessors are extremely complex machines which require substantial validation effort to ensure functional correctness prior to tapeout. Generating the corner cases to test these designs is a mostly manual process, where completion is hard to judge. Experience shows that the errors that are caught late in the design, many post-silicon, are interactions between different components in very improbable corner case situations. In this paper we present a technique that targets such error-causing interactions by automatically generating test vectors that will cause the processor to exercise all transitions of the control logic in simulation. We use techniques from formal verification to derive transition tours of a fully enumerated state graph of the control logic of the processor. Our system works from a Verilog description of the original machine and is currently being used to validate an embedded dual-issue processor in the node controller of the Stanford FLASH Multiprocessor. Modeling the processor control results in 200K states and an 8M instruction trace to check all transitions of control arcs.

The role of automatic formal protocol verification in hardware design is considered. Principles that maximize the benefits of protocol verification while minimizing the labor and computation required are identified. A novel protocol description language and verifier (both called Mur phi ) are described, along with experiences in applying them to two industrial protocols that were developed as part of hardware designs.>