Name
Title | ||
|---|---|---|
Opportunities and Challenges in Process-algebraic Verification of Asynchronous Circuit Designs |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.05.042 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
model checking,csp,process-algebraic verification,asynchronous circuit designs,asynchronous logic synthesis system,balsa environment,case study,asynchronous circuit,large-scale real-life case study,asynchronous hardware,high-level description,hierarchical verification,balsa design,unifying approach,levels of abstraction,gate-level implementation,abstraction level,parallel programming language,process algebra,logic synthesis | Algebraic number,Abstraction,Programming language,Model checking,Computer science,Work in process,Theoretical computer science,Implementation,Parallel programming model,Asynchronous circuit | Journal |
Volume | Issue | ISSN |
146 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
4 | 0.42 | 8 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| X. Wang | 1 | 33 | 1.64 |
| M. Kwiatkowska | 2 | 100 | 6.63 |
| Theodoropoulos, G. | 3 | 110 | 8.22 |
| Qingfu Zhang | 4 | 7634 | 255.05 |