An apparatus and method for automated use of phase abstraction for enhanced
verification of circuit designs is provided. With the apparatus and
method, latches are "colored," i.e. classified into different types, based
on information obtained from a clock tree of the circuit design. Clock
tree primitives contain sufficient information to taxonomize the clocks
into their respective phases and identify which latches are gated latches.
In coloring the latches, gated latches are replaced in the circuit design
with a free running clock, a multiplexor, and a sequence of L1 to Ln
latches to provide a feedback path via the data path. This allows the
gated latch to be phase abstracted without losing the "gated"
functionality of the gated latch in the resulting trace. Once the latches
are colored in this way, phase abstraction is performed on the colored
circuit design. The phase abstracted netlist is then subjected to
verification and a trace is produced. The coloring information of the
original circuit, plus information as to the exact nature of the phase
abstraction performed, is then used to transform the phase abstracted
trace to one which resembles a trace of the circuit without phase
abstraction.
