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 the CADP Web 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 the CADP Web 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.html

Back to the CADP case studies page