Skip to main content
SpringerLink
Log in

Getting Formal Verification into Design Flow

  • Conference paper
FM 2008: Formal Methods (FM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5014))

Included in the following conference series:

Abstract

The ultimate goal of formal methods is to provide assurances about the quality, performance, security, etc. of systems. While formal tools have advanced greatly over the past two decades, widespread proliferation has not yet occurred, and the full impact of formal methods is still to be realized. This paper presents some ideas on how to catalyze the growth of formal techniques in day-to-day engineering practice. We draw on our experience as hardware engineers that want to use, and have tried to use, formal methods in our own designs. The points we make have probably been made before. However we illustrate each one with concrete designs. Our examples support three major themes: (1) correctness depends highly on the application and even a collection of formal methods cannot handle the whole problem; (2) high-level design languages can facilitate the interaction between design and formal methods; and (3) formal method tools should be presented as integrated debugging aids as opposed to one requiring mastering a foreign language or esoteric concepts.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Paulson, L.C.: The Relative Consistency of the Axiom of Choice Mechanized using Isabelle/ZF. London Mathematical Society Journal of Computation and Mathematics 6 (2003)

    Google Scholar 

  2. McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University (1992)

    Google Scholar 

  3. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: 14th International Conference on Computer Aided Verification (CAV), Copenhagen, Denmark (2002)

    Google Scholar 

  4. de Moura, L., Bjorner, N.: Z3: An Efficient SMT Solver. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary (2008)

    Google Scholar 

  5. Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The Bit-Level Analysis Tool. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV), Berlin, Germany (2007)

    Google Scholar 

  6. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th conference on Design automation (DAC), Las Vegas, NV (2001)

    Google Scholar 

  7. Mentor Graphics Corp.: 0-In® Formal Verification, www.mentor.com/products/fv/abv/0-in_fv/

  8. Synopsys, Inc.: Formality® Equivalence Checker, www.synopsys.com/products/verification/

  9. Mentor Graphics Corp.: FormalProTM, www.mentor.com/products/fv/ev/formalpro/

  10. Cadence Design Systems, Inc.: Cadence® Encounter® Conformal® Equivalence Checker, www.cadence.com/products/digital_ic/conformal/index.aspx

  11. Jasper Design Automation, Inc.: JasperGold® Verification System, www.jasper-da.com/products_jaspergold.htm

  12. Cadence Design Systems, Inc.: Incisive® Formal Verifier, www.cadence.com/products/functional_ver/incisive_formal_verifier/index.aspx

  13. Meadows, C.: The NRL Protocol Analyzer: An Overview. The Journal of Logic Programming 26(2), 113–131 (1996)

    Article  MATH  Google Scholar 

  14. Kwiatkowska, M.Z., Norman, G., Sproston, J.: Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Proceedings of the Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV), Copenhagen, Denmark (2002)

    Google Scholar 

  15. Burch, J.R., Dill, D.L.: Automatic Verification of Pipelined Microprocessor Control. In: Proceedings of the 6th International Conference on Computer Aided Verification (CAV), Stanford, CA (1994)

    Google Scholar 

  16. Stoy, J.E., Shen, X., Arvind.: Proofs of Correctness of Cache-Coherence Protocols. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 47–71. Springer, Heidelberg (2001)

    Google Scholar 

  17. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI), San Diego, CA (2002)

    Google Scholar 

  18. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Portland, OR (2002)

    Google Scholar 

  19. Russinoff, D.M.: A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD AthlonTM Processor. In: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX (2000)

    Google Scholar 

  20. Seger, C.J., Jones, R., O’Leary, J., Melham, T., Aagaard, M., Barrett, C., Syme, D.: An Industrially Effective Environment for Formal Hardware Verification. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on 24(9), 1381–1405 (2005)

    Article  Google Scholar 

  21. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP), Edinburgh, UK (2005)

    Google Scholar 

  22. Berry, G.: The Foundations of Esterel, 425–454 (2000)

    Google Scholar 

  23. Arvind, N.R.S., Rosenband, D.L., Dave, N.: High-level synthesis: an essential ingredient for designing complex ASICs. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, CA (2004)

    Google Scholar 

  24. IEEE: IEEE standard 802.11a supplement. Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications (1999)

    Google Scholar 

  25. International Telecommunication Union: H.264, www.itu.int/rec/T-REC-H.264

  26. Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M., Yu, Y.: Checking Cache-Coherence Protocols with TLA+. Form. Methods Syst. Des. 22(2) (2003)

    Google Scholar 

  27. Arvind, S.X.: Using Term Rewriting Systems to Design and Verify Processors. IEEE Micro 19(3), 36–46 (1999)

    Article  Google Scholar 

  28. Krstić, S., Jones, R.B., O’Leary, J.: Mothers of Pipelines. Electron. Notes Theor. Comput. Sci. 174(8), 7–22 (2007)

    Article  Google Scholar 

  29. Manolios, P.: Correctness of Pipelined Machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 161–178. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  30. Dave, N., Pellauer, M., Gerding, S., Arvind.: 802.11a Transmitter: A Case Study in Microarchitectural Exploration. In: Proceedings of Formal Methods and Models for Codesign (MEMOCODE), Napa, CA (2006)

    Google Scholar 

  31. Bluespec, Inc. Waltham, MA: Bluespec SystemVerilog Ver. 3.8 Reference Guide (November 2004)

    Google Scholar 

  32. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  33. Berry, G.: The Esterel v5 Language Primer Version v5_91 (2000)

    Google Scholar 

  34. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall PTR, Upper Saddle River (1997)

    Google Scholar 

  35. Dave, N., Ng, M.C., Arvind.: Automatic Synthesis of Cache-Coherence Protocol Processors Using Bluespec. In: Proc. of Formal Methods and Models for Codesign, Verona, Italy (2005)

    Google Scholar 

  36. Dave, N., Ng, M.C., Arvind.: Standard for SystemVerilog: Unified Hardware Design, Specification and Verification Language (IEEE Std. 1800-2007)

    Google Scholar 

  37. Holzmann, G.J.: The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  38. Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)

    Google Scholar 

  39. Owre, S., Rushby, J.M., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Proceedings of the 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY (1992)

    Google Scholar 

  40. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, London (2002)

    MATH  Google Scholar 

  41. SRI International: Yices, yices.csl.sri.com/index.shtml

  42. Jackson, D.: Alloy: A Lightweight Object Modelling Notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)

    Article  Google Scholar 

  43. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    MATH  Google Scholar 

  44. Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing (PODC), Vancouver, British Columbia (1987)

    Google Scholar 

  45. Archer, L.M.H.L., Mitra, N., Umeno, S.: Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit. In: Proceedings. Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Napa, CA (2006)

    Google Scholar 

  46. Shen, X.: Design and Verification of Adaptive Cache Coherence Protocols. PhD thesis, MIT, Cambridge, MA (2000)

    Google Scholar 

  47. Shen, X., Rudolph, L., Arvind,: CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems. In: Proceedings of the 13th ACM SIGARCH International Conference on Supercomputing, IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, MA 02139, USA

    Arvind & Nirav Dave

  2. Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA

    Michael Katelman

Authors
  1. Arvind
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nirav Dave
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Katelman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jorge Cuellar Tom Maibaum Kaisa Sere

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arvind, Dave, N., Katelman, M. (2008). Getting Formal Verification into Design Flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-68237-0_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68235-6

  • Online ISBN: 978-3-540-68237-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation