Article

Automatic memory reductions for RTL model verification

Authors:

Panagiotis Manolios,

Sudarshan K. Srinivasan,

Daron VroonAuthors Info & Claims

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

Pages 786 - 793

https://doi.org/10.1145/1233501.1233663

Published: 05 November 2006 Publication History

Abstract

We present several techniques for automatically reducing memories in RTL designs. This includes a new memory abstraction algorithm that allows us to greatly reduce the size of memories and a technique based on-term rewriting that further improves the abstraction. In contrast to previously proposed methods for abstracting memories of RTL designs, our methods are general---e.g., they allow us to arbitrarily and directly compare memories---and they are sound and complete---e.g., there are no false positives or negatives. In addition, the combination of our techniques allows us to automatically verify RTL pipelined machine designs beyond the reach of current state-of-the-art methods, as our experimental results show.

References

[1]

Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah. Refinement strategies for verification methods based on datapath abstraction. In F. Hirose, editor, Asia South Pacific Design Automation Conference (ASP-DAC'06), pages 19--24. IEEE, 2006.

Digital Library

[2]

W. R. Bevier, W. A. Hunt, Jr., J. S. Moore, and W. D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411--428, December 1989.

[3]

P. Bjesse and A. Boralv. DAG-aware circuit compression. In IEEE/ACM International Conference on Computer Aided Design, 2004 (ICCAD-2004), pages 42--49, 2004.

Digital Library

[4]

R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In E. Brinksma and K. G. Larsen, editors, Computer Aided Verification (CAV'02), volume 2404 of Lecture Notes in Computer Science, pages 78--92. Springer, 2002.

Digital Library

[5]

J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In Computer-Aided Verification (CAV '94), volume 818 of LNCS, pages 68--80. Springer-Verlag, 1994.

Digital Library

[6]

L. Clark, E. Hoffman, J. Miller, M. Biyani, Y. Liao, S. Strazdus, M. Morrow, K. Velarde, and M. Yarch. An embedded 32-bit microprocessor core for low-power and high-performance applications. IEEE Journal of Solid-State Circuits, 36(11):1599--1608, 2001.

[7]

E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19, July 2001.

Digital Library

[8]

M. K. Ganai, A. Gupta, and P. Ashar. Efficient modeling of embedded memories in bounded model checking. In R. Alur and D. Peled, editors, Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 440--452. Springer, 2004.

[9]

M. K. Ganai, A. Gupta, and P. Ashar. Verification of embedded memory systems using efficient memory modeling. In Design, Automation and Test in Europe (DATE'05), pages 1096--1101. IEEE Computer Society, 2005.

Digital Library

[10]

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts), volume 3114 of Lecture Notes in Computer Science, pages 175--188. Springer, 2004.

[11]

R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification-CAV '99, volume 1633 of LNCS. Springer-Verlag, 1999.

[12]

H. Jain, D. Kroening, N. Sharygina, and E. M. Clarke. Word level predicate abstraction and refinement for verifying rtl verilog. In W. H. J. Jr., G. Martin, and A. B. Kahng, editors, Design Automation Conference (DAC'05), pages 445--450. ACM, 2005.

Digital Library

[13]

S. Lahiri, S. Seshia, and R. Bryant. Modeling and verification of out-of-order microprocessors using UCLID. In Formal Methods in Computer-Aided Design (FMCAD'02), volume 2517 of LNCS, pages 142--159. Springer-Verlag, 2002.

Digital Library

[14]

P. Manolios and S. Srinivasan. Automatic verification of safety and liveness for XScale-like processor models using WEB-refinements. In Design Automation and Test in Europe, DATE'04, 2004.

Digital Library

[15]

P. Manolios and S. Srinivasan. A complete compositional reasoning framework for the efficient verification of pipelined machines. In ACM-IEEE International Conference on Computer Aided Design (ICCAD'05), November 2005.

Digital Library

[16]

P. Manolios and S. K. Srinivasan. Verification of executable pipelined machines with bit-level interfaces. In ACM-IEEE International Conference on Computer Aided Design (ICCAD'05), November 2005.

Digital Library

[17]

L. Ryan. Siege homepage. See URL http://www.cs.sfu.ca/~loryan/personal.

[18]

J. Sawada and W. A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV '98), volume 1427 of LNCS, pages 135--146. Springer-Verlag, 1998.

Digital Library

[19]

Ultrasparc processors. See URL http://-www.sun.com/processors/technologies.html.

[20]

M. N. Velev, R. E. Bryant, and A. Jain. Efficient modeling of memory arrays in symbolic simulation. In O. Grumberg, editor, Computer Aided Verification (CAV'97), volume 1254 of Lecture Notes in Computer Science, pages 388--399. Springer, 1997.

Digital Library

Cited By

Emmer MKhasidashvili ZKorovin KSticksel CVoronkov A(2012)EPR-based bounded model checking at word levelProceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_18(210-224)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_18
German SBjesse PSlobodová A(2011)A theory of abstraction for arraysProceedings of the International Conference on Formal Methods in Computer-Aided Design10.5555/2157654.2157682(176-185)Online publication date: 30-Oct-2011
https://dl.acm.org/doi/10.5555/2157654.2157682
Baumgartner JCase MMony HBloem RSharygina N(2010)Coping with Moore's law (and more)Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998512(61-69)Online publication date: 20-Oct-2010
https://dl.acm.org/doi/10.5555/1998496.1998512
Show More Cited By

Index Terms

Automatic memory reductions for RTL model verification
1. Hardware

Recommendations

Automated Correctness Condition Generation for Formal Verification ofSynthesized RTL Designs
Special issue on formal methods for computer-added design

High-level synthesis tools generate register-transfer level designs from algorithmic behavioral specifications. The high-level synthesis process typically consists of dependency graph scheduling, functional unit allocation, register allocation, ...
Memory modeling in ESL-RTL equivalence checking
DAC '07: Proceedings of the 44th annual Design Automation Conference

When designers create RTL models from a system-level specification, arrays in the system-level model are often implemented as memories in the RTL. Knowing the correspondence between ESL arrays and RTL memories can significantly reduce the complexity of ...
A methodology to take credit for high-level verification during RTL verification

High-level verification and synthesis of SystemC models has become increasingly popular as a means to reduce the high RTL verification cost of today's complex designs. However, the saving derived from performing verification at a higher level of ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

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

November 2006

147 pages

ISBN:1595933891

DOI:10.1145/1233501

General Chair:
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS: Circuits & Systems
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICCAD06

Sponsor:

SIGDA
IEEE-CAS
IEEE-CS

ICCAD06: The International Conference on Computer-Aided Design 2006

November 5 - 9, 2006

California, San Jose

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
142
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Emmer MKhasidashvili ZKorovin KSticksel CVoronkov A(2012)EPR-based bounded model checking at word levelProceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_18(210-224)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_18
German SBjesse PSlobodová A(2011)A theory of abstraction for arraysProceedings of the International Conference on Formal Methods in Computer-Aided Design10.5555/2157654.2157682(176-185)Online publication date: 30-Oct-2011
https://dl.acm.org/doi/10.5555/2157654.2157682
Baumgartner JCase MMony HBloem RSharygina N(2010)Coping with Moore's law (and more)Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998512(61-69)Online publication date: 20-Oct-2010
https://dl.acm.org/doi/10.5555/1998496.1998512
He NHsiao MBenini LDe Micheli GAl-Hashimi BMueller W(2009)An efficient path-oriented bitvector encoding width computation algorithm for bit-precise verificationProceedings of the Conference on Design, Automation and Test in Europe10.5555/1874620.1875004(1602-1607)Online publication date: 20-Apr-2009
https://dl.acm.org/doi/10.5555/1874620.1875004
Koelbl AJacoby RJain HPixley CBenini LDe Micheli GAl-Hashimi BMueller W(2009)Solver technology for system-level to RTL equivalence checkingProceedings of the Conference on Design, Automation and Test in Europe10.5555/1874620.1874667(196-201)Online publication date: 20-Apr-2009
https://dl.acm.org/doi/10.5555/1874620.1874667
Srinivasan SSarker KKatti R(2009)Verification of Synchronous Elastic ProcessorsIEEE Embedded Systems Letters10.1109/LES.2009.20280431:1(14-18)Online publication date: 1-May-2009
https://dl.acm.org/doi/10.1109/LES.2009.2028043
He NHsiao M(2009)An efficient path-oriented bitvector encoding width computation algorithm for bit-precise verification2009 Design, Automation & Test in Europe Conference & Exhibition10.1109/DATE.2009.5090920(1602-1607)Online publication date: Apr-2009
https://doi.org/10.1109/DATE.2009.5090920
Koelbl AJacoby RJain HPixley C(2009)Solver technology for system-level to RTL equivalence checking2009 Design, Automation & Test in Europe Conference & Exhibition10.1109/DATE.2009.5090657(196-201)Online publication date: Apr-2009
https://doi.org/10.1109/DATE.2009.5090657
Bofill MNieuwenhuis ROliveras ARodríguez-Carbonell ERubio A(2008)A write-based solver for SAT modulo the theory of arraysProceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design10.5555/1517424.1517438(1-8)Online publication date: 17-Nov-2008
https://dl.acm.org/doi/10.5555/1517424.1517438
Keng BMangassarian HVeneris ANassif SRoychowdhury J(2008)A succinct memory model for automated design debuggingProceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design10.5555/1509456.1509496(137-142)Online publication date: 10-Nov-2008
https://dl.acm.org/doi/10.5555/1509456.1509496
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten