Automatic memory reductions for RTL model verification

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: Zaher S. Andraus , Mark H. Liffiton , Karem A. Sakallah, Refinement strategies for verification methods based on datapath abstraction, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan [doi>10.1145/1118299.1118306]
• 2: William R. Bevier , Warren A. Hunt, Jr. , J. Strother Moore , William D. Young, An approach to systems verification, Journal of Automated Reasoning, v.5 n.4, p.411-428, Dec. 1989
• 3: P. Bjesse , A. Boralv, DAG-aware circuit compression for formal verification, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.42-49, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382541]
• 4: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 5: 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
• 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: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 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: Malay K. Ganai , Aarti Gupta , Pranav Ashar, Verification of Embedded Memory Systems using Efficient Memory Modeling, Proceedings of the conference on Design, Automation and Test in Europe, p.1096-1101, March 07-11, 2005 [doi>10.1109/DATE.2005.325]
• 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: Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065697]
• 13: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 14: Panagiotis Manolios , Sudarshan K. Srinivasan, Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements, Proceedings of the conference on Design, automation and test in Europe, p.10168, February 16-20, 2004
• 15: P. Manolios , S. K. Srinivasan, A complete compositional reasoning framework for the efficient verification of pipelined machines, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.863-870, November 06-10, 2005, San Jose, CA
• 16: P. Manolios , S. K. Srinivasan, Verification of executable pipelined machines with bit-level interfaces, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.855-862, November 06-10, 2005, San Jose, CA
• 17: L. Ryan. Siege homepage. See URL http://www.cs.sfu.ca/~loryan/personal.
• 18: 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
• 19: Ultrasparc processors. See URL http://-www.sun.com/processors/technologies.html.
• 20: Miroslav N. Velev , Randal E. Bryant , Alok Jain, Efficient Modeling of Memory Arrays in Symbolic Simulation, Proceedings of the 9th International Conference on Computer Aided Verification, p.388-399, June 22-25, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.1 Design
          Subjects: Memory design

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Memory technologies
      B.7.2 Design Aids
          Subjects: Verification
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids

General Terms:
Design, Performance, Verification