Database of Case Studies Achieved Using CADP

Asynchronous Circuit for Data Encryption Standard (DES).

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: [Borrione-Boubekeur-Mounier-et-al-03] 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 System-on-Chip VLSI-SoC 2003 (Darmstadt, Germany), pp. 86-91, December 2003.
Available on-line at: http://www-verimag.imag.fr/~async/BIBLIO/papers/Borrione-Boubekeur-Mounier-03b.pdf
or from our FTP site in PDF or PostScript

[Boubekeur-Schellekens-07] 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. 283-286, december 2007.
Available on-line from our FTP site in PDF or PostScript
Contact:
Menouer Boubekeur
TIMA
46, avenue Félix Viallet
F-38031 Grenoble Cedex
FRANCE
Tel: +33 (0)4 76 57 45 10
Fax: +33 (0)4 76 47 38 14
E-mail: Menouer.Boubekeur@imag.fr



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies The analysis of a different model of the same cryptographic protocol is described in another case study: http://cadp.inria.fr/case-studies/15-f-des.txt


Last modified: Tue Sep 27 15:27:29 2016.


Back to the CADP case studies page