Logical errors in sequential circuit designs are an important problem for circuit designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called temporal logic model checking for this class of circuits. In this approach specifications are expressed in a propositional temporal logic, and circuits are modeled as state-transition systems. An efficient search procedure is used to determine automatically if the specifications are satisfied by the transition system. The technique has been used in the past to find subtle errors in a number of non-trivial circuit designs.#R##N##R##N#Recently, the size of the circuits that can be verified by model checking techniques has increased dramatically. By representing transition relations implicitly using Binary Decision Diagrams (BDDs), we have been able to check some examples that would have required 1020 states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10100. By combining model checking with various abstraction techniques, we have been able to handle even larger systems. In one example, we were able to verify a pipelined ALU with more than 101300 states (including 64 registers of 64 bits each).#R##N##R##N#Although we believe that model checking is already useful for verifying some sequential circuit designs that arise in industry, additional research is needed to exploit the full power of this method. We conclude by discussing three of the most important research areas:#R##N#•#TAB##R##N#Use of abstraction and symmetry to achieve an even greater reduction in the size of the state-space that must be explored by this method.#R##N##R##N#•#TAB##R##N#Development of model checking techniques that can handle parameterized circuit designs without requiring each individual instance of the circuit to be verified.#R##N##R##N#•#TAB##R##N#Tool interfaces that facilitate the specification of complex circuits and aid the user in isolating the cause of errors that are detected during verification.
['Edmund M. Clarke']
Automatic Verification of Sequential Circuit Designs