On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP

The work

AuthorsHubert Garavel; Gwen Salaün; Wendelin Serwe
Editors
Typearticle
Year2009
Citekeygaravel2009semantics

Where it appeared

Published inScience of Computer Programming
PublisherElsevier
Volume74
Issue3
Pages100--127

Identifiers

DOI10.1016/j.scico.2008.09.011
handleinria-00381642

Access

Landing pagehttps://inria.hal.science/inria-00381642
Free full texthttps://inria.hal.science/inria-00381642/document

Related

Distinct frombouzafour2018modelchecking
Distinct fromdumitrescu2003construction
Distinct fromebergen1989translating
Distinct fromkastenbaum2021mechanically
Distinct frommartin1986compiling

From bibtex.

Abstract

Hardware process calculi, such as Chp (Communicating Hardware Processes), Balsa, or Haste (formerly Tangram), are a natural approach for the description of asynchronous hardware architectures. These calculi are extensions of standard process calculi with particular synchronisation features implemented using handshake protocols. In this article, we first give a structural operational semantics for value-passing Chp. Compared to the existing semantics of Chp defined by translation into Petri nets, our semantics is general enough to handle value-passing Chp with communication channels open to the environment, and is also independent of any particular (2- or 4-phase) handshake protocol used for circuit implementation. We then describe the translation of Chp into the process calculus Lotos (ISO standard 8807), in order to allow asynchronous hardware architectures expressed in Chp to be verified using the Cadp verification toolbox for Lotos. A translator from Chp to Lotos has been implemented and successfully used for the compositional verification of two industrial case studies, namely an asynchronous implementation of the Des (Data Encryption Standard ) and an asynchronous interconnect of a NoC (Network on Chip).

A copy is held

pdf, 517.5 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-09-16 14:05 UTC
Approved bya person 2026-10-02 10:06 UTC

Filed under

garavel serwe state-space-not-proof the-cost-is-in-the-translation the-discipline-stops-at-the-edge what-one-proves-with

Cite it as

@article{garavel2009semantics,
  title        = {On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP},
  author       = {Hubert Garavel and Gwen Salaün and Wendelin Serwe},
  year         = {2009},
  journal      = {Science of Computer Programming},
  publisher    = {Elsevier},
  volume       = {74},
  number       = {3},
  pages        = {100--127},
  doi          = {10.1016/j.scico.2008.09.011},
}

This record lives at https://refs.drheap.org/garavel2009semantics/ and will keep doing so.