Monolithic verification of deep pipelines with collapsed flushing

ABSTRACT

We introduce collapsed flushing, a new flushing-based refinement map for automatically verifying safety and liveness properties of term-level pipelined machine models. We also present a new method for handling liveness that is both simpler to define and easier to verify than previous approaches. To empirically validate collapsed flushing, we ran extensive experiments which show more than an order-of-magnitude improvement in verification times over standard flushing. Furthermore, by combining collapsed flushing with commitment refinement maps, we can monolithically verify complex pipelined machine models with deep pipelines---a salient feature of state-of-the-art microprocessor designs---that previous approaches cannot handle.

REFERENCES

• 1: 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
• 2: Jerry R. Burch, Techniques for verifying superscalar microprocessors, Proceedings of the 33rd annual conference on Design automation, p.552-557, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240623]
• 3: 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
• 4: L. de Moura. Yices homepage. See URL http://-fm.csl.sri.com/yices.
• 5: H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 175--188. Springer, 2004.
• 6: 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.
• 7: Intel Pentium 4 Processor - Product Overview, 2005. See URL http://www.intel.com/design/-pentium4/prodbref/.
• 8: Robert B. Jones , Jens U. Skakkebæk , David L. Dill, Formal Verification of Out-of-Order Execution with Incremental Flushing, Formal Methods in System Design, v.20 n.2, p.139-158, March 2002 [doi>10.1023/A:1014118529369]
• 9: 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
• 10: P. Manolios. Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin, August 2001. See URL http://www.cc.gatech.edu/~manolios/-publications.html.
• 11: 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
• 12: 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
• 13: P. Manolios and S. Srinivasan. A computationally efficient method based on commitment refinement maps for verifying pipelined machines models. In ACM-IEEE International Conference on Formal Methods and Models for Codesign, pages 189--198, 2005.
• 14: P. Manolios and S. Srinivasan. A parameterized benchmark suite of hard pipelined-machine-verification problems. In D. Borrione and W. Paul, editors, Correct Hardware Design and Verification Methods (CHARME'05), LNCS, pages 363--366. Springer-Verlag, 2005.
• 15: Panagiotis Manolios , Sudarshan K. Srinivasan, Refinement Maps for Efficient Verification of Processor Models, Proceedings of the conference on Design, Automation and Test in Europe, p.1304-1309, March 07-11, 2005 [doi>10.1109/DATE.2005.257]
• 16: L. Ryan. Siege homepage. See URL http://www.cs.-sfu.ca/~loryan/personal.
• 17: Jun Sawada, Verification of a simple pipelined machine model, Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, Norwell, MA, 2000