Abstract
Design validation is becoming more and more a bottleneck in the microprocessor design process. The difficulty of validation stems from the complexity of the design, which requires searching an enormous space to check correctness. This is exacerbated by features for enhancing performance, such as pipelines, which are becoming common in most microprocessors. This paper describes a new abstraction technique to handle this problem. Our solution is a novel method to identify the control states automatically from the processor HDL description and to extract an abstract finite state machine model which preserves the behaviors of the design accurate to the clock cycle, so that the state space to be analyzed is drastically reduced.
This model is used to evaluate microarchitecture-level coverage of validation tests. We also present validation test generation algorithm for traversing state transition paths and covering snapshot and temporal events. These abstract paths with a finite length, along with information about the instruction set, are used to generate system-level tests. Results on example microprocessor models show the technique is efficient in finding bugs that other verification methods miss.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Semiconductor Industry Association, “National Technology Roadmap for Semiconductors, ” 1997.
D. Moundanos, J.A. Abraham, and Y. Hoskote, “A Unified Framework for Design Validation and Manufacturing Test, ” Proc. Intl. Test Conf., 1996.
J. Burch and D. Dill, “Automatic Verification of Pipelined Microprocessor Control, ” Proc. of the Computer Aided Verification Conf., 1994, pp. 68–80.
J. Sawada and W.A. Hunt, “Trace Table Based Approach for Pipelined Microprocessor Verification, ” Proc. of the Computer Aided Verification Conf., June 1997.
M. Kantrowitz and L.M. Noack, “I'm Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DEC chip 21164 Alpha microprocessor, ” Proc. of the Design Automation Conf., June 1996, pp. 325–333.
Verisure, VHDLcover, in http://www.transeda.com/products/.
Simulation Technologies. Vericov User's Guide, 1997.
B. Hetzel, The Complete Guide to Software Testing, QED Information Sciences, Inc., Wellesley, 1988.
B. Beizer, Software Testing Techniques, Van Nostrand Reihold, New York, 1990.
D. Ince. Software Testing. Software Engineer's Reference Book (Volume A: Algorithms and Complexity), J. McDermid Leeuwen (Ed.), Butterworth-Heinemann, London, England, 1991.
R. Ho, C.H. Yang, M.A. Horowitz, and D.L. Dill, “Architecture Validation for Processors, ” Proc. Intl. Symposium on Computer Architecture, June 1995, pp. 404–413.
N. Weste and K. Eshraghian, Principles of CMOS VLSI Design, A Systems Approach, Addison-Wesley Publishing Company, 1994.
A. Chandra, V. Iyengar, D. Jameson, R. Jawalekar, I. Nair, B. Rosen, M. Mullen, J. Yoon, R. Armoni, D. Geist, and Y. Wofsthal, “AVPGEN-A Test Generation for Architecture Verification, ” IEEE Transactions on Very Large Scale Integration Systems, Vol. 3, No. 2, pp. 188–200, June 1995.
A. Aharon, D. Goodman, M. Levinger, Y. Lichtenstein, Y. Malka, C. Metzger, M. Molcho, and G. Shurek, “Test Program Generation for Functional Verification of PowerPC Processors in IBM, ” Proc. of the Design Automation Conf., June 1995, pp. 279–285.
Verisity. Specman Data Sheet, in verisity.com/html/default productspecman.html.
R. Mandayam and R.R. Vemuri, “Generation of Design Verification Tests from Behavioral VHDL Programs using Path Enumeration and Constraint Programming, ” IEEE Transactions on Very Large Scale Integration Systems, Vol. 3, No. 2, pp. 201–214, June 1995.
N. Utamaphethai, R.D. Blanton, and J.P. Shen, “Validation of Speculative and Out-of-order Execution Microarchitecture, ” Proc. Intl. Workshop on Microprocessor Test and Verification, 1998.
V. Bhagwati and S. Devadas, “Automatic Verification of Pipelined Microprocessors, ” Proc. of the Design Automation Conf., 1994, pp. 603–608.
K. Cheng and A. Krishnakumar, “Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model, ” ACM Transactions on Design Automation of Electronic System, Vol. 1, pp. 57–79, Jan. 1996.
D. Moundanos, J.A. Abraham, and Y. Hoskote, “Abstraction Techniques for Validation Coverage Analysis and Test Generation, ” IEEE Transactions on Computers, Vol. 47, pp. 2–14, 1998.
R. Ho and M.A. Horowitz, “Validation Coverage for Complex Digital Designs, ” Proc. Intl. Conf. on Computer-Aided Design, 1996, pp. 146–151.
D. Geist, M. Farkas, A. Landver, and Y. Lichtenstein, “Coverage-Directed Test Generation Using Symbolic Techniques, ” Proc. FMCAD, 1996, pp. 143–158.
S. Ur and Y. Yadin, “Micro Architecture Coverage Directed Generation of Test Programs, ” High-Level Design Validation and Test Workshop, 1998.
K.L. McMillan, “The SMV System DRAFT, ” Carnegie Mellon University, Pittsburgh, PA, 1992. RTL Abstraction Technique 81
IBM, Genesys, in http://www.ibm.net.il/ibm il/ibmhrl/62dauto. htm.
M.S. Abadir, J. Ferguson, and T. Kirkland, “Logic Design Verification via Test Generation, ” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 7, pp. 138–148, Jan. 1988.
S. Kang and S.A. Szygenda, “The Simulation Automation System SAS: Concept, Implementation and Results, ” IEEE Transactions on Very Large Scale Integration Systems, 1994.
H. Al-Asaad and J.P. Hayes, “Design Verification Via Simulation and Automatic Test Pattern Generation, ” Proc. Intl. Conf. on Computer-Aided Design, Austin, TX, Oct. 1995, pp. 174–180.
D. Van Campenhout, H. Al-Asaad, J.P. Hayes, T. Mudge, and R.B. Brown, “High-Level Design Verification of Microprocessors via Error Modeling, ” ACM Transactions on Design Automation of Electronic System, Vol. 3, No. 4, 1998.
S. Devadas, A. Ghosh, and K.Keutzer, “An Observability-Based Code Coverage Metric for Functional Simulation, ” Proc. Intl. Conf. on Computer-Aided Design, 1996, pp. 418–425.
F. Fallah, S. Devadas, and K. Keutzer, “OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification, ” Proc. of the Design Automation Conf., 1998, pp. 152–157.
R. Grinwald, E. Harel, M. Orgad, S. Ur, and A. Ziv, “User Defined Coverage: A Tool Supported Methodology for Design Verification, ” Proc. of the Design Automation Conf., 1998, pp. 158–163.
J. Shen and J.A. Abraham, “Verification of Processor Microarchitectures, ” Proc. IEEE VLSI Test Symposium, 1999, pp. 189–194.
W.J. Culler, Implementing Safety Critical Systems: The VIPER Microprocessor, Kluwer Academic Publishers, 1987.
B. Gennart and D. Luckham, “Validating Discrete Event Simulations Using Event Pattern Mappings, ” Proc. of the Design Automation Conf., 1992, pp. 414–419.
J. Shen and J.A. Abraham, “Native Mode Functional Test Generation for Microprocessors with Applications to Self Test and Design Validation, ” Proc. Intl. Test Conf., 1998, pp. 990–999.
VLSI Technology Inc., ACRON RISC Machine Family Data Manual, Prentice Hall, 1990.
A. Takach and W. Wolf, “Scheduling Constraint Generation for Communicating Processes, ” IEEE Transactions on Very Large Scale Integration Systems, Vol. 3, No. 2, pp. 215–230, June 1995.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Shen, J., Abraham, J.A. An RTL Abstraction Technique for Processor Microarchitecture Validation and Test Generation. Journal of Electronic Testing 16, 67–81 (2000). https://doi.org/10.1023/A:1008388623771
Issue Date:
DOI: https://doi.org/10.1023/A:1008388623771