Organisation: 
National Polytechnic Institute of Grenoble
University Joseph Fourier (FRANCE) 

Method: 
CHP
IF 
Tools used: 
CADP (Construction and Analysis of Distributed Processes)
IF toolbox 
Domain: 
Hardware Design.

Period: 
2003

Size: 
about 5.3 million states and 30 million transitions

Description: 
An asynchronous circuit can be seen as a set of communicating
processes, and thus described in languages based on process algebras,
as for instance CHP, a language based on CSP and developed initially
by Alain Martin. Thus verification tools for asynchronous process
algebra specifications are a good starting point when considering the
verification of asynchronous circuits.
A translator from CHP to IF has been developed, using sophisticated techniques in order to reduce the state space of the corresponding LTS, which was generated using the IF toolbox. Then CADP tools, such as EVALUATOR can be used for the verification of properties of the specification. The approach is illustrated by the verification of an asynchronous circuit implementing the Data Encryption Standard (DES). Among the verified properties are deadlock freedom, and correct synchronisation of the different parts of the circuit over the 16 iterations of the DES. For some properties, hiding of labels not occurring in the property and reducing with respect to branching equivalence before verification of the property was found very helpful: Since reducing the LTS requires less than half the time needed for the verification using the complete LTS, and the verification on the reduced LTS is almost instantaneous, this approach allows to reduce the verification time considerably. 
Conclusions: 
CADP offers a convenient abstraction level for the formal validation
of CHP specifications. When linked by an automatic tool to a design
flow, it allows to prove essential properties of an architecture
earlier in the design process, and to check preservation of properties
when exploring architectures obtained by transformations not yet
formally proven correct.

Publications: 
[BorrioneBoubekeurMounieretal03]
Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin,
and Antoine Sirianni.
"Validation of Asynchronous Circuit Specifications using IF/CADP".
In Manfred Glesner, Ricardo Augusto da Luz Reis, Hans Eveking,
Vincent John Mooney, Leandro Soares Indrusiak, and Peter Zipf, editors,
Proceedings of the IFIP International Conference on Very Large Scale
Integration of SystemonChip VLSISoC 2003 (Darmstadt, Germany),
pp. 8691, December 2003.
Available online at: http://wwwverimag.imag.fr/~async/BIBLIO/papers/BorrioneBoubekeurMounier03b.pdf or from our FTP site in PDF or PostScript [BoubekeurSchellekens07] Menouer Boubekeur, and M. P. Schellekens. "Automatic Optimization Techniques for Formal Verification of Asynchronous Circuits" In D. Bouami, E. M. Aboulhamid, M. Eleuldj, and M. Zwolinski, editors, Proceedings of the 5th International Workshop on Formal Aspects of Component Software FACS'2008 (Málaga, Spain), pp. 283286, december 2007. Available online from our FTP site in PDF or PostScript 
Contact:  Menouer Boubekeur TIMA 46, avenue Félix Viallet F38031 Grenoble Cedex FRANCE Tel: +33 (0)4 76 57 45 10 Fax: +33 (0)4 76 47 38 14 Email: Menouer.Boubekeur@imag.fr 
Further remarks:  This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies The analysis of a different model of the same cryptographic protocol is described in another case study: http://cadp.inria.fr/casestudies/15fdes.txt 