Abstract.
Asynchronous circuits have received much attention recently due to their potential for
energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis
of asynchronous circuits. This paper develops a theoretical basis for using process algebra and
associated model checking tools to verify asynchronous circuits. We formulate a model that extends
existing verification theory for asynchronous circuits, and integrate it into the framework of standard
process algebra theory. Our theory permits analysis of safeness (i.e. choke) and progress (i.e. illegal
stop, divergence and relative starvation) conditions. We show how the model can be translated into
CSP, and how the satisfaction of safeness and progress requirements can be reduced to refinement
checks in CSP. Finally, the correspondence of our theory with trace theory (i.e. prefix-closed trace
structures), receptive process theory and the XDI model is investigated.
|