Title: Efficient Verification of Hazard-Freedom in Gate-Level Timed Circuits

New algorithms will be presented for verifying hazard-freedom in timed circuits. Timed circuits are a class of asynchronous circuits that utilize explicit timing information for optimization throughout the entire design process. Asynchronous circuits offer the potential advantage over synchronous circuits of faster operation at the expense of circuitry overhead to eliminate hazards. Hazards are conditions generated by the structure of the circuit or timing relationships between inputs and propagation delays that can cause incorrect behavior. Each internal node and output of the circuit must be verified for hazard-freedom to ensure correct operation. Current verification algorithms require a netlist and a timed state graph. These approaches suffer from state explosion problems because each node is treated as a new state variable potentially doubling the number of states. In addition, these algorithms do not utilize existing timing information to help determine hazard-freedom. Our approach abstracts the behavior of internal nodes and makes a determination of hazard-freedom through a process of adding an array of implicit information about each internal node to each specification state (i.e., states that only include information about primary inputs and outputs). This information is used in the place of exhaustive state exploration to determine behavior of each node under the given timing constraints. Initial experimental results match those from established software tools using standard benchmarks. For large benchmarks, a significant reduction in computation time is possible as the size of the state space is reduced substantially.