The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - August (2010 vol.59)
pp: 1138-1144
Sudarshan K. Srinivasan , North Dakota State University, Fargo
ABSTRACT
We show how to automatically verify pipelined machines with out-of-order execution using refinement. Our notion of refinement is based on Well-Founded Equivalence Bisimulations. Proving refinement guarantees that a pipelined machine will preserve all safety and liveness properties of its instruction set architecture. Checking liveness—used to ensure that deadlocks do not occur, i.e., there is always forward progress—is essential for out-of-order machines as the control logic is involved and prone to deadlock defects. In previous work on out-of-order verification, liveness checking was either ignored or not automated. We developed two automatic methods based on refinement that check both safety and liveness of out-of-order pipelined machines. We use extensive experimentation based on 14 out-of-order machine models to study and compare these methods. We find overall that the cost of proving both safety and liveness is about 81 percent more than the cost of proving safety alone.
INDEX TERMS
Pipelined machine verification, refinement, out-of-order execution.
CITATION
Sudarshan K. Srinivasan, "Automatic Refinement Checking of Pipelines with Out-of-Order Execution", IEEE Transactions on Computers, vol.59, no. 8, pp. 1138-1144, August 2010, doi:10.1109/TC.2010.18
REFERENCES
[1] AMD Opteron "x86, 64-Bit Processors for Servers and Workstations," http://www.amd.com/us-en/Processors/ProductInformation 030_118_ 8825,00.html , 2008.
[2] T. Arons, "Verification of an Advanced Mips-Type Out-of-Order Execution Algorithm," Proc. Int'l Conf. Computer-Aided Verification (CAV '04), pp. 414-426, 2004.
[3] T. Arons and A. Pnueli, "A Comparison of Two Verification Methods for Speculative Instruction Execution," Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '00), pp. 487-502, Mar. 2000.
[4] R.E. Bryant, S.K. Lahiri, and S. Seshia, "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions," Proc. Int'l Conf. Computer-Aided Verification (CAV '02), pp. 78-92, 2002.
[5] J.R. Burch and D.L. Dill, "Automatic Verification of Pipelined Microprocessor Control," Proc. Int'l Conf. Computer-Aided Verification (CAV '94), pp. 68-80, 1994.
[6] A.C.J. Fox, "Formal Specification and Verification of ARM6," Lecture Notes in Computer Science, vol. 2758, pp. 25-40, Springer Berlin/Heidelberg 2003.
[7] R. Hosabettu, M. Srivas, and G. Gopalakrishnan, "Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach," Proc. Int'l Conf. Computer-Aided Verification (CAV '99), pp. 47-59, 1999.
[8] W.A. Hunt and J. Sawada, "Verifying the FM9801 Microarchitecture," IEEE Micro, vol. 19, no. 3, pp. 47-55, May 1999.
[9] Intel, "Core 2 Duo Processor Overview," http://www.intel.com/products/ processor/ core2duoindex.htm, 2008.
[10] R.B. Jones, J.U. Skakkebæk, and D.L. Dill, "Formal Verification of Out-of-Order Execution with Incremental Flushing," Formal Methods in System Design, Special Issue on Microprocessor Verification, vol. 20, no. 2, pp. 139-158, Mar. 2002.
[11] R. Kane, P. Manolios, and S.K. Srinivasan, "Monolithic Verification of Deep Pipelines with Collapsed Flushing," Proc. Conf. Design, Automation and Test in Europe (DATE '06), pp. 1234-1239, 2006.
[12] M. Kaufmann, P. Manolios, and J.S. Moore, Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, July 2000.
[13] D. Kroning, "Formal Verification of Pipelined Microprocessors," PhD thesis, Universität des Saarlandes, 2001.
[14] S. Lahiri, S. Seshia, and R. Bryant, "Modeling and Verification of Out-of-Order Microprocessors Using UCLID," Proc. Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '02), pp. 142-159, 2002.
[15] P. Manolios, "Correctness of Pipelined Machines," Proc. Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '00), pp. 161-178, 2000.
[16] P. Manolios, "Mechanical Verification of Reactive Systems," PhD thesis, Univ. of Texas at Austin, http://www.cc.gatech.edu/~manolios publications.html , Aug. 2001.
[17] P. Manolios, "A Compositional Theory of Refinement for Branching Time," Proc. 12th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '03), pp. 304-318, 2003.
[18] P. Manolios and S.K. Srinivasan, "Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements," Proc. Conf. Design, Automation and Test in Europe (DATE '04), pp. 168-175, 2004.
[19] P. Manolios and S.K. Srinivasan, "A Complete Compositional Reasoning Framework for the Efficient Verification of Pipelined Machines," Proc. IEEE Int'l Conf. Computer-Aided Design (ICCAD '05), pp. 863-870, 2005.
[20] P. Manolios and S.K. Srinivasan, "A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines," Proc. IEEE Int'l Conf. Formal Methods and Models for Co-Design (MEMOCODE '05), pp. 188-197, July 2005.
[21] H.I. Shehata and M. Aagaard, "A General Decomposition Strategy for Verifying Register Renaming," Proc. Design Automation Conf. (DAC '04), pp. 234-237, 2004.
[22] S.K. Srinivasan, "Efficient Verification of Bit-Level Pipelined Machines Using Refinement," PhD thesis, Georgia Inst. of Technology, http://etd.gatech.edu/theses/availableetd-08242007-111625 /, Dec. 2007.
[23] M.N. Velev, "Using Rewriting Rules and Positive Equality to Formally Verify Wide Issue Out-of-Order Microprocessors with a Reorder Buffer," Proc. Conf. Design, Automation and Test in Europe (DATE '02), pp. 28-35, 2002.
[24] M.N. Velev, "Using Automatic Case Splits and Efficient CNF Translation to Guide a Sat-Solver When Formally Verifying Out-of-Order Processors," Proc. Int'l Symp. Artificial Intelligence and Math. (AI&M), 2004.
[25] M.N. Velev, "Using Positive Equality to Prove Liveness for Pipelined Microprocessors," Proc. Asia and South Pacific Design Automation Conf. (ASP-DAC), pp. 316-321, 2004.
[26] M.N. Velev, "Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units," Proc. Conf. Correct Hardware Design and Verification Methods (CHARME), pp. 97-113, 2005.
[27] Yices, "Home Page," http://fm.csl.sri.comyices, 2007.
35 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool