HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 8:10:55 PM
Last modification on : Friday, February 4, 2022 - 3:24:19 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:59:58 PM


  • HAL Id : inria-00070342, version 1



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⟩



Record views


Files downloads