Article

Free access

Verifying correct pipeline implementation for microprocessors

Authors:

Jeremy Levitt,

Kunle OlukotunAuthors Info & Claims

ICCAD '97: Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design

Pages 162 - 169

Published: 13 November 1997 Publication History

PDF eReader Publisher Site

Abstract

We introduce a general, automatic verification technique for pipelined designs. The technique is based on a scalable, formal methodology for analyzing pipelines. The key advantages to our technique are: it specifically targets pipeline control, making it more efficient; it requires no explicit specification, since it compares hardware against itself; it can be used within the broader framework of hierarchical verification; and, it can be easily extended to handle certain "complex" pipelined structures.

References

[1]

V. Bhagwati and S. Devadas, "Automatic Verification of Pipelined Microprocessors," in Proceedings of 31st Design Automation Conference, San Diego CA, June 1994.

Digital Library

Google Scholar

[2]

J. R. Burch and D. L. Dill, "Automatic Verification of Pipelined Microprocessor Control," in Conference on Computer-Aided Verification, Lecture Notes in Computer Science, vol 18, pp 68-80, Springer-Verlag, 1994.

Digital Library

Google Scholar

[3]

C. Barrett, D. L. Dill and J. Levitt, "Validity Checking for Combinations of Theories with Equality" in Proceedings of The International Conference on Formal Methods in Computer-Aided Design, Palo Alto, CA, November 1996.

Digital Library

Google Scholar

[4]

J. R. Burch, "Techniques for Verifying Superscalar Microprocessors" in Proceedings of The 33rid ACM/IEEE Design Automation Conference, Las Vegas NV, June 1996.

Digital Library

Google Scholar

[5]

J. Levitt and K. Olukotun, "A Scalable Formal Verification Methodology for Pipelined Microprocessors" in Proceedings of The 33rid ACM/IEEE Design Automation Conference, Las Vegas NV, June 1996.

Digital Library

Google Scholar

[6]

J. Hennessy and D. Paterson, Computer Architecture: A Quantitative Approach, 2nd ed. Morgan Kaufman, 1996.

Digital Library

Google Scholar

[7]

R. B. Jones, D. L. Dill, J. R. Burch, "Efficient Validity Checking for Processor Verification," in Proceedings of The International Conference on Computer Aided Design, San Jose CA, Nov, 1995.

Digital Library

Google Scholar

[8]

M. C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial," IEEE Transactions on computer- Aided Design of lntegrated Circuits and Systems, vol. 12, no. 5, May 1993.

Google Scholar

[9]

K. McMillan, "Fitting Formal Methods into the Design Cycle," in Proceedings of 31st Design Automation Conference, San Diego CA, June, 1994.

Digital Library

Google Scholar

[10]

M. Srivas and M. Bickford, "Formal Verification of a Pipelined Microprocessor" IEEE Software, vol. 7, no. 5), pp. 52-64, Sept. 1990

Digital Library

Google Scholar

Cited By

View all

Roy APanda SKumar RChakrabarti P(2005)A framework for systematic validation and debugging of pipeline simulatorsACM Transactions on Design Automation of Electronic Systems10.1145/1080334.108033610:3(462-491)Online publication date: 1-Jul-2005
https://dl.acm.org/doi/10.1145/1080334.1080336
Velev M(2004)Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of MicroprocessorsProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969033Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969033
Velev MGarrett DLach JZukowski C(2004)Efficient formal verification of pipelined processors with instruction queuesProceedings of the 14th ACM Great Lakes symposium on VLSI10.1145/988952.988975(92-95)Online publication date: 26-Apr-2004
https://dl.acm.org/doi/10.1145/988952.988975
Show More Cited By

Index Terms

Verifying correct pipeline implementation for microprocessors

Recommendations

Split-Path Enhanced Pipeline Scheduling

Software pipelining increases the loop execution throughput by overlapping the execution of successive iterations in a pipelined fashion. For loops with control flows, however, software pipelining is not straightforward because we need to consider the ...
Verifying Pipeline Implementations in OpenMP
Model Checking Software
Abstract
OpenMP is a popular API for the development of parallel, shared memory programs and allows programmers to easily ready their programs to utilize modern multi-core processors. However, OpenMP-compliant programs do not guarantee that the OpenMP ...
Asynchronous pipeline analysis and scheduling

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICCAD '97: Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design

November 1997

769 pages

ISBN:0818682000

Chairmen:
Ralph H. J. M. Otten
Delft Univ., delft, The Netherlands
,
Hiroto Yasuura
Kyushu Univ., Kasuga, Japan

Publisher

IEEE Computer Society

United States

Publication History

Published: 13 November 1997

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
291
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)12

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Roy APanda SKumar RChakrabarti P(2005)A framework for systematic validation and debugging of pipeline simulatorsACM Transactions on Design Automation of Electronic Systems10.1145/1080334.108033610:3(462-491)Online publication date: 1-Jul-2005
https://dl.acm.org/doi/10.1145/1080334.1080336
Velev M(2004)Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of MicroprocessorsProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969033Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969033
Velev MGarrett DLach JZukowski C(2004)Efficient formal verification of pipelined processors with instruction queuesProceedings of the 14th ACM Great Lakes symposium on VLSI10.1145/988952.988975(92-95)Online publication date: 26-Apr-2004
https://dl.acm.org/doi/10.1145/988952.988975
Mishra PDutt N(2004)Modeling and validation of pipeline specificationsACM Transactions on Embedded Computing Systems10.1145/972627.9726333:1(114-139)Online publication date: 1-Feb-2004
https://dl.acm.org/doi/10.1145/972627.972633
Yang ZMin BChoi G(2000)Si-EmulationProceedings of the 2000 IEEE International Test Conference10.5555/839295.843556Online publication date: 3-Oct-2000
https://dl.acm.org/doi/10.5555/839295.843556
Van Campenhout DMudge THayes J(1999)High-level test generation for design verification of pipelined microprocessorsProceedings of the 36th annual ACM/IEEE Design Automation Conference10.1145/309847.309912(185-188)Online publication date: 1-Jun-1999
https://dl.acm.org/doi/10.1145/309847.309912
Ho PIsles AKam TYasuura H(1998)Formal verification of pipeline control using controlled token nets and abstract interpretationProceedings of the 1998 IEEE/ACM international conference on Computer-aided design10.1145/288548.289082(529-536)Online publication date: 1-Nov-1998
https://dl.acm.org/doi/10.1145/288548.289082

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Split-Path Enhanced Pipeline Scheduling

Verifying Pipeline Implementations in OpenMP

Asynchronous pipeline analysis and scheduling