Advertisement

Combining Stream-Based and State-Based Verification Techniques

  • Nancy A. Day
  • Mark D. Aagaard
  • Byron Cook
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

Algebraic verification techniques manipulate the structure of a circuit while preserving its behavior. Algorithmic verification techniques verify properties about the behavior of a circuit. These two techniques have complementary strengths: algebraic techniques are largely independent of the size of the state space, and algorithmic techniques are highly automated. It is desirable to exploit both in the same verification. However, algebraic techniques often use stream-based models of circuits, while algorithmic techniques use state-based models. We prove the consistency of stream- and state-based interpretations of circuit models, and show how stream-based veri_cation results can be used hand-in-hand with state-based veri_cation results. Our approach allows us to combine stream-based algebraic rewriting and state-based reasoning, using SMV and SVC, to verify a pipelined microarchitecture with speculative execution.

Keywords

Observation Function Hardware Description Language Symbolic Model Check Algorithmic Technique Lambda Calculus 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. D. Aagaard and M. E. Leeser. Reasoning about pipelines with structural hazards. In Theorem Provers in Circuit Design (TPCD). pages 13–32, Springer, 1994.Google Scholar
  2. 2.
    S. Bainbridge, A. Camilleri, and R. Fleming. Theorem proving as an industrial tool for system level design. In Theorem Provers in Circuit Design (TPCD), pages 253–274. Elsevier Science Publishers, 1992.Google Scholar
  3. 3.
    C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In FMCAD, volume 1166 of LNCS, pages 187–201. Springer, 1996.Google Scholar
  4. 4.
    P. Bjesse, K. Claessen, M. Sheeran, and S. Singh. Lava: Hardware design in Haskell. In ACM Int. Conf. on Functional Programming (ICFP), pages 174–184. ACM Press, 1998.Google Scholar
  5. 5.
    R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. V. Tassel. Experience with embedding hardware description languages in HOL. In Theorem Provers in Circuit Design (TPCD). pages 129–156, Elsevier, 1992.Google Scholar
  6. 6.
    J. R. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990.Google Scholar
  7. 7.
    J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In Computer Aided Verification (CAV), volume 818 of LNCS, pages 68–80. Springer, 1994.Google Scholar
  8. 8.
    K. Claessen and D. Sands. Observable sharing for functional circuit description. In Asian Computing Science Conference, 1999.Google Scholar
  9. 9.
    K. Claessen and M. Sheeran. A tutorial on Lava: A hardware description and verification system. April 9, 2000.Google Scholar
  10. 10.
    E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.zbMATHCrossRefGoogle Scholar
  11. 11.
    B. Cook, J. Launchbury, and J. Matthews. Specifying superscalar microprocessors in Hawk. In Workshop on Formal Techniques for Hardware, 1998.Google Scholar
  12. 12.
    N. A. Day, J. Launchbury, and J. Lewis. Logical abstractions in Haskell. In Proceedings of the 1999 Haskell Workshop. Utrecht University Department of Computer Science, Technical Report UU-CS-1999-28, October 1999.Google Scholar
  13. 13.
    M. Gordon. Reachability programming in Hol98 using BDDs. To appear in 13th International Conference on Theorem Proving and Higher Order Logics (TPHOLs), August, 2000.Google Scholar
  14. 14.
    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.Google Scholar
  15. 15.
    S. D. Johnson, B. Bose, and C. D. Boyer. A tactical framework for digital design. In VLSI Specification, Verification and Synthesis, pages 349–384. Kluwer, 1988.Google Scholar
  16. 16.
    G. Jones and M. Sheeran. Circuit design in Ruby. In Formal Methods for VLSI Design, pages 13–70. Elsevier Science Publications, 1990.Google Scholar
  17. 17.
    J. Matthews, B. Cook, and J. Launchbury. Microprocessor specification in Hawk. In International Conference on Computer Languages, 1998.Google Scholar
  18. 18.
    J. Matthews and J. Launchbury. Elementary microarchitecture algebra. In Computer Aided Verification (CAV), volume 1633 of LNCS, pages 288–300. Springer, 1999.CrossRefGoogle Scholar
  19. 19.
    K. L. McMillan. SymbolicModel Checking. PhD thesis, Carnegie Mellon University, May 1992.Google Scholar
  20. 20.
    R. Milner. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 481–489. The British Computer Society, 1971.Google Scholar
  21. 21.
    R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989.zbMATHGoogle Scholar
  22. 22.
    J. C. Mitchell. Foundations for programming languages. MIT Press, 1996.Google Scholar
  23. 23.
    J. C. Mitchell and A. R. Meyer. Second-order logical relations (extended abstract). In Logic of Programs, volume 193 of LNCS, pages 225–236. Springer, 1985.Google Scholar
  24. 24.
    J. O’Donnell. Generating netlists from executable functional circuit specifications in a pure functional language. In Functional Programming Glasgow, Workshops in Computing, pages 178–194. Springer, 1992Google Scholar
  25. 25.
    D. Park. Concurrency and automata on in_nite sequences. In 5th GI Conference on Theorectical Computer Science, volume 104 of LNCS. Springer, 1981.Google Scholar
  26. 26.
    L. C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Lab, 1993. Latest edition: 24 November 1997.Google Scholar
  27. 27.
    J. Peterson and K. Hammond, editors. Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.4). Yale University, Department of Computer Science, RR-1106, February 1997.Google Scholar
  28. 28.
    J. Sawada and W. Hunt. Trace table based approach for pipelined microprocessor verification. In Computer Aided Verification (CAV), volume 1254 of LNCS, pages 364–375. Springer, 1997.Google Scholar
  29. 29.
    J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using transformations and verification in circuit design. In Designing Correct Circuits, 1992.Google Scholar
  30. 30.
    C. J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147–189, March 1995.Google Scholar
  31. 31.
    R. Sharp. T-Ruby: A tool for handing Ruby expressions. August, 1996.Google Scholar
  32. 32.
    S. Singh. Implementation of a nonstandard interpretation system. In Functional Programming, Glasgow, Workshops in Computing, pages 206–224. Springer, 1989.Google Scholar
  33. 33.
    P. Wadler. Theorems for free! In Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA89), pages 347–359, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Nancy A. Day
    • 1
  • Mark D. Aagaard
    • 2
  • Byron Cook
    • 1
  1. 1.Oregon Graduate InstituteBeavertonUSA
  2. 2.Performance Microprocessor DivisionIntel CorporationHillsboroUSA

Personalised recommendations