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).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beigné, E., Clermidy, F., Vivet, P., Clouard, A., Renaudin, M.: An Asynchronous NOC Architecture Providing Low Latency Service and Its Multi-Level Design Framework. In: ASYNC 2005, March 2005, pp. 54–63. IEEE Computer Society, Los Alamitos (2005)
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14(1), 25–59 (1988)
Borrione, D., Boubekeur, M., Mounier, L., Renaudin, M., Sirianni, A.: Validation of Asynchronous Circuit Specifications using IF/CADP. In: VLSI-SoC 2003, December 2003, pp. 86–91 (2003)
de Boer, F.S., Palamidessi, C.: A Fully Abstract Model for Concurrent Constraint Programming. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 296–319. Springer, Heidelberg (1991)
Edwards, D., Bardsley, A.: Balsa: An Asynchronous Hardware Synthesis Language. The Computer Journal 45(1), 12–18 (2002)
Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer, Heidelberg (2000)
Garavel, H., Lang, F., Mateescu, R.: Compiler Construction using LOTOS NT. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 9–13. Springer, Heidelberg (2002)
Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. EASST Newsletter 4, 13–24 (2002)
Garavel, H., Serwe, W.: State Space Reduction for Process Algebra Specifications. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 164–180. Springer, Heidelberg (2004)
Garavel, H., Sifakis, J.: Compilation and Verification of LOTOS Specifications. In: International Symposium on Protocol Specification, Testing and Verification, June 1990. IFIP, pp. 379–394. North-Holland, Amsterdam (1990)
Hauck, S.: Asynchronous Design Methodologies: An Overview. Proceedings of the IEEE 83(1), 69–93 (1995)
ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, Geneva (1989)
Kessels, J.L.W., Peeters, A.M.G.: The Tangram Framework (Embedded Tutorial): Asynchronous Circuits for Low Power. In: ASP-DAC 2001, pp. 255–260. ACM, New York (2001)
Lang, F.: Compositional Verification using SVL Scripts. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 465–469. Springer, Heidelberg (2002)
Martin, A.J.: The Probe: An Addition to Communication Primitives. Information Processing Letters 20(3), 125–130 (1985)
Martin, A.J.: Compiling Communicating Processes into Delay-Insensitive VLSI Circuits. Distributed Computing 1(4), 226–234 (1986)
Data Encryption Standard (DES). Federal Information Processing Standards FIPS PUB 46-3, National Institute of Standards and Technology (October 25, 1999)
Renaudin, M.: TAST Compiler and TAST_CHP Language, Version 0.6. TIMA Laboratory, CIS Group (2005)
Renaudin, M., Yakovlev, A.: From Hardware Processes to Asynchronous Circuits via Petri Nets: an Application to Arbiter Design. In: TOBACO 2004 (June 2004)
Serwe, W.: On Concurrent Functional-Logic Programming. Thèse de doctorat, Institut National Polytechnique de Grenoble (March 2002)
van Berkel, K.: Handshake Circuits: An Asynchronous Architecture for VLSI Programming. Cambridge University Press, Cambridge (1993)
Wang, X., Kwiatkowska, M., Theodoropoulos, G., Zhang, Q.: Towards a Unifying CSP approach for Hierarchical Verification of Asynchronous Hardware. In: AVoCS 2004. ENTCS, vol. 128, pp. 231–246 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salaün, G., Serwe, W. (2005). Translating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_17
Download citation
DOI: https://doi.org/10.1007/11589976_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)