Skip to main content
SpringerLink
Log in

Formal verification by symbolic evaluation of partially-ordered trajectories

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Symbolic trajectory evaluation provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. The desired system properties are expressed in a notation combining Boolean expressions and the temporal logic “next-time” operator. In its simplest form, each property is expressed as an assertion [A⇒C], where the antecedentA expresses some assumed conditions on the system state over a bounded time period, and the consequentC expresses conditions that should result. A generalization allows simple invariants to be established and proven automatically.

The verifier operates on system models in which the state space is ordered by “information content”. By suitable restrictions to the specification notation, we guarantee that for every trajectory formula, there is a unique weakest state trajectory that satisfies it. Therefore, we can verify an assertion [A⇒C] by simulating the system over the weakest trajectory forA and testing adherence toC. Also, establishing invariants correspond to simple fixed point calculations.

This paper presents the general theory underlying symbolic trajectory evaluation. It also illustrates the application of the theory to the taks of verifying switch-level circuits as well as more abstract implementations.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. D. L. Beatty, R. E. Bryant, and C.-J. H. Seger, “Synchronous Circuit Verification by Symbolic Simulation: An Illustration,”Sixth MIT Conference on Advanced Research in VLSI, pp. 98–112, 1990.

  2. D. L. Beatty, “A Methodology for Formal Hardware Verification, with Application to Microprocessors,” Technical Report CMU-CS-;93-190, Carnegie Mellon University, 1993.

  3. D. L. Beatty and R. E. Bryant, “Formally Verifying a Microprocessor using a Simulation Methodology,”31st Design Automation Conference, pp. 596–602, June, 1994.

  4. S. Bose and A. L. Fisher, “Verifying Pipelined Hardware Using Symbolic Logic Simulation,”International Conference on Computer Design, pp. 217–221, 1989.

  5. S. Bose and A. L. Fisher, “Automatic Verification of Synchronous Circuits using Symbolic Logic Simulation and Temporal Logic,“IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pp. 759–764, 1989.

  6. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,”IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677–691.

    Google Scholar 

  7. R. E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler, “COSMOS: a Compiled Simulator for MOS Circuits,”24th Design Automation Conference, 9–16, 1987.

  8. R. E. Bryant, “Boolean Analysis of MOS Circuits,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. CAD-6, No. 4 (July, 1987), 634–649.

    Google Scholar 

  9. R. E. Bryant, and C.-J. H. Seger, “Formal Verification of Digital Circuits Uisng Symbolic Ternary System Models,”Computer-Aided Verification '90, E. M. Clarke, and R. P. Kurshan,eds. American Mathematical Society, pp. 121–146, 1991.

  10. R. E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,”IEEE Transactions on Computers, Vol. 40, No. 2 (February, 1991), pp. 205–213.

    Google Scholar 

  11. R. E. Bryant, “Formal Verification of Memory Circuits by Switch-Level Simulation,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 10, No. 1 (January, 1991), pp. 94–102.

    Google Scholar 

  12. R. E. Bryant, “A Methodology for Hardware Verification Based on Logic Simulation,”J. ACM, Vol. 38, No. 2 (April, 1991), pp. 299–328.

    Google Scholar 

  13. R. E. Bryant, D. E. Beatty, and C.-J. H. Seger, “Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation,”ACM/IEEE 28th Design Automation Conference, June, pp. 297–402, 1991.

    Google Scholar 

  14. J. A. Brzozowski and M. Yoeli, “On a Ternary Model of Gate Networks,”IEEE Transactions on Computers, C-28, No. 3 (March 1979), pp. 178–183, 1979.

    Google Scholar 

  15. J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,”27th Design Automation Conference, pp. 46–51, 1990.

  16. E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,”ACM Transactions on Programming Languages, Vol. 8, No. 2 (April, 1986), pp. 244–263.

    Google Scholar 

  17. E. M. Clarke, O. Grumberg, and D. E. Long, “Model Checking and Abstraction,”Proc. 19th Annual ACM Symposium on Principles of Programming Languages, Jan., 1992.

  18. O. Coudert, C. Berthet, and J. C. Madre, “Verification of Sequential Machines using Boolean Functional Vectors,”IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pp. 111–128, 1989.

  19. O. Coudert, J.-C. Madre, and C. Berthet, “Verifying temporal properties of sequential machines without building their state diagrams,”Computer-Aided Verification 90, E. M. Clarke and R. P. Kurshan,eds. American Mathematical Society, pp. 75–84.

  20. J. A. Darringer, “The Application of Program Verification Techniques to Hardware Verification,”16th Design Automation Conference, pp. 375–381, 1979.

  21. S. Devadas, H.-K. T. Ma, and A. R. Newton, “On the Verification of Sequential Machines at Differing levels of Abstraction,”24th Design Automation Conference, pp. 271–276, 1987.

  22. T. Kam and P. A. Subramanyam, “Comparing Layouts with HDL Models: A Formal Verification Technique,”International Conference on Computer Design, IEEE, 1992, pp. 588–591.

  23. M. Gordon, R. Milner, and C. Wadsworth, “Edinburgh LCF,”Lecture Notes in Computer Science, No. 78, Springer Verlag, 1979.

  24. M. Gordon, “Why higher-order logic is a good formalism for specifying and verifying hardware,”Formal Aspects of VLSI Design, G. Milne and P. A. Subrahmanyam,eds., North-Holland, pp. 153–177, 1986.

  25. N. Halbwachs, F. Lagnier, and C. Ratel, “Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE,”IEEE Transactions on Software Engineering, Vol. 18, No. 9 (September, 1992), pp. 785–793.

    Google Scholar 

  26. J. Joyce, “Generic Structures in the Formal Specification and Verification of Digital Circuits,”The Fusion of Hardware Design and Verification, G. Milne,ed., North Holland, pp. 50–74, 1988.

  27. J. Joyce and C. Seger, “Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving,”30th Design Automation Conference, pp. 469–474, 1993.

  28. J. S. Jephson, R. P. McQuarrie, and R. E. Vogelsberg, “A Three-Level Design Verification System,”IBM Systems Journal, Vol. 8, No. 3, pp. 178–188, 1969.

    Google Scholar 

  29. R. P. Kurshan and K. L. McMillan, “Analysis of Digital Circuits Through Symbolic Reduction,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 10, No. 11 (November, 1991), pp. 1356–1371.

    Google Scholar 

  30. C. A. Mead and L. Conway,Introduction to VLSI Systems, Addison-Wesley, 1980.

  31. R. Milner, “A Proposal for Standard ML,”Proceedings of ACM Conference on LISP and Functional Programming, Austin, TX, pp. 184–197, 1984.

  32. A. Pnueli, “The Temporal Logic of Programs,”18th Symposium on the Foundations of Computer Science, IEEE, pp. 46–56, 1977.

  33. D. S. Reeves and M. J. Irwin, “Fast Methods for Switch-Level Verification of MOS Circuits,”IEEE Transactions on CAD/IC, Vol. CAD-6, No. 5 (Sept., 1987), pp. 766–779.

    Google Scholar 

  34. C-J. Seger and R. E. Bryant, “Modeling of Circuit Delays in Symbolic Simulation,”IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pp. 625–639, 1989.

  35. C. Seger and J. Joyce, “A Mathematically Precise Two-Level Formal Hardware Verification Methodology,” Technical Report 92-34, Department of Computer Science, University of British Columbia, December 1992.

  36. C. Seger, “Voss—A formal hardware verification system: User's guide”, Technical Report 93-45, Department of Computer Science, University of British Columbia, December 1993.

  37. J. Stoy,Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.

  38. P. Wolper, “Expessing Interesting Properties of Programs in Propositional Temporal Logic,”Proc. 13th Annual ACM Symposium on Principles of Programming Languages, Jan., 1986, pp. 184–193.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of British Columbia, V6T 1Z4, Vancouver, B.C., Canada

    Carl-Johan H. Seger

  2. School of Computer Science, Carnegie Mellon University, PA, Pittsburgh, 15213, USA

    Randal E. Bryant

Authors
  1. Carl-Johan H. Seger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Randal E. Bryant
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This research was supported by the Defense Advanced Research Projects Agency, ARPA Order Number 4976, by the National Science Foundation, under grant number MIP-8913667, by operating grant OGPO 109688 from the Natural Sciences and Engineering Research Council of Canada, and by a fellowship from the British Columbia Advanced Systems Institute.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Seger, CJ.H., Bryant, R.E. Formal verification by symbolic evaluation of partially-ordered trajectories. Form Method Syst Des 6, 147–189 (1995). https://doi.org/10.1007/BF01383966

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01383966

Keywords

Search

Navigation