Modeling and validation of pipeline specifications

ABSTRACT

Verification is one of the most complex and expensive tasks in the current Systems-on-Chip design process. Many existing approaches employ a bottom-up approach to pipeline validation, where the functionality of an existing pipelined processor is, in essence, reverse-engineered from its RT-level implementation. Our validation technique is complementary to these bottom-up approaches. Our approach leverages the system architect's knowledge about the behavior of the pipelined architecture, through architecture description language (ADL) constructs, and thus allows a powerful top-down approach to pipeline validation. The most important requirement in top-down validation process is to ensure that the specification (reference model) is golden. This paper addresses automatic validation of processor, memory, and coprocessor pipelines described in an ADL. We present a graph-based modeling that captures both structure and behavior of the architecture. Based on this model, we present algorithms to ensure that the static behavior of the pipeline is well formed by analyzing the structural aspects of the specification. We applied our methodology to verify specification of several realistic architectures from different architectural domains to demonstrate the usefulness of our approach.

REFERENCES

• 1: Mark Aagaard , Byron Cook , Nancy A. Day , Robert B. Jones, A Framework for Microprocessor Correctness Statements, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.433-448, September 04-07, 2001
• 2: ARC. http://www.arccores.com. ARC Cores.
• 3: Axys. Axys Design Automation. http://www.axysdesign.com.
• 4: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 5: Cyrluk, D. 1993. Microprocessor Verification in PVS: A Methodology and Simple Example. Tech. Rep., SRI-CSL-93-12.
• 6: Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997 [doi>10.1145/248621.248624]
• 7: Freericks, M. 1993. The nML machine description formalism. Tech. Rep. TR SM-IMP/DIST/08, TU Berlin CS Dept.
• 8: George Hadjiyiannis , Silvina Hanono , Srinivas Devadas, ISDL: an instruction set description language for retargetability, Proceedings of the 34th annual conference on Design automation, p.299-302, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266108]
• 9: Ashok Halambi , Peter Grun , Vijay Ganesh , Asheesh Khare , Nikil Dutt , Alex Nicolau, EXPRESSION: a language for architecture exploration through compiler/simulator retargetability, Proceedings of the conference on Design, automation and test in Europe, p.100-es, January 1999, Munich, Germany [doi>10.1145/307418.307549]
• 10: David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
• 11: Yirng-An Chen , Edmund M. Clarke , Pei-Hsin Ho , Yatin Vasant Hoskote , Timothy Kam , Manpreet Khaira , John W. O'Leary , Xudong Zhao, Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.19-33, November 06-08, 1996
• 12: Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289082]
• 13: Ravi Mohan Hosabettu , Ganesh Gopalakrishnan, Systematic verification of pipelined microprocessors, 2000
• 14: James K. Huggins , David Van Campenhout, Specification and verification of pipelining in the ARM2 RISC microprocessor, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.4, p.563-580, Oct. 1998 [doi>10.1145/296333.296345]
• 15: Inoue, A., Tomiyama, H., Eko, F., Kanbara, H., and Yasuura, H. 1998. A programming language for processor based embedded systems. In Proceedings of Asia Pacific Conference on Hardware Description Languages (APCHDL), 89--94.
• 16: Christian Jacobi, II, Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving, Proceedings of the 14th International Conference on Computer Aided Verification, p.309-323, July 27-31, 2002
• 17: Ranjit Jhala , Kenneth L. McMillan, Microarchitecture Verification by Compositional Model Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.396-410, July 18-22, 2001
• 18: Lanneer, D., Praet, J., Kifli, A., Schoofs, K., Geurts, W., Thoen, F., and Goossens, G. 1995. CHESS: Retargetable code generation for embedded DSP processors. In Code Generation for Embedded Processors. Kluwer Academic, Norwell, MA, 85--102.
• 19: Rainer Leupers , Peter Marwedel, Retargetable Generation of Code Selectors from HDL Processor Models, Proceedings of the 1997 European conference on Design and Test, p.140, March 17-20, 1997
• 20: Leupers, R. and Marwedel, P. 1998. Retargetable Code generation based on structural processor descriptions. Design Automation for Embedded Systems 3, 1.
• 21: Jeremy Levitt , Kunle Olukotun, Verifying correct pipeline implementation for microprocessors, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.162-169, November 09-13, 1997, San Jose, California, United States
• 22: Prabhat Mishra , Nikil D. Dutt, Modeling and Verification of Pipelined Embedded Processors in the Presence of Hazards and Exceptions, Proceedings of the IFIP 17th World Computer Congress - TC10 Stream on Distributed and Parallel Embedded Systems: Design and Analysis of Distributed Embedded Systems, p.81-90, August 25-29, 2002
• 23: Mishra, P., Dutt, N., and Nicolau, A. 2001. Architecture description language driven validation of processor, memory, and co-processor pipelines. Tech. Rep. UCI-ICS 01-55, University of California, Irvine.
• 24: Prabhat Mishra , Peter Grun , Nikil Dutt , Alex Nicolau, Processor-Memory Co-Exploration driven by a Memory-Aware Architecture Description Language, Proceedings of the The 14th International Conference on VLSI Design (VLSID '01), p.70, January 03-07, 2001
• 25: Prabhat Mishra , Arun Kejariwal , Nikil Dutt, Rapid Exploration of Pipelined Processors through Automatic Generation of Synthesizable RTL Models, Proceedings of the 14th IEEE International Workshop on Rapid System Prototyping (RSP'03), p.226, June 09-11, 2003
• 26: P. Mishra , N. Dutt , A. Nicolau , H. Tomiyama, Automatic Verification of In-Order Execution In Microprocessors with Fragmented Pipelines and Multicycle Functional Units, Proceedings of the conference on Design, automation and test in Europe, p.36, March 04-08, 2002
• 27: Paulin, P., Liem, C., May, T., and Sutarwala, S. 1994. FlexWare: A flexible firmware development environment for embedded systems. In Prof. of Dagstuhl Workshop on Code Generation for Embedded Processors, 67--84.
• 28: V. Rajesh , R. Moona, Processor Modeling for Hardware Software Codesign, Proceedings of the 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', p.132, January 10-13, 1999
• 29: Jun Sawada , Warren A. Hunt, Jr., Processor Verification with Precise Exeptions and Speculative Execution, Proceedings of the 10th International Conference on Computer Aided Verification, p.135-146, June 28-July 02, 1998
• 30: Jun Sawada , Warren A. Hunt, Jr., Trace Table Based Approach for Pipeline Microprocessor Verification, Proceedings of the 9th International Conference on Computer Aided Verification, p.364-375, June 22-25, 1997
• 31: Oliver Schliebusch , Andreas Hoffmann , Achim Nohl , Gunnar Braun , Heinrich Meyr, Architecture Implementation Using the Machine Description Language LISA, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.239, January 07-11, 2002
• 32: Chuck Siska, A processor desription language supporting retargetable multi-pipeline DSP program development tools, Proceedings of the 11th international symposium on System synthesis, p.31-36, December 02-04, 1998, Hsinchu, Taiwan, China
• 33: Jens U. Skakkebæk , Robert B. Jones , David L. Dill, Formal Verification of Out-of-Order Execution Using Incremental Flushing, Proceedings of the 10th International Conference on Computer Aided Verification, p.98-109, June 28-July 02, 1998
• 34: Mandayam Srivas , Mark Bickford, Formal Verification of a Pipelined Microprocessor, IEEE Software, v.7 n.5, p.52-64, September 1990 [doi>10.1109/52.57892 ]
• 35: Target. http://www.retarget.com. Target Compiler Technologies.
• 36: Tensilica. http://www.tensilica.com. Tensilica Inc.
• 37: Trimaran. 1997. The MDES User Manual. Trimaran release: http://www.trimaran.org.
• 38: Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337331]
• 39: Miroslav N. Velev, Formal Verification of VLIW Microprocessors with Speculative Execution, Proceedings of the 12th International Conference on Computer Aided Verification, p.296-311, July 15-19, 2000
• 40: Zivojnovic, V., Pees, S., and Meyr, H. 1996. LISA---Machine description language and generic machine model for HW/SW co-design. In IEEE Workshop on VLSI Signal Processing, 127--136.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Modeling of computer architecture

Additional Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Systems specification methodology
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Algorithms, Design, Languages, Verification

Keywords:
Modeling of processor pipeline, architecture description language, pipeline validation, pipelined processor specification