Advertisement

Applications of Hierarchical Verification in Model Checking

  • Robert Beers
  • Rajnish Ghughal
  • Mark Aagaard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)

Abstract

The LTL model checker that we use provides sound decomposition mechanisms within a purely model checking environment. We have exploited these mechanisms to successfully verify a wide spectrum of large and complex circuits. This paper describes a variety of the decomposition techniques that we have used as part of a large industrial formal verification effort on the Intel Pentium® 4 (Willamette) processor.

Keywords

Model Check Theorem Prove Proof System Decomposition Technique Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    M. D. Aagaard, R. B. Jones, K. R. Kohatsu, R. Kaivola, and C.-J. H. Seger. Formal verification of iterative algorithms in microprocessors. In DAC, June 2000.Google Scholar
  2. 2.
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Formal verification using parametric representations of Boolean constraints. In DAC, July 1999. (Short paper).Google Scholar
  3. 3.
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. In L. Thery, editor, Theorem Proving in Higher Order Logics, pages 323–340. Springer Verlag; New York, Sept. 1999.CrossRefGoogle Scholar
  4. 4.
    A. Camilleri. A hybrid approach to verifying liveness in a symmetric multi-processor. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics, pages 49–68. Springer Verlag; New York, Sept. 1997.CrossRefGoogle Scholar
  5. 5.
    Y.-A. Chen and R. Bryant. Verification of floating-point adders. In A. J. Hu and M. Y Vardi, editors, CAV, pages 488–499, July 1998.Google Scholar
  6. 6.
    E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans, on Prog. Lang. and Systems, 16(5):1512–1542, Sept. 1994.Google Scholar
  7. 7.
    E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In LICS, pages 353–362, 1989.Google Scholar
  8. 8.
    E. M. J. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press; Cambridge, MA, 1999.Google Scholar
  9. 9.
    A. P. Eiríkson. The formal design of 1m-gate ASICs. In P. Windley and G. Gopalakrishnan, editors, Formal Methods in CAD, pages 49–63. Springer Verlag; New York, Nov. 1998.Google Scholar
  10. 10.
    M. Gordon. Programming combinations of deduction and BDD-based symbolic calculation. Technical Report 480, Cambridge Comp. Lab, 1999.Google Scholar
  11. 11.
    IEEE. IEEE Standard for binary floating-point arithmetic. ANSI/IEEE Std 754-1985, 1985.Google Scholar
  12. 12.
    J.-Y Jang, S. Qadeer, M. Kaufmann, and C. Pixley. Formal verification of FIRE: A case study. In DAC, pages 173–177, June 1997.Google Scholar
  13. 13.
    J. Joyce and C.-J. Seger. Linking BDD based symbolic evaluation to interactive theorem proving. In DAC, June 1993.Google Scholar
  14. 14.
    G. Kamhi, L. Fix, and O. Weissberg. Automatic datapath extraction for efficient usage of hdds. In O. Grumberg, editor, CAV, pages 95–106. Springer Verlag; New York, 1997.Google Scholar
  15. 15.
    S. Mador-Haim and L. Fix. Input elimination and abstraction in model checking. In P. Windley and G. Gopalakrishnan, editors, Formal Methods in CAD, pages 304–320. Springer Verlag; New York, Nov. 1998.Google Scholar
  16. 16.
    K. McMillan. Minimalist proof assistants: Interactions of technology and methodology in formal system level verification. In G. C. Gopalakrishnan and P. J. Windley, editors, Formal Methods in CAD, page 1. Springer Verlag; New York, Nov. 1998.Google Scholar
  17. 17.
    S. P. Miller and M. Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In Workshop on Industrial-Strength Formal Specification Techniques, Apr. 1995.Google Scholar
  18. 18.
    Y. Xu, E. Cerny, A. Silburt, A. Coady, Y. Liu, and P. Pownall. Practical application of formal verification techniques on a frame mux/demux chip from Nortel Semiconductors. In L. Pierre and T. Kropf, editors, CHARME, pages 110–124. Springer Verlag; New York, Oct. 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Robert Beers
    • 1
  • Rajnish Ghughal
    • 1
  • Mark Aagaard
    • 1
  1. 1.Performance Microprocessor DivisionIntel CorporationHillsboroUSA

Personalised recommendations