Translating Hardware Process Algebras into Standard Process Algebras : Illustration with CHP and LOTOS

Gwen Salaün 1 Wendelin Serwe
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : A natural approach for the description of asynchronous hardware designs are hardware process algebras, such as Martin's CHP (Communicating Hardware Processes), Tangram, or BALSA, which are extensions of standard process algebras with particular operators exploiting the implementation of synchronisation using handshake protocols. In this research report, we give a structural operational semantics for value-passing CHP. Compared to existing semantics of CHP defined by translation into Petri nets, our semantics handles value-passing CHP with communication channels open to the environment and is independent of any particular (2- or 4-phase) handshake protocol used for circuit implementation. In a second step, we describe the translation of CHP into the standard process algebra LOTOS, in order to allow the application of the CADP verification toolbox to asynchronous hardware designs. A prototype translator from CHP to LOTOS has been successfully used for the compositional verification of the control part of an asynchronous circuit implementing the DES (Data Encryption Standard).
Document type :
Reports
RR-5666, INRIA. 2005, pp.25
Liste complète des métadonnées

https://hal.inria.fr/inria-00070342
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:10:55 PM
Last modification on : Saturday, September 17, 2016 - 1:38:19 AM
Document(s) archivé(s) le : Sunday, April 4, 2010 - 8:59:58 PM

Identifiers

  • HAL Id : inria-00070342, version 1

Collections

Citation

Gwen Salaün, Wendelin Serwe. Translating Hardware Process Algebras into Standard Process Algebras : Illustration with CHP and LOTOS. RR-5666, INRIA. 2005, pp.25. <inria-00070342>

Share

Metrics

Record views

145

Document downloads

114