Sequential circuit verification using symbolic model checking

ABSTRACT

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of sequential circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 1020 states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to handle a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.

REFERENCES

• 1: S. Bose and A. Fisher. Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic. In IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, 1989.
• 2: S. Bose and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In IEEE International Conference on Computer Design, 1989.
• 3: M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
• 4: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 5: Randal E. Bryant, Verifying a static RAM design by logic simulation, Proceedings of the fifth MIT conference on Advanced research in VLSI, p.335-349, January 1988, Cambridge, Massachusetts, United States
• 6: J. R. Burch, E. M. Clarke, K. L. M cMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. Technical report, Carnegie Mellon University, School of Computer Science, 1990. In Preparation.
• 7: 3. R. Butch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. ttwang. Symbolic model checking: 102~ states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990. To Appear.
• 8: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 9: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 10: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• 11: D. L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, Proceedings of the fifth MIT conference on Advanced research in VLSI, p.51-65, January 1988, Cambridge, Massachusetts, United States
• 12: M. Fujita and It. Fujizawa. Specification, verification, and synthesis on control circuits with propositional temporal logic. In Ninth International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, June 1989.
• 13: A. J. Martin. A synthesis method for self-timed VLSI circuits. In Proceedings of the IEEE International Con- }erence on Computer Design, 1987.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Verification