Introduction:

In this paper we present a technique for automatic synthesis of delay insensitive circuits from high level programs written in a language called Synchronized Transitions. This language is intended for both formal verification and synthesis, making it possible to use the same description (program) for formal verification, possibly with the assistance of a mechanical theorem prover, and for automated synthesis. As the synthesis is performed without manual intervention, the fabricated chip corresponds exactly to the descrition that has been formally verified. A circuit is described as many small processes, called transitions, executing concurrently. Therefore, each process can be realized as a sub-circuit independently of other processes. The entire chip consists of sub-circuits with the same structure, simplifying both the synthesis and the layout generation.

The majority of digital chips constructed today are synchronous. However, in recent years there has been a revival in research activity in asynchronous circuits. Asynchronous circuits do not have global synchronization signals, which makes them more robust and often faster than synchronous circuits. They are potentially faster, because the speed is determined by the average case of factors such as temperature, power variation, data dependence, and fabrication parameters. For traditional synchronous designs, the speed is limited by the worst case of these factors. Problems with clock skew are avoided and the power consumption is smoother. A subset of asynchronous circuits are delay insensitive, i.e. they function correctly disregarding delays in wires and gates.

Our approach to delay insensitivity is briefly explained in Sect. 2. A more thorough explanation can be found in [Staunstrup90]. In Sect. 3 the verification aspect is considered. The synthesis technique is described in Sect. 4, and in Sect. 5 we describe a compiler that implements this technique.

One-line summary: Using "Synchronized Transitions" for both program verification and layout generation.

Published in: Jean-Pierre Banatre and Daniel Le Metayer, editors, Research Directions in High-Level Parallel Programming Languages, pages 326-337. Springer-Verlag (Lecture Notes in Computer Science #574), 1991. (Mont Saint-Michel, France, June 17-19.)

Back to Per's publication page.