Michael Boyer
Advisor: Cherrice Traver
Union College

Using ATACS for Verification of Hazard-Freedom of Phased Logic Wrappers

Phased Logic (PL) is an asynchronous methodology introduced in [1] that supports the synchronous design paradigm by allowing automated translation from a clocked netlist implementation of a circuit to a self-timed netlist implementation. Early work with PL utilized a fine-grain mapping technique in which each individual gate in the clocked netlist was mapped directly to a PL gate. More recent work by Reese, Thornton, and Traver [2], however, has utilized a coarse-grain mapping technique in which entire logic blocks in the clocked netlist are enclosed by PL wrapper logic. Because the wrapper logic interfaces between the external PL circuit and the internal logic block, the logic block itself can be reused with no modification. There are two types of logic blocks in this methodology [3]: barrier blocks, which contain D-Flip-Flops as well as combinational logic; and through blocks, which contain only combinational logic. There are also two different speed-up techniques supported by coarse-grain PL: time borrowing and early evaluation. The choice of wrapper depends both on the type of logic block and whether or not it uses either of the speed-up techniques. There are four different wrappers, one for each of the four possible block configurations.

ATACS is a tool developed by the Myers Research Group at the University of Utah for the synthesis and verification of timed asynchronous circuits. The use of timed asynchronous circuits allows us to take advantage of known (or assumed) timing information in order to optimize a circuit's performance, as discussed in [4]. Although ATACS supports both synthesis and verification, our primary interest for this research was its verification capability. The program supports six different timing methods that affect this verification process; the method which we were concerned with was POSETs, which represents timing information using zones and represents timing between events using a POSET matrix. The program also supports three different types of verification; only hazard checking was relevant to our research. Hazards are defined in [4] as "conditions generated by the structure of the circuit or timing relationships between inputs and propagation delays that can cause incorrect behavior." ATACS automates the process of finding hazards and allowed us to analyze the potential hazards in each one of the manually designed PL wrapper circuits. By systematically modifying the delays of the individual components in each wrapper and using ATACS to find and examine the resulting hazards, we were able to determine the rules that the delays must follow in order to guarantee the hazard-freedom of the wrapper circuits.


[1] Daniel H. Linder and James C. Harden, "Phased Logic: Supporting the Synchronous Design Paradigm with Delay-Insensitive Circuitry." IEEE Transactions on Computers, Vol. 45, No. 9, September 1996.

[2] Robert B. Reese, Mitchell A. Thornton, and Cherrice Traver, "A Course-Grain Phased Logic CPU", 9th IEEE International Symposium on Asynchronous Circuits and Systems (Async 2003), Vancouver, Canada.

[3] Robert B. Reese, Mitchell A. Thornton, and Cherrice Traver, "Async 2004 Tutorial - Phased Logic", Workshop Notes, 10th International Symposium on Advanced Research in Asynchronous Circuits and Systems, Crete, Greece, April 2004.

[4] Curtis A. Nelson, Chris J. Meyers, and Tomohiro Yoneda, "Efficient Verification of Hazard-Freedom in Gate-Level Timed Asynchronous Circuits", 2003 International Conference on Computer-Aided Design, November 2003.