Thesis Abstract
                                ---------------

Title: Delay Insensitive Processes: A Formal Approach to the Design of Asynchronous Circuits

With the proliferation of electronic devices in our day-to-day existence, the quality of the
underlying circuits is becoming increasingly important. The devices are expected to run robustly 
under different operating conditions. Asynchronous circuits are promising as compared to 
synchronous approach, in achieving low power, low noise and high speed circuits which can be 
developed in a modular way. However, the absence of a global clock in these circuits comes 
at the cost of added concurrency. Therefore, it is important to have a better understanding
of such highly concurrent systems in order to have confidence in the resultant devices.


A formalism known as delay-insensitive (DI) processes is used to reason about a special class 
of asynchronous circuits that make no assumptions about delays in any of its components or wires. 
The formalism is shown to be useful in verification of such circuits using existing verification 
tools. DI processes can be easily integrated into such tools and existing equivalence checking 
techniques applied to them, instead of starting from scratch. In particular, the application
of the Concurrency Workbench (CWB) to the verification of DI processes is shown by modelling 
them in CCS and using MUST-testing for equivalence and refinement checking.


DI processes interact with their environment to form closed systems. A new restriction operator 
is defined to obtain the effective behaviour of a process in a given environment, which eases
specification and facilitates implementation. This operator is also shown to be more general 
than the alternation operator defined previously by Mallon.


Building on the work of Josephs and Udding, the algebraic semantics of DI processes is investigated 
and transformations are automated using the term rewriting system Maude. A canonical form is defined 
and is further used for equivalence and refinement checking based on syntactic comparison.


The formalism is useful not only in verification, but also in the decomposition of certain forms 
of processes that have been found difficult for logic synthesis tool, such as Petrify, to handle.
The decompositions introduce Wires and Fork elements that preserve the delay-insensitive behaviour
of asynchronous controllers. The proposed heuristics are applied on benchmark examples to help the 
tool Petrify to synthesise area-efficient circuits rapidly.


Besides using the CWB, Maude and Petrify, the experiments reported here have involved tools
developed in-house, namely, Furey's translation tool di2pn, verification tool diana and the 
authors translation tool di2ccs.

The thesis demonstrates that (i) DI processes can be verified by adopting existing verification 
tools and techniques; (ii) consideration of the environment of a process leads to simpler 
specifications; and (iii) decomposing specifications leads to area efficient implementations.


Bibtex:
@phdthesis{hkapoor2004,
author = "H. K. Kapoor",
title = "Delay Insensitive Processes: A Formal Approach to the Design of Asynchronous Circuits",
school = "London South Bank University, UK",
year = "2004",
month = "July",
}