In: Judi M.T. Romijn, Graeme P. Smith, Jaco Pol (Eds.): Lecture Notes in Computer Science, 3771: Integrated Formal Methods: 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005., pages 287-306. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1158997617,.
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 paper, 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 veri.cation of the control part of an asynchronous circuit implementing the DES (Data Encryption Standard).