Database of Case Studies Achieved Using CADP

Specification and Verification of Hardware Circuits

Organisation: Centre for Efficiency-Oriented Languages, University College Cork (IRELAND)

Method: muCRL

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: 2007-2009

Size: n/a

Description: The validation of hardware circuits by simulation or prototype testing is both costly and time-consuming. This case study examines how a computer science based approach based on a process algebra can be applied to the specification and verification of hardware circuits that are asynchronous or combinatorial. Such an approach can be applied much earlier in the design cycle, saving time, and reducing both risk and cost.

Two benchmark circuits, an asynchronous arbiter and a hazardous circuit, were analysed. The asynchronous arbiter was described in muCRL, linearised, and its state space was generated. Analysis with CADP showed it to be deadlock-free and satisfying liveness properties.

Conclusions: This case study demonstrates that process algebraic languages, when used in combination with a comprehensive verification toolset such as CADP, are an efficient and effective means of formally specifying and verifing hardware circuits that are asynchronous or combinatorial.

Publications: [Man-07] K.L. Man. "Specification and Analysis of Hardware Systems Using Timed Process Algebras". World Scientific and Engineering Academy and Society Transactions on Electronics, Issue 4, volume 4, April 2007.
Available on line at:
or from the CADP Web site: PDF or PostScript

[Man-09] K.L. Man. "muCRL: A Computer Science based Approach for Specification and Verification of Hardware Circuits". Proceedings of the International SoC Design Conference ISOCC'08, I-387-I-390. IEEE, November 2009.
Available on-line at:
or from the CADP Web site: PDF or PostScript

K.L. Man
Centre for Efficiency-Oriented Languages (CEOL)
Department of Computer Science
University College Cork

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page