On Process-algebraic Verification of Asynchronous Circuits

Issue title: Half a Century of Inspirational Research: Honoring the Scientific Influence of Antoni Mazurkiewicz

Article type: Research Article

Authors: Wang, Xu | Kwiatkowska, Marta

Affiliations: International Institute of Software Technology, United Nations University, P.O. Box 3058, Macau. E-mail: wx@iist.unu.edu | Oxford University Computing Laboratory, Parks Road, Oxford OX1 3QD, UK. E-mail: Marta.Kwiatkowska@comlab.ox.ac.uk

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.

Keywords: Process algebra, asynchronous circuits, assume/guarantee verification, progress/liveness, and CSP/FDR2

Journal: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 283-310, 2007