Database of Case Studies Achieved Using CADP

Asynchronous Circuits.

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 our FTP 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 our FTP 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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page