Opportunities and challenges in process-algebraic verification of asynchronous circuit designs

X. Wang; M. Kwiatkowska; G. Theodoropoulos; Q. Zhang

doi:10.1016/j.entcs.2005.05.042

Opportunities and challenges in process-algebraic verification of asynchronous circuit designs

X. Wang, M. Kwiatkowska, G. Theodoropoulos, Q. Zhang

Research output: Journal Publications and Reviews › RGC 22 - Publication in policy or professional journal

5 Citations (Scopus)

26 Downloads (CityUHK Scholars)

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. © 2006 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	189-206
Journal	Electronic Notes in Theoretical Computer Science
Volume	146
Issue number	2
DOIs	https://doi.org/10.1016/j.entcs.2005.05.042
Publication status	Published - 26 Jan 2006
Externally published	Yes
Event	Proceedings of the Second Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS 2005) - Duration: 15 Jul 2005 → 15 Jul 2005

Research Keywords

Asynchronous hardware
CSP
Hierarchical verification
Levels of abstraction
Model checking

Publisher's Copyright Statement

This full text is made available under CC-BY-NC-ND 3.0. https://creativecommons.org/licenses/by-nc-nd/3.0/

Access Output

10.1016/j.entcs.2005.05.042

7910573.pdfFinal Published version, 222 KBLicence: CC BY-NC-ND

Other Access Options

Check CityUHK Library

Permanent Link

Right click to copy link

Cite this

@article{11bf4060572f43bab67c2d7425d993c5,

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. {\textcopyright} 2006 Elsevier B.V. All rights reserved.",

keywords = "Asynchronous hardware, CSP, Hierarchical verification, Levels of abstraction, Model checking",

author = "X. Wang and M. Kwiatkowska and G. Theodoropoulos and Q. Zhang",

year = "2006",

month = jan,

day = "26",

doi = "10.1016/j.entcs.2005.05.042",

language = "English",

volume = "146",

pages = "189--206",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "2",

note = "Proceedings of the Second Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS 2005) ; Conference date: 15-07-2005 Through 15-07-2005",

}

TY - JOUR

T1 - Opportunities and challenges in process-algebraic verification of asynchronous circuit designs

AU - Wang, X.

AU - Kwiatkowska, M.

AU - Theodoropoulos, G.

AU - Zhang, Q.

PY - 2006/1/26

Y1 - 2006/1/26

N2 - 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. © 2006 Elsevier B.V. All rights reserved.

AB - 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. © 2006 Elsevier B.V. All rights reserved.

KW - Asynchronous hardware

KW - CSP

KW - Hierarchical verification

KW - Levels of abstraction

KW - Model checking

UR - http://www.scopus.com/inward/record.url?scp=30644470561&partnerID=8YFLogxK

UR - https://www.scopus.com/record/pubmetrics.uri?eid=2-s2.0-30644470561&origin=recordpage

U2 - 10.1016/j.entcs.2005.05.042

DO - 10.1016/j.entcs.2005.05.042

M3 - RGC 22 - Publication in policy or professional journal

SN - 1571-0661

VL - 146

SP - 189

EP - 206

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

T2 - Proceedings of the Second Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS 2005)

Y2 - 15 July 2005 through 15 July 2005

ER -

Opportunities and challenges in process-algebraic verification of asynchronous circuit designs

Abstract

Research Keywords

Publisher's Copyright Statement

Access Output

Other Access Options

Permanent Link

Other Files and Links

Fingerprint

Cite this