Satisfiability models and algorithms for circuit delay computation

ABSTRACT

The existence of false paths represents a significant and computationally complex problem in the estimation of the true delay of combinational and sequential circuits. In this article we conduct a comprehensive study of modeling circuit delay computation, accounting for false paths, as a sequence of instances of Boolean satisfiability. Several path sensitization models and delay models are studied. In addition we evaluate some of the most competitive Boolean satisfiability algorithms seeking to identify which are best suited for solving circuit delay computation problems. Finally, realistic delay modeling (taking into account extracted interconnect delays and fanout data) is considered in order to experimentally evaluate the complexity of solving real-world instances.

REFERENCES

• 1: ASHAR, P., MALIK, S., AND ROTHWEILER, S. 1993. Functional timing analysis using ATPG. In Proceedings of the European Design Automation Conference.
• 2: BARTH, P. 1995. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimizations. Tech. Rep. MPI-I-95-2-003 (Jan.), Max-Planck-Institut fur Informatik.
• 3: BAYARDO, JR., R. AND SCHRAG, R. 1997. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the National Conference on Artificial Intelligence (AAAI'97 ).
• 4: BENKOSKI, J., MEERSCH, E. V., CLAESEN, L., AND DE MAN, H. 1987. Efficient algorithms for solving the false path problem in timing verification. In Proceedings of the International Conference on Computer-Aided Design (Nov.), 44-47.
• 5: BERGAMASCHI, R. 1991. The effects of false paths in high-level synthesis. In Proceedings of the International Conference on Computer Aided-Design (Nov.).
• 6: CHEN, H.-C. AND DU, D. H. C. 1991. Path sensitization in critical path problem. In Proceedings of the International Conference on Computer Aided-Design (Nov.), 208-211.
• 7: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 8: DEVADAS, S., KEUTZER, K., AND MALIK, S. 1993. Computation of floating-mode delay in combinational circuits: Practice and implementation. IEEE Trans. CAD 12, 12 (Dec.), 1924-1936.
• 9: Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
• 10: Jan F Groote , Joost P. Warners, The propositional formula checker HeerHugo, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1999
• 11: GUERRA E SILVA, L., MARQUES-SILVA, J., SILVEIRA, L. M., AND SAKALLAH, K. A. 1998a. Realistic delay modeling in satisfiability-based timing analysis. In Proceedings of the IEEE International Symposium on Circuits and Systems (Monterey, CA, May-June).
• 12: GUERRA E SILVA, L., MARQUES-SILVA, J., SILVEIRA, L. M., AND SAKALLAH, K. A. 1998b. Timing analysis using propositional satisfiability. In Proceedings of the IEEE International Conference on Electronics, Circuits and Systems (Lisboa, Portugal, Sept.).
• 13: HRAPCENKO, V. 1978. Depth and delay in a network. Soviet Math. Dokl. 19,4.
• 14: LARRABEE, T. 1992. Test pattern generation using Boolean satisfiability. In IEEE Trans. Comput. Aided Des. 11 (Jan.), 4-15.
• 15: LI, C. M. AND ANBULAGAN. 1997. Look-ahead versus look-back for satisfiability problems. In Proceedings of the International Conference on Principles and Practice of Constraint Programming.
• 16: MARQUES-SILVA, J. AND SAKALLAH, K. A. 1994. Efficient and robust test-generation based timing analysis. In Proceedings of the International Symposium on Circuits and Systems, 303-306.
• 17: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 18: Patrick Charles Mcgeer , Robert K. Brayton, On the interaction of functional and timing behaviour of combinational logic circuits, 1989
• 19: Patrick C. McGeer , Robert K. Brayton, Integrating Functional and Temporal Domains in Logic Design: The False Path Problem and Its Implications, Kluwer Academic Publishers, Norwell, MA, 1991
• 20: MCGEER, P. C., SALDANHA, A., STEPHAN, P. R., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. L. 1991. Timing analysis and delay-fault test generation using path-recursive functions. In Proceedings of the International Conference on Computer Aided-Design, 180-183.
• 21: STEPHAN, P. R., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. L. 1992. Combinational test generation using satisfiability. Tech. Rep. UCB/ERL M92/112 (Oct.), Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, Berkeley, CA.
• 22: Hakan Yalcin , John P. Hayes, Hierarchical timing analysis using conditional delays, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.371-377, November 05-09, 1995, San Jose, California, United States
• 23: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection

General Terms:
Algorithms, Verification

Keywords:
Boolean satisfiability, circuit delay computation, delay modeling, false path, timing analysis