Advertisement

Symbolic analysis and verification of CPA descriptions

  • M. C. McFarland
  • T. J. Kowalski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

CPA is a formalism for specifying the behavior of digital systems. It describes the input/output behavior, independent of the internal structure and operation of the system. The primary use for CPA is formal verification of digital designs, in which the behavior of a design is checked for consistency against the CPA specification. This paper describes audit, a system we are developing that formally verifies a digital design against a CPA specification. The design is represented as a state machine with multi-bit data registers that can be tested and changed on the state transitions. Whereas many verification programs that work at this level expand the data part of the machine into individual states, audit treats the registers as symbolic entities and uses symbolic simulation and first-order predicate calculus to reason about their effect on the behavior of the machine. Yet unlike other symbolic simulation programs, audit can automatically analyze the behavior of simple loops and can reason about sequences of inputs and outputs.

Keywords

Clock Cycle Finite State Machine Input Port Formal Verification Path State 
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]
    Bochmann, G. V., “Hardware Specification with Temporal Logic: An Example,” IEEE Transactions on Computers C-31(3), pp. 223–231 (March, 1982).Google Scholar
  2. [2]
    Browne, M. C., Clarke, E. M., Dill, D. L., and Mishra, B., “Automatic Verification of Sequential Circuits Using Temporal Logic,” IEEE Transactions on Computers C-35(12), pp. 1035–1044 (December, 1986).Google Scholar
  3. [3]
    Darringer, J., “The application of program verification techniques to hardware verification,” Proceedings of the Sixteenth Design Automation Conference, pp. 375–381, ACM SIGDA and IEEE Computer Society DATC (June, 1979).Google Scholar
  4. [4]
    Crocker, S., “State deltas: A formalism for representing segments of computation,” UCLA-ENG-7784, Computer Science Department, University of California at Los Angeles (February, 1978).Google Scholar
  5. [5]
    Hunt, W. A., FM8501: A Verified Microprocessor, PhD Thesis, University of Texas at Austin (February, 1986).Google Scholar
  6. [6]
    Devadas, S., Ma, H. T., and Newton, A. R., “On The Verification of Sequential Machines At Different Levels of Abstraction,” Proceedings of the 24th Design Automation Conference, pp. 271–276, ACM/IEEE (June, 1987).Google Scholar
  7. [7]
    Kurshan, R. P. and McMillan, K. L., “Analysis of Digital Circuits Through Symbolic Reduction,” IEEE Transactions on Computer-Aided Design 10(11), pp. 1356–1371 (November, 1991).Google Scholar
  8. [8]
    Berthet, C., Coudert, O., and Madre, J., “New Ideas on Symbolic Manipulations of Finite State Machines,” International Conference on Computer Design, IEEE (September, 1990).Google Scholar
  9. [9]
    Bryant, R., “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers C-35(8), pp. 677–691 (August, 1986).Google Scholar
  10. [10]
    Burch, J. R., Clarke, E. M., and Long, D. E., “Representing Circuits More Efficiently in Symbolic Model Checking,” Proceedings of the 28th Design Automation Conference, pp. 403–407, ACM/IEEE (June, 1991).Google Scholar
  11. [11]
    Gordon, M., “Why higher-order logic is a good formalism for specifying and verifying hardware,” in Formal Aspects of VLSI Design, Milne, G. and Subrahmanyam, P. A. (Eds.), North Holland, New York (1986).Google Scholar
  12. [12]
    Wegbreit, B., “The synthesis of loop predicates,” Communications of the ACM 17(2), pp. 102–112 (February, 1974).Google Scholar
  13. [13]
    Devadas, S., Keutzer, K., and Krishnakumar, A. S., “Design Verification and Reachability Analysis Using Algebraic Manipulation,” Proceedings of the International Conference on Computer Design, pp. 250–258, IEEE (October, 1991).Google Scholar
  14. [14]
    Lee, D. and Yannakakis, M., “Online Minimization of Transition Systems,” Proceedings of the 24th Annual ACM Symposium on the Theory of Computing, pp. 264–274, ACM (May, 1992).Google Scholar
  15. [15]
    Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, J., “Symbolic Model Checking 10∧20 States and Beyond,” Proceedings of the Fifth Annual Symposium on Logic in Computer Science (June, 1990).Google Scholar
  16. [16]
    McFarland, M. C. and Kowalski, T. J., “Specifying System Behavior in CPA,” ICCD91, pp. 342–345, IEEE (October, 1991).Google Scholar
  17. [17]
    Chu, T., Synthesis of Self-timed VLSI Circuits from Graph-Theoretic Specifications, PhD Thesis, Department of Electrical Engineering and Computer Science, MIT (May, 1987).Google Scholar
  18. [18]
    McFarland, M. C., “CPA: Giving an Account of Timed System Behavior,” ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU'90), ACM, Vancouver, BC (August, 1990).Google Scholar
  19. [19]
    McFarland, M. C., Kowalski, T. J., and Peman, M. J., “Language and Formal Semantics of the Specification System CPA,” Proceedings of the International Workshop on Hardware-Software Co-design, IEEE, Estest Park, CO (September 30, 1992).Google Scholar
  20. [20]
    King, J. C., “Proving programs to be correct,” IEEE Transactions on Computers C-20(11), pp. 1331–1336 (November, 1971).Google Scholar
  21. [21]
    Sarkar, D. and De Sarkar, S. C., “Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers,” IEEE Transactions on Software Engineering 15(1), pp. 1–8 (January, 1989).Google Scholar
  22. [22]
    Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications, McGraw-Hill, New York (1991).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • M. C. McFarland
    • 1
  • T. J. Kowalski
    • 2
  1. 1.Boston CollegeChestnut Hill
  2. 2.AT&T Bell LaboratoriesMurray Hill

Personalised recommendations