Speeding Up Functional Timing Analysis by Concise Formulation of Timed Characteristic Functions

Functional timing analysis (FTA) is a renowned method of finding the true critical delay for the design under interest. By constructing conjunctive normal form (CNF) clauses based on temporal and function constraints, false paths can be identified through the satisfiability (SAT) solving. As a result, the critical delay estimated by FTA is more accurate than that by conventional static timing analysis (STA). However, FTA suffers from the extremely long formulation and computation time, as the number of the clauses in CNF grows exponentially with the increasing size of the design. Due to the reconvergent effect, thousands of clauses can be redundantly formulated for one pin. Even worse, most of them are found useless but seriously lengthen the computation time. Therefore, to avoid ineffective computation in FTA, three novel techniques are proposed: 1) encoding duplication removal (EDR) for removing duplicated functional literals; 2) redundant state propagation (RSP) for propagating temporal states to identify redundant clauses; and 3) temporal footprint identification (TFI) for combining clauses that represent constraints with the same behavior. The experiments show that under a given timing constraint, 94% clauses and 95% literals can be pruned averagely (99% clauses and 99% literals under the best case), resulting in $15.3 \times $ speedup ($72.99 \times $ under the best case) for formulation and SAT solving. As a result, the proposed techniques (EDR, RSP, and TFI) are proven effective to reduce useless computation and improve the overall performance of FTA.