|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: http://www.worldses.org/journals/electronics/electronics-april2007.htm 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: http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=4815653&tag=1 or from the CADP Web site: PDF
or
PostScript
|
| Contact: | K.L. Man Centre for Efficiency-Oriented Languages (CEOL) Department of Computer Science University College Cork Ireland Email: pafesd@gmail.com |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page