In [19], we are concerned with approximation algorithms
for timing analysis of combinational circuits.
As a result of intensive research in the early 90's,
efficient tools exist
which can analyze circuits of thousands of gates
in a few minutes or even in seconds for many cases. However,
the computation time of these tools is unpredictable
since the internal engine of analysis is either a SAT solver
or a modified ATPG algorithm,
both of which are just heuristic algorithms to an NP-complete problem.
Although they are highly tuned for CAD applications,
there exists a class of problem instances
which exhibits the worst-case exponential CPU time behavior.
In the context of timing analysis,
circuits with a large amount of reconvergence,
e.g. C6288 of the ISCAS benchmark suite,
are known to be difficult to analyze
under sophisticated delay models
even with state-of-the-art techniques without path enumeration.
For example, all algorithms can not complete
the analysis under the mapped delay model.
To make timing analysis of such corner case circuits
feasible we proposed in [19]
an approximate computation scheme to the timing analysis problem
as an extension to the exact analysis method
proposed by McGeer. Sensitization conditions are conservatively
approximated in a selective fashion so that
the size of SAT problems solved during analysis is controlled.
Initial experimental results show that
the approximation technique is effective
in reducing the total analysis time without losing accuracy
in cases where the exact approach takes too much time
or cannot complete.
GENERAL VERIFICATION METHODS: