Gate-level modelling and verification of asynchronous circuits using CSPM and FDR

FDR (failures-divergences refinement) is a tool for verifying properties of processes expressed in a machine-readable dialect of CSP (CSP_M). This paper shows how to model asynchronous logic blocks as processes in CSP_M and how to verify them using FDR: processes abstract away from the speed of the blocks; multi-way synchronization facilitates the modelling of isochronic forks; receptiveness is formalised as an assertion for FDR to check; process trans formations allow one to model transmission lines and handshaking ports. A process parameterised by a Boolean function suffices to model any complex gate; another such process models N-way mutual exclusion. The approach is illustrated on a variety of asynchronous circuits drawn from the literature.