On process-algebraic verification of asynchronous circuits
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.
asynchronous circuits process algebra assume/guarantee verification progress/liveness and csp/fdr2