Oxford logo
[WKTZ04] X. Wang, M. Kwiatkowska, G. Theodoropoulos and Q. Zhang. Towards a unifying CSP approach for hierarchical verification of asynchronous hardware. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 231-246, Elsevier Science. 2004. [pdf] [bib]
Downloads:  pdf pdf (308 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. 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 asynchronous hardware synthesis framework like Balsa and verifies 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.