Browse Theses

In recent years, there has been a resurgence of interest in the design of asynchronous circuits due to their ability to eliminate clock skew problems, achieve average case performance, adapt to processing and environmental variations, provide component modularity, and lower system power requirements. Traditional academic asynchronous designs methodologies use unbounded delay assumptions, resulting in circuits that are verifiable, but ignore timing for simplicity, leading to unnecessarily conservative designs. In industry, however, timing is critical to reduce both chip area and circuit delay. Due to a lack of formal methods that handle timing information correctly, circuits with timing constraints usually require extensive simulation to gain confidence in the design.This thesis bridges this gap by introducing timed circuits in which explicit timing information is incorporated into the specification and utilized throughout the design procedure to optimize the implementation. Our timed circuits are more efficient than those produced using untimed methods and more reliable than those produced using ad hoc design techniques. Timing analysis, however, often introduces substantial complexity into the design procedure, and has hitherto either been avoided, simplified, or considered only after synthesis. In this thesis, we describe an exact and efficient timing analysis algorithm, and its application to the automatic synthesis and verification of gate-level timed circuits. Our synthesis procedure generates hazard-free timed circuits and maps the resulting implementations to practical semi-custom gate libraries. The resulting implementations are up to 40 percent smaller and 50 percent faster than previous asynchronous designs. We also demonstrate that our timed designs can be smaller and faster than their synchronous counterparts. After back-annotating the synthesized circuits, our verification procedure checks that all circuits satisfy their specifications. This procedure has also been applied to a wide collection of highly concurrent timed circuits that could not previously be verified.