skip to main content
research-article

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

Published: 25 July 2008 Publication History

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]
Aagaard, M., Cook, B., Day, N. A., and Jones, R. B. 2001. A framework for microprocessor correctness statements. In Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Livingston, UK. T. Margaria and T. F. Melham, eds. Lecture Notes in Computer Science, vol. 2144. Springer, 433--448.]]
[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]
Abadir, M. S., Albin, K., Havlicek, J., Krishnamurthy, N., and Martin, A. K. 2003. Formal verification successes at Motorola. Formal Meth. Syst. Des. 22, 2, 117--123.]]
[4]
Arons, T. and Pnueli, A. 2000. A comparison of two verification methods for speculative instruction execution. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Berlin. Lecture Notes in Computer Science, vol. 1785. Springer, 487--502.]]
[5]
Bentley, B. 2001. Validating the Intel Pentium 4 microprocessor. In Proceedings of the ACM Design Automation Conference (DAC). ACM, 244--248.]]
[6]
Bentley, B. 2005. Validating a modern microprocessor. http://www.cav2005.inf.ed.ac.uk/bentley_CAV_07_08_2005.ppt.]]
[7]
Bryant, R. E., German, S., and Velev, M. N. 1999. Exploiting positive equality in a logic of equality with uninterpreted functions. In Proceedings of the Computer-Aided Verification (CAV), Trento, Italy. N. Halbwachs and D. Peled, eds. Lecture Notes in Computer Science, vol. 1633. Springer, 470--482.]]
[8]
Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proceedings of the Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, eds. Lecture Notes in Computer Science, vol. 2404. Springer, 78--92.]]
[9]
Burch, J. R. and Dill, D. L. 1994. Automatic verification of pipelined microprocessor control. In Proceedings of the Computer-Aided Verification (CAV), D. L. Dill, ed. Lecture Notes in Computer Science, vol. 818. Springer, 68--80.]]
[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]
Huggins, J. K. and Campenhout, D. V. 1998. Specification and verification of pipelining in the ARM2 RISC microprocessor. ACM Trans. Des. Autom. Electron. Syst. 3, 4, 563--580.]]
[14]
Jones, R., Skakkebæk, J., and Dill, D. 1998. Reducing manual abstraction in formal verification of out-of-order execution. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD), Palo Alto, CA. G. Gopalakrishnan and P. Windley, eds. Lecture Notes in Computer Science, vol. 1522. Springer, 2--17.]]
[15]
Kane, R., Manolios, P., and Srinivasan, S. K. 2006. Monolithic verification of deep pipelines with collapsed flushing. In Proceedings of the Design Automation and Test in Europe (DATE), Leuven, Belgium. G. G. E. Gielen, ed. European Design and Automation Association, 1234--1239.]]
[16]
Kaufmann, M., Manolios, P., and Moore, J. S., Eds. 2000a. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic.]]
[17]
Kaufmann, M., Manolios, P., and Moore, J. S. 2000b. Computer-Aided Reasoning: An Approach. Kluwer Academic.]]
[18]
Kroening, D. 2001. Formal verification of pipelined microprocessors. Ph.D. thesis, Universität des Saarlandes.]]
[19]
Lahiri, S., Seshia, S., and Bryant, R. 2002. Modeling and verification of out-of-order microprocessors using UCLID. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD), Portland, OR. Lecture Notes in Computer Science, vol. 2517. Springer, 142--159.]]
[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]
Manolios, P. 2000. Correctness of pipelined machines. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD), W. A. H., Jr. and S. D. Johnson, eds. Lecture Notes in Computer Science, vol. 1954. Springer, 161--178.]]
[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]
Manolios, P. and Srinivasan, S. K. 2004. Automatic verification of safety and liveness for XScale-like processor models using WEB refinements. In Proceedings of the Design, Automation, and Test in Europe (DATE). IEEE Computer Society, 168--175.]]
[26]
Manolios, P. and Srinivasan, S. K. 2005a. A complete compositional reasoning framework for the efficient verification of pipelined machines. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), San Jose, CA. IEEE Computer Society, 863--870.]]
[27]
Manolios, P. and Srinivasan, S. K. 2005b. A computationally efficient method based on commitment refinement maps for verifying pipelined machines. In Proceedings of the International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE, 188--197.]]
[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]
Manolios, P. and Srinivasan, S. K. 2005d. Refinement maps for efficient verification of processor models. In Proceedings of the Design Automation and Test in Europe (DATE). IEEE Computer Society, 1304--1309.]]
[30]
McMillan, K. L. 1998. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In Proceedings of the Computer Aided Verification (CAV), Van Couver, British Colombia, Canada. A. J. Hu and M. Y. Vardi, eds. Lecture Notes in Computer Science, vol. 1427. Springer, 110--121.]]
[31]
Mishra, P. and Dutt, N. D. 2002. Modeling and verification of pipelined embedded processors in the presence of hazards and exceptions. In Proceedings of the IFIP WCC Stream 7 on Distributed and Parallel Embedded Systems (DIPES), Montreal, Qubec, Canada, vol. 219. B. Kleinjohann et al., eds. Kluwer, 81--90.]]
[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]
Patankar, V. A., Jain, A., and Bryant, R. E. 1999. Formal verification of an ARM processor. In Proceedings of the 12th International Conference on VLSI Design, Goa, India. IEEE, 282--287.]]
[34]
Ryan, L. 2008. Siege homepage. http://www.cs.sfu.ca/~loryan/personal.]]
[35]
Sawada, J. 1999. Formal verification of an advanced pipelined machine. Ph.D. thesis, University of Texas at Austin. http://www.cs.utexas.edu/users/sawada/dissertation/.]]
[36]
Sawada, J. and Hunt, W. A. 2002. Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Formal Meth. Syst. Des. 20, 2, 187--222.]]
[37]
Srivas, M. and Bickford, M. 1990. Formal verification of a pipelined microprocessor. IEEE Softw. 7, 5, 52--64.]]
[38]
Velev, M. N. 2004. Using positive equality to prove liveness for pipelined microprocessors. In Proceedings of the Asia and South Pacific Design Automation Conference (ASPDAC), Yokohama, Japan. M. Imai, ed. IEEE, 316--321.]]
[39]
Velev, M. N. and Bryant, R. E. 2000. Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. In Proceedings of the ACM Design Automation Conference (DAC), Los Angeles, CA. ACM Press, 112--117.]]

