Automatic Synthesis Of Asynchronous Circuits Based On Action Refinement

A widely accepted approach to design hardware circuits is stepwise refinement. Action refinement is an essential operation in the hierarchical system specification methodology. This methodology leads to a successful technique known as top-down system design. It allows the representation of systems in a hierarchical way, changing the level of abstraction by interpreting actions on a higher level by more complicated processes on a lower level until the implementation level is reached. Although this theory has been researched for many years, until so far there is no work on applying it to realistic applications.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, provide component modularity and adapt to processing and environmental variations. Specifying an asynchronous circuit is a cumbersome and error prone task.The main contribution of this thesis is that action refinement techniques and theories are applied to the realistic applications, integrating with the design and verification technologies of asynchronous circuits, and furthermore, providing a novel method for automatic synthesis of asynchronous circuits. In other words, we will discuss case studies for syntactic and semantic action refinement in asynchronous circuits.First, with the purpose of providing a formal specification of pipelines, a central problem in asynchronous hardware design, we show how action refinement can be used to develop asynchronous pipelined microprocessors, where each functional unit of the processor is stepwise obtained, leading to a structured and modular design. Furthermore, the handling of hazard situations is realized during the refinement procedures.Second, we present an automatic technique for handshake expansion and reshuffling in asynchronous control circuit design. Handshake expansion and reshuffling are two key steps in high-level synthesis of asynchronous circuits. We show how to use a parametric action refinement technique to develop handshake expansion for asynchronous control circuits. We present a formal refinement model for handshake expansion. The proposed methodology employs wait event structures. It derives a true concurrency model with the maximum parallelism and the refined system conforms to the original specification with respect to a vertical bis-mulation relation. Furthermore, the refinement function can preserve correctness and deadlock-freeness of the behavior in the refined system.Finally, the method explores reshuffling of events under interface and concurrency constraints by means of concurrency reduction. The algorithm trades off the number of required state signals and logic complexity. In doing so, the algorithm optimizes the circuit both in size and performance. Experimental results show a significant increase in the solution space explored when compared to existing synthesis tools.