Timing analysis using propositional satisfiability

The existence of false paths represents a significant and computationally complex problem in the timing analysis of combinational and sequential circuits. In this paper we describe propositional satisfiability based algorithms for timing analysis, which introduce significant perfomance improvements over existing procedures. In particular we address the problems of circuit delay computation and path delay validation, describing algorithms and providing experimental results for both problems