Timing algorithm version 1.1 9/19/2002

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

2. Color those edges that we know are stable in the untimed sense. Means finding the state->state transitions where the output changes and seeing 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.

3. Find points where the state graph has state-to-state transitions from R->F or F->R. For each one of these, do the following:

4. Find the edge transition at which this occurs (ie. a+, b-, etc.)

5. Set this as the reference point.

6. Find the maximum delay from this transition event to the node of interest in my decomposition.

a. What if this path doesn't exist, or must it always? It will always exist.

b. If there are two paths, do I take the longer one? Yes, for now. This is the conservative route. Later, maybe dynamic analysis could be used to determine which path is the active one.

c. What if there is both a + and - event? See answer to b above.

7. Find the first zone following the transition in step 4.

8. For each successor state:

9. For each transition out of the successor state:

10. Find the causal event for this transition.

(assume it’s the previous transition)

11. Add this information to the zone.

12. Look up in the ruleADT the <lower, upper> bounds.

The ruleADT is indexed by the event number.

The row is the enabling event, the column is the enabled event: rules[enabled,enabling]

A non-zero entry means something interesting.

13. Modify zone with new <lower upper> information

14. Canonicalize zone

15. Continue until the zone timing shows I've exceeded max delay in my decomposition or I reach a termination point. If max delay exceeded, color edge 0 or 1 and go back to step 3. A termination point is when I find an edge enabled in the opposite direction of the transition under consideration. If this happens, cannot stabilize the edge.

16. Propagate the stable edges and check for coloring inconsistencies.