Preface

详细信息    查看全文

• 作者：Djamal Benslimane ; Chirine Ghedira ; Zakaria Maamar
• 关键词：Asynchronous hardware ; Hierarchical verification ; CSP ; Model checking ; Levels of abstraction
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2006
• 出版时间：24 January 2006
• 年：2006
• 卷：146
• 期：1
• 页码：1-2
• 全文大小：58 K

文摘

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.