Towards a Unifying CSP approach to Hierarchical Verification of Asynchronous Hardware

Formal verification is increasingly important in asynchronous circuit design, since the lack of a global synchronizing clock makes errors due to concurrency (e.g., deadlocks) virtually impossible to detect by means of conventional methods such as simulation. This paper presents a hierarchical approach to asynchronous systems verification using CSP and its model checker FDR. The approach reflects the hierarchical nature of asynchronous hardware synthesis frameworks, for example the Balsa system, and enables the verification of the system at different levels of abstraction against properties such as deadlock, delay insensitivity, conformance and refinement. We demonstrate the feasibility of our approach by automatically detecting errors due to delay sensitivity and deadlock in simple asynchronous hardware components.