Cited By

View all
  • (2023)Verification of GossipSub in ACL2sElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.393.10393(113-132)Online publication date: 14-Nov-2023
  • (2022)Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models2022 27th Asia and South Pacific Design Automation Conference (ASP-DAC)10.1109/ASP-DAC52403.2022.9712564(154-159)Online publication date: 17-Jan-2022
  • (2015)A formal verification methodology for DDD mode pacemaker control programsJournal of Electrical and Computer Engineering10.1155/2015/9390282015(57-57)Online publication date: 1-Jan-2015
  • Show More Cited By

Index Terms

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

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Transactions on Design Automation of Electronic Systems
    ACM Transactions on Design Automation of Electronic Systems  Volume 13, Issue 3
    July 2008
    370 pages
    ISSN:1084-4309
    EISSN:1557-7309
    DOI:10.1145/1367045
    Issue’s Table of Contents
    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]

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Journal Family

    Publication History

    Published: 25 July 2008
    Accepted: 01 November 2007
    Revised: 01 September 2006
    Received: 01 December 2005
    Published in TODAES Volume 13, Issue 3

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. Refinement maps
    2. SAT
    3. bisimulation
    4. commitment
    5. flushing
    6. liveness
    7. pipelined machines
    8. refinement
    9. verification

    Qualifiers

    • Research-article
    • Research
    • Refereed

    Funding Sources

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)3
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 15 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2023)Verification of GossipSub in ACL2sElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.393.10393(113-132)Online publication date: 14-Nov-2023
    • (2022)Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models2022 27th Asia and South Pacific Design Automation Conference (ASP-DAC)10.1109/ASP-DAC52403.2022.9712564(154-159)Online publication date: 17-Jan-2022
    • (2015)A formal verification methodology for DDD mode pacemaker control programsJournal of Electrical and Computer Engineering10.1155/2015/9390282015(57-57)Online publication date: 1-Jan-2015
    • (2015)Modular Deductive Verification of Multiprocessor Hardware DesignsComputer Aided Verification10.1007/978-3-319-21668-3_7(109-127)Online publication date: 14-Jul-2015
    • (2011)Verifying deadlock-freedom of communication fabricsProceedings of the 12th international conference on Verification, model checking, and abstract interpretation10.5555/1946284.1946300(214-231)Online publication date: 23-Jan-2011
    • (2011)Controller synthesis for pipelined circuits using uninterpreted functionsProceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2011.5970508(31-42)Online publication date: 1-Jul-2011
    • (2011)Verifying Deadlock-Freedom of Communication FabricsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-642-18275-4_16(214-231)Online publication date: 2011
    • (2010)Utility of transaction-level hardware models in refinement checking2010 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2010.5496650(121-128)Online publication date: Jun-2010
    • (2009)Industrial strength refinement checking2009 Formal Methods in Computer-Aided Design10.1109/FMCAD.2009.5351123(180-183)Online publication date: Nov-2009

    View Options

    Login options

    Full Access

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media