This paper addresses test generation for design verification of pipelined microprocessors. We describe a highlevel model for testing pipelined microprocessors, which exposes high-level knowledge that is useful for verification test generation. We present a three-part test generation algorithm that uses this knowledge: The core part of the algorithm conducts a branch-and-bound search in a transformed state space of the controller. The decision variables of the search represent the essential interaction between concurrent instructions in the pipeline. The size of this transformed search space can be significantly smaller than the original state space of the controller. The second part of the algorithm selects justification and propagation paths in the datapath, which guide the search in the control space. The third part uses discrete relaxation to determine appropriate data values. We have implemented the proposed algorithm and used it to generate verification tests for design errors in the datapath of a representative pipelined microprocessor. I.

This paper addresses static timing verification for sequential circuits implemented in a mix of static and dynamic logic. We restrict our focus to regular domino logic and footless domino logic, a variant of domino logic. First we derive constraints for proper operation of dynamic gates. An important observation is that for dynamic gates, input signals may start changing near the end of the evaluate phase without compromising correct operation. This gives the circuit designer extra flexibility. We present two verification methods. Both are based on the Sakallah-Mudge-Olukotun (SMO) model for static timing analysis of sequential circuits. The first method models dynamic gates explicitly. The signals at the terminals of the dynamic gates are modeled by five events: the earliest/latest, rising/falling transitions, and a fifth event that models the occurrence of a spurious rising transition. The second method applies the original SMO model after a preprocessing step that computes the combinational delays. A postprocessing step checks the constraints specific to dynamic gates. The relationship between both methods is studied. We show that the second method may result in a more conservative analysis than the first method, but at a lower computational cost. We also examine a less aggressive set of constraints, which disallows spurious transitions. A detailed example illustrating the important features of the model is presented, and an electrical simulation of that circuit is performed. The results demonstrate the practical relevance of the methods.

A design verification methodology for microprocessor hardware based on modeling design errors and generating simulation vectors for the modeled errors via physical fault testing techniques is presented. We have systematically collected design error data from a number of microprocessor design projects. The error data is used to derive error models suitable for design verification testing. A class of basic error models is identified and shown to yield tests that provide good coverage of common error types. To improve coverage for more complex errors, a new class of conditional error models is introduced. An experiment to evaluate the effectiveness of our methodology is presented. Single actual design errors are injected into a correct design, and it is determined if the methodology will generate a test that detects the actual errors. The experiment has been conducted for two microprocessor designs and the results indicate that very high coverage of actual design errors can be obtained with test sets that are complete for a small number of synthetic error models.

Gurevich Abstract State Machines (ASMs) provide a sound mathematical basis for the specification and verification of systems. An application of the ASM methodology to the verification of a pipelined microprocessor (an ARM2 implementation) is described. Both the sequential execution model and final pipelined model are formalized using ASMs. A series of intermediate models are introduced that gradually expose the complications of pipelining. The first intermediate model is proven equivalent to the sequential model in the absence of structural, control, and data hazards. In the following steps, these simplifying assumptions are lifted one by one, and the original proof is refined to establish the equivalence of each intermediate model with the sequential model, leading ultimately to a full proof of equivalence of the sequential and pipelined models.

Two methods are presented for static timing verification of sequential circuits implemented as a mix of static and domino logic. Constraints for proper operation of domino gates are derived. An important observation is that input signals to domino gates may start changing near the end of the evaluate phase. The first method models domino gates explicitly, similar to latches. The second method treats domino gates only during pre- and post-processing steps. This method is shown to be more conservative, but easier to compute.