Skip to main content
SpringerLink
Log in

Symbolic Trajectory Evaluation

  • Chapter
  • First Online:
Handbook of Model Checking

Abstract

Symbolic trajectory evaluation is an industrial-strength formal hardware verification method, based on symbolic simulation, which has been highly successful in data-path verification, especially for microprocessor execution units. It is a ‘model-checking’ method in the basic sense that properties, expressed in a simple temporal logic, are verified by (symbolic) exploration of formal models of sequential circuits. Its defining characteristic is that it operates by symbolic simulation over abstractions of sets of states that only partially delineate the circuit states in the set. These abstract state sets are ordered in a lattice by information content, based on a three-valued domain for values on circuit nodes (true, false, and don’t know). The algorithm operates over families of these abstractions encoded by Boolean formulas, providing a flexible, specification-driven mechanism for partitioned data abstraction. We provide a basic introduction to symbolic trajectory evaluation and its extensions, and some details of how it is deployed in industrial practice. The aim is to get across the essence and value of the method in clear and accessible terms.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aagaard, M.D., Jones, R.B., Melham, T.F., O’Leary, J.W., Seger, C.J.H.: A methodology for large-scale hardware verification. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 1954, pp. 263–282. Springer, Heidelberg (2000)

    Google Scholar 

  2. Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: Design Automation Conf. (DAC), pp. 538–541. IEEE, Piscataway (1998)

    Google Scholar 

  3. Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conf. (DAC), pp. 402–407. ACM, New York (1999)

    Google Scholar 

  4. Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Lifted-FL: a pragmatic implementation of combined model checking and theorem proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 1690, pp. 323–340. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Adams, S., Björk, M., Melham, T., Seger, C.J.: Automatic abstraction in symbolic trajectory evaluation. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 127–135. IEEE, Piscataway (2007)

    Chapter  Google Scholar 

  6. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5, 49–58 (2003)

    Article  Google Scholar 

  7. Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: Design Automation Conf. (DAC), pp. 596–602. ACM, New York (1994)

    Chapter  Google Scholar 

  8. Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Form. Methods Syst. Des. 18(2), 141–162 (2001)

    Article  Google Scholar 

  9. Berkeley Logic Synthesis and Verification Group: ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/~alanmi/abc/

  10. Bhadra, J., Martin, A., Abraham, J., Abadir, M.: A language formalism for verification of PowerPC custom memories using compositions of abstract specifications. In: High-Level Design Validation and Test Workshop, pp. 134–141. IEEE, Piscataway (2001)

    Chapter  Google Scholar 

  11. Bhadra, J., Martin, A.K., Abraham, J.A., Abadir, M.S.: Using abstract specifications to verify PowerPC custom memories by symbolic trajectory evaluation. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 1690, pp. 386–402. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Bird, R.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice Hall, New York (1998)

    Google Scholar 

  13. Bryant, R.E.: Formal verification of memory circuits by switch-level simulation. Trans. Comput.-Aided Des. Integr. Circuits Syst. 10(1), 94–102 (1991)

    Article  Google Scholar 

  14. Bryant, R.E.: A methodology for hardware verification based on logic simulation. J. ACM 38(2), 299–328 (1991)

    Article  MathSciNet  Google Scholar 

  15. Bryant, R.E., Beatty, D., Brace, K., Cho, K., Sheffler, T.: COSMOS: a compiled simulator for MOS circuits. In: Design Automation Conf. (DAC), pp. 9–16. ACM, New York (1987)

    Google Scholar 

  16. Bryant, R.E., Beatty, D.E., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: Design Automation Conf. (DAC), pp. 297–402. IEEE, Piscataway (1991)

    Google Scholar 

  17. Camilleri, A., Gordon, M., Melham, T.: Hardware verification using higher-order logic. In: Borrione, D. (ed.) From HDL Descriptions to Guaranteed Correct Circuit Designs, pp. 43–67. North-Holland, Amsterdam (1987)

    Google Scholar 

  18. Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Ramakrishnan, R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 233–248. Springer, Heidelberg (2008)

    Google Scholar 

  19. Chou, C.T.: The mathematical foundation of symbolic trajectory evaluation. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 196–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  20. Claessen, K., Roorda, J.W.: An introduction to symbolic trajectory evaluation. In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM). LNCS, vol. 3965, pp. 56–77. Springer, Heidelberg (2006)

    Google Scholar 

  21. Claessen, K., Roorda, J.W.: A faithful semantics for generalised symbolic trajectory evaluation. Log. Methods Comput. Sci. 5(2), 1–32 (2009)

    Article  MathSciNet  Google Scholar 

  22. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Symp. on Principles of Programming Languages (POPL), pp. 343–354. ACM, New York (1992)

    Google Scholar 

  23. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  24. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  25. Een, N.: ABC/ZZ. https://bitbucket.org/niklaseen/abc-zz

  26. Flaisher, A., Gluska, A., Singerman, E.: Case study: integrating FV and DV in the verification of the Intel Core 2 Duo microprocessor. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 192–195. IEEE, Piscataway (2007)

    Chapter  Google Scholar 

  27. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  28. Grumberg, O.: Abstraction and refinement in model checking. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects. LNCS, vol. 4111, pp. 219–242. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  29. Halmos, P.R.: Naive Set Theory. Springer, Heidelberg (1987)

    MATH  Google Scholar 

  30. Hazelhurst, S.: Compositional model checking of partially ordered state spaces. Technical report 96-02, Department of Computer Science, University of British, Columbia (1996)

    Google Scholar 

  31. Hazelhurst, S., Seger, C.J.H.: A simple theorem prover based on symbolic trajectory evaluation and BDDs. Trans. Comput.-Aided Des. Integr. Circuits Syst. 14(4), 413–422 (1995)

    Article  Google Scholar 

  32. Hazelhurst, S., Seger, C.J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification, pp. 3–78. Springer, Heidelberg (1997). Chap. 1

    Chapter  Google Scholar 

  33. Hellerman, L.: A catalog of three-variable or-invert and and-invert logical circuits. Trans. Electron. Comput. EC-12(3), 198–223 (1963)

    Article  Google Scholar 

  34. Hunt, W.A. Jr., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at Centaur Technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65–88. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  35. Jain, A.: Formal hardware verification by symbolic trajectory evaluation. Ph.D. thesis, Carnegie Mellon University (1997)

    Google Scholar 

  36. Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. Trans. Comput.-Aided Des. Integr. Circuits Syst. 13(11), 1005–1015 (1994)

    Article  Google Scholar 

  37. Jones, R.B.: Applications of symbolic simulation to the formal verification of microprocessors. Ph.D. thesis, Department of Electrical Engineering, Stanford University (1999)

    Google Scholar 

  38. Jones, R.B., O’Leary, J.W., Seger, C.J.H., Aagaard, M.D., Melham, T.F.: Practical formal verification in microprocessor design. IEEE Des. Test Comput. 18(4), 16–25 (2001)

    Article  Google Scholar 

  39. Joyce, J., Seger, C.J.: Linking BDD-based symbolic evaluation to interactive theorem-proving. In: Design Automation Conf. (DAC), pp. 469–474. IEEE, Piscataway (1993)

    Google Scholar 

  40. Kaivola, R.: Formal verification of Pentium® 4 components with symbolic simulation and inductive invariants. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 170–184. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  41. Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodova, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing testing with formal verification in Intel Core i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, pp. 414–429. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  42. Kaivola, R., Kohatsu, K.R.: Proof engineering in the large: formal verification of Pentium 4 floating-point divider. Int. J. Softw. Tools Technol. Transf. 4(3), 323–334 (2003)

    Article  Google Scholar 

  43. Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common Lisp. Trans. Softw. Eng. 23(4), 203–213 (1997)

    Article  Google Scholar 

  44. Khasidashvili, Z., Gavrielov, G., Melham, T.: Assume-guarantee validation for STE properties within an SVA environment. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 108–115. IEEE, Piscataway (2009)

    Google Scholar 

  45. Krishnamurthy, N., Martin, A.K., Abadir, M.S., Abraham, J.A.: Validating PowerPC custom memories. IEEE Des. Test Comput. 17(4), 61–76 (2000)

    Article  Google Scholar 

  46. Melham, T.: Higher Order Logic and Hardware Verification. Cambridge University Press, Cambridge (1993)

    Book  Google Scholar 

  47. Melham, T.F., Jones, R.B.: Abstraction by symbolic indexing transformations. In: Aagaard, M.D., O’Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 2517, pp. 1–18. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  48. Nelson, K.L., Jain, A., Bryant, R.E.: Formal verification of a superscalar execution unit. In: Design Automation Conf. (DAC), pp. 161–166. ACM, New York (1997)

    Google Scholar 

  49. Ng, K., Hu, A.J., Yang, J.: Generating monitor circuits for simulation-friendly GSTE assertion graphs. In: Grochowski, E., Dillinger, T. (eds.) Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD), pp. 409–416. IEEE, Piscataway (2004)

    Google Scholar 

  50. Nguyen, M.D., Thalmaier, M., Wedler, M., Bormann, J., Stoffel, D., Kunz, W.: Unbounded protocol compliance verification using interval property checking with invariants. Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(11), 2068–2082 (2008)

    Article  Google Scholar 

  51. O’Leary, J., Kaivola, R., Melham, T.: Relational STE and theorem proving for formal verification of industrial circuit designs. In: Jobstmann, B., Ray, S. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 97–104. IEEE, Piscataway (2013)

    Google Scholar 

  52. Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: Design Automation Conf. (DAC), pp. 167–172. ACM, New York (1997)

    Google Scholar 

  53. Roorda, J.W.: Semantics, decision procedures, and abstraction refinement for symbolic trajectory evaluation. Ph.D. thesis, Chalmers University of Technology and Göteborg Universty (2006)

    Google Scholar 

  54. Roorda, J.W., Claessen, K.: Explaining symbolic trajectory evaluation by giving it a faithful semantics. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) International Computer Science Symposium in Russia (CSR). LNCS, vol. 3967, pp. 555–566. Springer, Heidelberg (2006)

    Google Scholar 

  55. Roorda, J.W., Claessen, K.: SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Intl. Conf. on Computer-Aided Verification (CAV), pp. 175–189. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  56. Ryan, M., Sadler, M.: Valuation systems and consequent relations. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 1, pp. 1–78. Oxford University Press, Oxford (1992). Chap. 1

    Google Scholar 

  57. Santarini, M.: Synopsys extends formal reach with InnoLogic acquisition. EE Times (2003). www.eetimes.com/document.asp?doc_id=1216962

  58. Schubert, T.: High level formal verification of next-generation microprocessors. In: Design Automation Conf. (DAC), pp. 1–6. ACM, New York (2003)

    Google Scholar 

  59. Sebastiani, R., Singerman, E., Tonetta, S., Vardi, M.Y.: GSTE is partitioned model checking. Form. Methods Syst. Des. 31(2), 177–196 (2007)

    Article  Google Scholar 

  60. Sebastiani, R., Tonetta, S., Vardi, M.: Property-driven partitioning for abstraction refinement. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 389–404. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  61. Seger, C.J., Joyce, J.: A mathematically precise two-level formal hardware verification methodology. Report 92-34, Department of Computer Science, University of British, Columbia (1992)

    Google Scholar 

  62. Seger, C.J.H.: Voss—a formal hardware verification system: user’s guide. Tech. Rep. TR-93-45, University of British Columbia, Department of Computer Science (1993)

    Google Scholar 

  63. Seger, C.J.H.: Personal communication (2014)

    Google Scholar 

  64. Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147–189 (1995)

    Article  Google Scholar 

  65. Seger, C.J.H., Jones, R.B., O’Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. Trans. Comput.-Aided Des. Integr. Circuits Syst. 24(9), 1381–1405 (2005)

    Article  Google Scholar 

  66. Slobodová, A., Davis, J., Swords, S., Hunt, W.: A flexible formal verification framework for industrial scale validation. In: International Conference on Formal Methods and Models for Codesign, pp. 89–97. IEEE, Piscataway (2011)

    Google Scholar 

  67. Smith, E.: A logic for GSTE. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 119–126. IEEE, Piscataway (2007)

    Chapter  Google Scholar 

  68. Smith, E.: Specifying properties for generalized symbolic trajectory evaluation. Ph.D. thesis, University of Oxford (2008)

    Google Scholar 

  69. Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 190–204. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  70. Velev, M.N., Bryant, R.E.: Efficient modeling of memory arrays in symbolic ternary simulation. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1384, pp. 136–150. Springer, Heidelberg (1998)

    Google Scholar 

  71. Wang, L.C., Abadir, M.S., Krishnamurthy, N.: Automatic generation of assertions for formal verification of PowerPC microprocessor arrays using symbolic trajectory evaluation. In: Design Automation Conf. (DAC), pp. 534–537. IEEE, Piscataway (1998)

    Google Scholar 

  72. Yang, J., Ghughal, R., Tiemeyer, A.: Industrial scale formal verification using concurrent GSTE. In: Tang, T.A., Huang, Y. (eds.) International Conference on ASIC (ASICON), pp. 930–933. IEEE, Piscataway (2005)

    Google Scholar 

  73. Yang, J., Goel, A.: GSTE through a case study. In: Pileggi, L., Kuelmann, A. (eds.) International Conference on Computer Aided Design (ICCAD), pp. 534–541. ACM, New York (2002)

    Google Scholar 

  74. Yang, J., Seger, C.H.: Generalized symbolic trajectory evaluation—abstraction in action. In: Aagaard, M.D., O’Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 2517, pp. 70–87. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  75. Yang, J., Seger, C.J.: Compositional specification and model checking in GSTE. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 216–228. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  76. Yang, J., Seger, C.J.H.: Generalized symbolic trajectory evaluation. Tech. rep., Intel Strategic CAD Labs (2000)

    Google Scholar 

  77. Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. Trans. Very Large Scale Integr. (VLSI) Syst. 11(3), 345–353 (2003)

    Article  Google Scholar 

  78. Zhong, J.X.: Circuit simulation using encoding of repetitive subcircuits (2001). US Patent Number 6,865,525

    Google Scholar 

  79. Zhu, Z., Seger, C.J.: The completeness of a hardware inference system. In: Dill, D.L. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 818, pp. 286–298. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    Tom Melham

Authors
  1. Tom Melham
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tom Melham .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Melham, T. (2018). Symbolic Trajectory Evaluation. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation