High-Level Test Generation for Design Verification of Pipelined Microprocessors 1

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