Hazard checking algorithm version 1.5 10/15/2002

1. [Done] Color all states with R or F based on the Boolean evaluation of the node under consideration.

2. [Done] Speed Independent edge stabilization. Find the state->state transitions where the output changes and see if the path from my node of interest to the output can propagate. If so, then color the edge with a 0 or 1, depending on the Boolean evaluation. Store these stabilized edges in a linked list for propagation later.

3. [Done] Find points where the state graph has state-to-state transitions from R->F or F->R (this is where there is a change in evaluation on my node under consideration). Store these in a separate linked list. For each of these, do the following:

4. [Done] Find the edge transition at which this occurs (i.e. a+, b-, etc.). Store this in the linked list.

5. [Done] Set this as the reference point.

6. [Done] Find the maximum delay from this reference point to the node of interest in my decomposition. If more than one path, take the outside bounds.

Note: Sense ignored in decomposition i.e. if the reference transition is a+ then a timing must be calculated for any a+ or a- input found in my decomposition.

Note: A more conservative approach is to find the longest path from any input to the node of interest. [Done].

7. [Done] Find the zone associated with the state previous to the reference transition.

Note: What if more than one zone exists?

8. [Done] Make a new zone of dimension + 1.

9. [Done] Copy previous clocks data into new zone.

10. [Done] Set all new entries equal to INFINITY except the diagonal entry which should be set to 0.

11. [Done] Make new clockkey vector of dimension + 1, copy previous clockkey data, and put new transition in the new entry.

12. [Done] Modify zone with new <lower, upper> information.

Go to rules->[causal transition][new transition], get lower field and place –(lower) in upper right corner of clocks matrix. Get upper field and place in lower left corner.

Note: For concurrent systems, a more general approach is needed, which is as follows. For the new column added to the zone, go to rules->[causal transition][new transition] and if a rule exists, place the negative of the lower bound in the column entry. Do this for each row in the new column except the diagonal. For upper bounds, search backward through the clockkey until I find one upper bound that exists for the entry [new transition][causal transition] and update this one entry, then stop.

13. [Done] Canonicalize zone. Use Floyd’s all path algorithm.

14. [Done] Extract new timing information from zone.

15. [Done] Compare the minimum elapsed time in the zone with the maximum delay through my decomposition.

16. [Done] If the minimum elapsed time is equal to or greater than delay through my decomposition, color this edge with a stable color (1 if color was Rising, 0 if color was Falling). Go to step 3, else go to step 7.

17. [Done] If I reach a termination point, I cannot stabilize the edge so leave it colored as is. Go to step 7. (A termination point is when I find an edge enabled in the opposite direction of my reference transition (maybe, not implemented), I reach an edge previously stabilized, I reach an edge previously visited, or the enabling on an edge changes from R->F->R or from F->R->F.)

18. [Done] Do a soft propagation of the stable edges from the start state.

19. [Done] Propagate the stable edges from the SI hazard check and the timed hazard check. Allow soft colorings from the start state to be overwritten. After all propagation is done, soft propagation values are converted back to un-stabilized values.

20. Check for and report coloring inconsistencies.