Automatic verification of safety and liveness for pipelined machines using WEB refinement

ABSTRACT

We show how to automatically verify that complex pipelined machine models satisfy the same safety and liveness properties as their instruction-set architecture (ISA) models by using well-founded equivalence bisimulation (WEB) refinement. We show how to reduce WEB-refinement proof obligations to formulas expressible in the decidable logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). This allows us to automate the verification of the pipelined machine models by using the UCLID decision procedure to transform CLU formulas to Boolean satisfiability problems. To relate pipelined machine states to ISA states, we use the commitment and flushing refinement maps. We evaluate our work using 17 pipelined machine models that contain various features, including deep pipelines, precise exceptions, branch prediction, interrupts, and instruction queues. Our experimental results show that the overhead of proving liveness, obtained by comparing the cost of proving both safety and liveness with the cost of only proving safety, is about 17%, but depends on the refinement map used; for example, the liveness overhead is 23% when flushing is used and is negligible when commitment is used.

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: Aagaard, M., Cook, B., Day, N. A., and Jones, R. B. 2003. A framework for superscalar microprocessor correctness statements. Int. J. Softw. Tools Technol. Transfer 4, 3, 298--312.
• 3: Magdy S. Abadir , Kenneth L. Albin , John Havlicek , Narayanan Krishnamurthy , Andrew K. Martin, Formal Verification Successes at Motorola, Formal Methods in System Design, v.22 n.2, p.117-123, March 2003 [doi>10.1023/A:1022917321255]
• 4: Tamarah Arons , Amir Pnueli, A Comparison of Two Verification Methods for Speculative Instruction Execution, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.487-502, March 25-April 02, 2000
• 5: Bob Bentley, Validating the intel pentium 4 microprocessor, Proceedings of the 38th conference on Design automation, p.244-248, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378473]
• 6: Bentley, B. 2005. Validating a modern microprocessor. http://www.cav2005.inf.ed.ac.uk/bentley_CAV_07_08_2005.ppt.
• 7: Randal E. Bryant , Steven M. German , Miroslav N. Velev, Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions, Proceedings of the 11th International Conference on Computer Aided Verification, p.470-482, July 06-10, 1999
• 8: 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
• 9: 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
• 10: de Moura, L. 2006. Yices homepage. http://fm.csl.sri.com/yices.
• 11: Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2004. DPLL(T): Fast decision procedures. In Proceedings of the Computer-Aided Verification (CAV), Boston, MA. R. Alur and D. Peled, eds. Lecture Notes in Computer Science, vol. 3114. Springer, 175--188.
• 12: Hosabettu, R., Srivas, M., and Gopalakrishnan, G. 1999. Proof of correctness of a processor with reorder buffer using the completion functions approach. In Proceedings of the Computer-Aided Verification (CAV), Trento, Italy. N. Halbwachs and D. Peled, eds. Lecture Notes in Computer Science, vol. 1633. Springer, 686--698.
• 13: 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]
• 14: Robert B. Jones , Jens U. Skakkebæk , David L. Dill, Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.2-17, November 04-06, 1998
• 15: Roma Kane , Panagiotis Manolios , Sudarshan K. Srinivasan, Monolithic verification of deep pipelines with collapsed flushing, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 16: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 17: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 18: Kroening, D. 2001. Formal verification of pipelined microprocessors. Ph.D. thesis, Universität des Saarlandes.
• 19: 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
• 20: Ludden, J. M., Roesner, W., Heiling, G. M., Reysa, J. R., Jackson, J. R., Chu, B.-L., Behm, M. L., Baumgartner, J., Peterson, R. D., Abdulhafiz, J., Bucy, W. E., Klaus, J. H., Klema, D. J., Le, T. N., Lewis, F. D., Milling, P. E., McConville, L. A., Nelson, B. S., Paruthi, V., Pouarz, T. W., Romonosky, A. D., Stuecheli, J., Thompson, K. D., Victor, D. W., and Wile, B. 2002. Functional verification of the POWER4 microprocessor and POWER4 multiprocessor system. IBM J. Res. Devel. 46, 1, 53--76.
• 21: Panagiotis Manolios, Correctness of Pipelined Machines, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.161-178, November 01-03, 2000
• 22: Manolios, P. 2001. Mechanical verification of reactive systems. Ph.D. thesis, University of Texas at Austin. http://www.cc.gatech.edu/~manolios/publications.html.
• 23: Manolios, P. 2003. A compositional theory of refinement for branching time. In Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME), D. Geist and E. Tronci, eds. Lecture Notes in Computer Science, vol. 2860. Springer, 304--318.
• 24: Manolios, P. and Srinivasan, S. K. 2003. Automatic verification of safety and liveness for XScale-like processor models using WEB refinements. Tech. Rep. GIT-CERCS-03-17, Georgia Institute of Technology, College of Computing. September.
• 25: 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
• 26: 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
• 27: P. Manolios , S. K. Srinivasan, A computationally ef~cient method based on commitment re~nement maps for verifying pipelined machines., Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design, p.188-197, July 11-14, 2005 [doi>10.1109/MEMCOD.2005.1487914]
• 28: Manolios, P. and Srinivasan, S. K. 2005c. A parameterized benchmark suite of hard pipelined machine verification problems. http://www.cc.gatech.edu/~manolios/benchmarks/charme.html.
• 29: 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]
• 30: Kenneth L. McMillan, Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.110-121, June 28-July 02, 1998
• 31: 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
• 32: Owre, S., Shankar, N., Rushby, J. M., and Stringer-Calvert, D. W. J. 2001. PVS system guide. http://pvs.csl.sri.com/doc/pvs-system-guide.pdf.
• 33: V. A. Patankar , A. Jain , R. E. Bryant, Formal Verification of an ARM Processor, Proceedings of the 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', p.282, January 10-13, 1999
• 34: Ryan, L. 2008. Siege homepage. http://www.cs.sfu.ca/~loryan/personal.
• 35: Jun Sawada , Warren A. Hunt, Jr. , Donald Fussell, Formal verification of an advanced pipelined machine, The University of Texas at Austin, 1999
• 36: Jun Sawada , Warren A. Hunt, Jr., Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability, Formal Methods in System Design, v.20 n.2, p.187-222, March 2002 [doi>10.1023/A:1014122630277]
• 37: 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]
• 38: Miroslav N. Velev, Using positive equality to prove liveness for pipelined microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, January 27-30, 2004, Yokohama, Japan
• 39: 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]

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Design, Reliability

Keywords:
Refinement maps, SAT, bisimulation, commitment, flushing, liveness, pipelined machines, refinement, verification