| Verifying the timing properties of VLSI circuits is NP-Hard due to the false path problem, and considering just the topological delay of the circuit is too conservative and may result in unnecessary redesign efforts. We present in this thesis a timing verification method based on Waveform Narrowing . The method has linear space complexity, and has controllable time complexity that can be virtually linear, n × log (n), quadratic, or exponential, depending on the required level of accuracy. The method consists of modeling the circuit, the timing constraints, and the operating conditions as a constraint system that is consistent if and only if the timing constraints are violated. The constraint system is composed of a finite set of variables that take values from their respective domains, and a set of relational constraint operators, each operating on a subset of the variables. The system is solved partially by repeatedly applying the constraints, removing from the domains values that are not part of any solution, until the greatest fixpoint is reached. If we end up with empty domains, we conclude that the timing constraints are satisfied; otherwise, no conclusion can be drawn.; The method results in false negative answers when we end up with non-empty domains, and yet the constraint system has no solution. To reduce this pessimism we developed two polynomial techniques:; The Timing dominators concept that determines key circuit nets for which the domains can be narrowed as a consequence of necessary conditions deduced from the global circuit function; Spatial correlation procedure that enforces partially the global circuit function by restricting the domains of selected reconvergent fan-outs to waveforms stabilizing at 0 and 1, and then merging the results.; Also, we developed a case analysis procedure able to find a test vector or to prove that no violation is possible.; When tested on ISCAS'85 benchmarks, the method found tight upper bounds that correspond to exact circuit delays for all circuits. Moreover, except for c6288, the case analysis procedure found test vectors for all circuits with a remarkably low number of backtracks!; We extended the method by implementing capabilities necessary to verify industrial designs. The resulting timing verifier was tested successfully on a 122K-gate industrial circuit, and proved that its relative safe margin is 17.459% of the clock cycle instead of 8.74% reported by topological analysis. |
