Advertisement

Symbolic Trajectory Evaluation

  • Tom Melham
Chapter

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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) CrossRefGoogle Scholar
  5. 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) CrossRefGoogle Scholar
  6. 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) CrossRefGoogle Scholar
  7. 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) CrossRefGoogle Scholar
  8. 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) CrossRefGoogle Scholar
  9. 9.
    Berkeley Logic Synthesis and Verification Group: ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/~alanmi/abc/
  10. 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) CrossRefGoogle Scholar
  11. 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) CrossRefGoogle Scholar
  12. 12.
    Bird, R.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice Hall, New York (1998) Google Scholar
  13. 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) CrossRefGoogle Scholar
  14. 14.
    Bryant, R.E.: A methodology for hardware verification based on logic simulation. J. ACM 38(2), 299–328 (1991) MathSciNetCrossRefGoogle Scholar
  15. 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. 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. 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. 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. 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) CrossRefGoogle Scholar
  20. 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. 21.
    Claessen, K., Roorda, J.W.: A faithful semantics for generalised symbolic trajectory evaluation. Log. Methods Comput. Sci. 5(2), 1–32 (2009) MathSciNetCrossRefGoogle Scholar
  22. 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. 23.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) Google Scholar
  24. 24.
    Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990) zbMATHGoogle Scholar
  25. 25.
  26. 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) CrossRefGoogle Scholar
  27. 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) zbMATHGoogle Scholar
  28. 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) CrossRefGoogle Scholar
  29. 29.
    Halmos, P.R.: Naive Set Theory. Springer, Heidelberg (1987) zbMATHGoogle Scholar
  30. 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. 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) CrossRefGoogle Scholar
  32. 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 CrossRefGoogle Scholar
  33. 33.
    Hellerman, L.: A catalog of three-variable or-invert and and-invert logical circuits. Trans. Electron. Comput. EC-12(3), 198–223 (1963) CrossRefGoogle Scholar
  34. 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) CrossRefGoogle Scholar
  35. 35.
    Jain, A.: Formal hardware verification by symbolic trajectory evaluation. Ph.D. thesis, Carnegie Mellon University (1997) Google Scholar
  36. 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) CrossRefGoogle Scholar
  37. 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. 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) CrossRefGoogle Scholar
  39. 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. 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) CrossRefGoogle Scholar
  41. 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) CrossRefGoogle Scholar
  42. 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) CrossRefGoogle Scholar
  43. 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) CrossRefGoogle Scholar
  44. 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. 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) CrossRefGoogle Scholar
  46. 46.
    Melham, T.: Higher Order Logic and Hardware Verification. Cambridge University Press, Cambridge (1993) CrossRefGoogle Scholar
  47. 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) CrossRefGoogle Scholar
  48. 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. 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. 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) CrossRefGoogle Scholar
  51. 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. 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. 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. 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. 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) CrossRefGoogle Scholar
  56. 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. 57.
    Santarini, M.: Synopsys extends formal reach with InnoLogic acquisition. EE Times (2003). www.eetimes.com/document.asp?doc_id=1216962
  58. 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. 59.
    Sebastiani, R., Singerman, E., Tonetta, S., Vardi, M.Y.: GSTE is partitioned model checking. Form. Methods Syst. Des. 31(2), 177–196 (2007) CrossRefGoogle Scholar
  60. 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) zbMATHGoogle Scholar
  61. 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. 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. 63.
    Seger, C.J.H.: Personal communication (2014) Google Scholar
  64. 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) CrossRefGoogle Scholar
  65. 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) CrossRefGoogle Scholar
  66. 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. 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) CrossRefGoogle Scholar
  68. 68.
    Smith, E.: Specifying properties for generalized symbolic trajectory evaluation. Ph.D. thesis, University of Oxford (2008) Google Scholar
  69. 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) CrossRefGoogle Scholar
  70. 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. 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. 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. 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. 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) CrossRefGoogle Scholar
  75. 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) CrossRefGoogle Scholar
  76. 76.
    Yang, J., Seger, C.J.H.: Generalized symbolic trajectory evaluation. Tech. rep., Intel Strategic CAD Labs (2000) Google Scholar
  77. 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) CrossRefGoogle Scholar
  78. 78.
    Zhong, J.X.: Circuit simulation using encoding of repetitive subcircuits (2001). US Patent Number 6,865,525 Google Scholar
  79. 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) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.University of OxfordOxfordUK

Personalised recommendations