A unified validation framework for VLSI circuits using formal and abstraction techniques

The functional validation of modern, high complexity circuits is a difficult and resource demanding process. Despite great advances in the area of formal verification, it is becoming increasingly clear that utilization of various approaches and techniques will be necessary in order to ensure correctness before tapeout. In this dissertation a unified validation framework is developed to integrate a number of automated techniques for the verification of sequential circuits. Since the well known "state explosion" problem makes formal verification impractical for large designs, simulation is still the primary means of verifying real-life circuits. Associated with simulation is the problem of coverage, i.e., ensuring that all important cornercases have been tested. We provide a unified framework, based on powerful abstraction techniques, for validation coverage analysis, coverage directed test generation, manufacturing test and formal verification of certain types of control properties.; The basis of our abstraction techniques is the fact that most design errors are associated with the control flow in the circuit and the interaction of the control logic with datapath circuitry. In this regard we present a novel technique for automatically extracting the control flow machine of a design from its description at any level. The extraction is done based on the underlying mathematical model and is independent of the description style. Furthermore the extracted model has a much smaller state space while exhibiting the same control flow as the original circuit. We propose a pragmatic and meaningful definition of functional coverage as the amount of control behavior covered by the test suite. We then combine formal verification techniques, using Binary Decision Diagrams (BDDs) as the underlying technology, with traditional Automatic Test Pattern Generation (ATPG) and behavioral test generation algorithms to automatically generate tests for uncovered parts of the state graph of the control logic of the circuit. To continue, we extend our functional coverage definition to include monitoring of event sequences, specified by the designer. We also employ the same approach for the efficient detection of hard stuck-at faults in the control part of the design, for which conventional ATPG techniques alone prove to be inadequate or inefficient at best. Finally we formally verify certain types of control properties by applying the same abstraction to both the design and the property machine. The properties are specified as finite state machines in a Hardware Description Language (HDL). The capability of producing witnesses and counter examples is also provided. Our experience with the proposed methodology has shown this approach to be successful in the validation of complex circuits.