Current verification algorithms require a net list and a timed state
graph to verify hazard freedom for gate-level circuits. Assuming that
primary inputs as given are hazard-free, each node in the netlist must
be examined for hazard freedom. Current approaches suffer from state
explosion problems because each node is treated as a new state
variable, potentially doubling the number of states. These approaches
also fail to utilize explicit timing values to ensure correctness
which can potentially reduce computation time significantly. Our
approach takes the same inputs and creates a color vector at each
state, with each indices of the color vector corresponding to a node
in the netlist. Initial colors for each state are evaluated by
applying the given state vector to the network and determining the
boolean evaluations at each node. An attempt is then made to try to
stabilize each edge in the state graph to a high or low value in two
ways. First, a time independent method attempts to show that a primary
output switching can only occurred if the edge under consideration was
at a known value. Secondly, timing is used to try and show that
elapsed time in traversing the state graph is greater than the delay
of the network up to the node of interest. If either case is true, the
edge must have stabilized to a known logic value. The resultant
stabilized edges are than propagated throughout the state graph. The
resulting color vectors are checked for consistency and any node
showing a consistent coloring is considered hazard-free. Experimental
results match those from established software tools with a x-fold
decrease in computation time. This decrease in computation time is
achieved by avoiding the state-space explosion problem, simply by
examining the explicit behavior of internal nodes.