Opportunities and Challenges in Process-algebraic Verification of Asynchronous Circuit Designs

This paper reports our experiences of applying process algebras and associated tools (esp. CSP/FDR2) to verify asynchronous circuit designs developed in the Balsa environment. Balsa is an asynchronous logic synthesis system which uses syntax-directed compilation to generate gate-level implementations from high-level descriptions in a parallel programming language (also called Balsa). Previously, we have proposed a unifying approach to compositionally verifying Balsa designs across several abstraction levels. This paper continues our effort by applying and testing our approach on several large-scale real-life case studies. We describe the outcome of verification for the case studies, and also analyse the strengths and limitations of our method.