|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Technion, Department of Computer Science (ISRAEL)
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Hardware Design.
|
| Period: |
January-February 1998.
|
| Size: |
about 50 lines of LOTOS
|
| Description: |
Asynchronous (clock-free) systems are particularly attractive in the context of high-speed and high-density hardware technologies.
The currently available literature in the domain of asynchronous circuits focuses mainly on the (correct-by-construction) circuit synthesis problem.
However, less attention has been given to the verification problem.
This work proposes a method for analyzing asynchronous circuits built from modular components. The realizations (i.e., implementations) and the specifications (i.e., external behaviours) of the circuits are described in LOTOS and their properties are checked using the CADP toolset. The method uses an intermediate model of the dynamic behaviour of asynchronous circuits, called Circuit Transition System, which can be represented by a LOTOS program. The verification problem consists in checking several requirements on an asynchronous circuit description: observational equivalence of specification and realization, livelock freedom, and no-desirable-output condition (deadlock freedom).
These properties are verified automatically using the CAESAR and ALDEBARAN tools. The approach is illustrated by two examples of asynchronous circuits: a combinational network built from two-entry XOR gates, and a modulo-3 transition counter.
|
| Conclusions: |
Formal description techniques like LOTOS appear to be particularly suitable for the modelling and verification of asynchronous circuits.
The approach of using LOTOS and state-of-the-art verification tools such as CADP was found to compete favourably with other available methods for the verification of asynchronous circuits.
|
| Publications: |
[Yoeli-Ginzburg-01]
Michael Yoeli and Abraham Ginzburg.
"LOTOS/CADP-based Verification of Asynchronous Circuits."
Technical Report CS-2001-09, Technion, Department of Computer Science,
2001.
Available on-line at: http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2001/CS/CS-2001-09 or also from the CADP Web site in PDF 
or
PostScript 
This reference supersedes the following one: Michael Yoeli and Abraham Ginzburg. "LOTOS-based Verification of Asynchronous Circuits." Technical Report TR CS0951, Technion, Department of Computer Science, January 1998. [Yoeli-01] Michael Yoeli. "Examples of LOTOS-Based Verification of Asynchronous Circuits." Technical Report CS-2001-08, Technion, Department of Computer Science, 2001. Available on-line at: http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2001/CS/CS-2001-08 or also from the CADP Web site in PDF
or
PostScript
This reference supersedes the following one: Michael Yoeli. "Modulo-3 Transition Counter: A Case Study in LOTOS-Based Verification." Technical Report TR CS0950, Technion, Department of Computer Science, February 1998. |
| Contact: | Michael Yoeli Technion, Department of Computer Science Haifa 32000 Israel E-mail: myoeli@cs.technion.ac.il |
| 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