This research is on the development of methods for synthesis and verification of asynchronous circuits. The approach is to extend approximation techniques for state exploration, that have been successfully applied to speed-independent circuits, to semi-custom timed circuits. Tools and techniques being developed include: 1. estimators of circuit area, performance, and power at architectural, gate, and circuit levels; 2. a synthesis tool that accepts behavioral specifications and derives gate-level circuits; and 3. a hierarchical verification tool for timed circuits. The verification and synthesis tools are integrated so as to support advanced logic optimizations.