Bounded Delay Timing Analysis Using Boolean Satisfiability

This paper proposes an accurate technique for computing critical delay of a circuit under a bounded delay model. The bounded delay model is better adapted to capture real time variations in the gate delays due to changes in operating conditions. But this flexibility comes at a price, since the uncertainty in gate delays increases the complexity of the timing analysis problem greatly. But we have shown in this paper that using fixed delay timing analysis with worst case delay values for gates can potentially underestimate the critical delay of a circuit. We propose a SAT based methodology for timing analysis in a bounded delay framework which utilises the phenomenal speed and efficiency of modern SAT solvers, and report encouraging results on the ISCAS benchmark circuits