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

Gwen Salaün, Wendelin Serwe

Proceedings of the 5th International Conference on Integrated Formal Methods IFM 2005 (Eindhoven, The Netherlands), November - December 2005.

Full version available as INRIA Research Report RR-5666.

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).

25 pages

PDF

PostScript

Slides of G. Salaün's lecture at IFM'05

PDF