×

On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. (English) Zbl 1160.68465

Summary: 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 with 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).

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M99 Computer system organization
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Hauck, S.: Asynchronous design methodologies: an overview, Proceedings of the IEEE 83, No. 1, 69-93 (1995)
[2] Van Berkel, K.; Josephs, M. B.; Nowick, S. M.: Scanning the technology: applications of asynchronous circuits, Proceedings of the IEEE 87, No. 2, 223-233 (1999)
[3] Martin, A. J.: Compiling communicating processes into delay-insensitive VLSI circuits, Distributed computing 1, No. 4, 226-234 (1986) · Zbl 0643.94039 · doi:10.1007/BF01660034
[4] Edwards, D.; Bardsley, A.: Balsa: an asynchronous hardware synthesis language, The computer journal 45, No. 1, 12-18 (2002) · Zbl 1002.68522 · doi:10.1093/comjnl/45.1.12
[5] A. Peeters, M. de Wit, Haste Manual, Version 3.0, Handshake Solutions, 2006
[6] Kessels, J. L. W.; Peeters, A. M. G.: The tangram framework (embedded tutorial): asynchronous circuits for low power, , 255-260 (2001)
[7] , Handbook of process algebra (2001) · Zbl 0971.00006
[8] Fokkink, W.: Introduction to process algebra, (2000) · Zbl 0941.68087
[9] Martin, A. J.: The probe: an addition to communication primitives, Information processing letters 20, No. 3, 125-130 (1985) · Zbl 0586.68023 · doi:10.1016/0020-0190(85)90078-X
[10] M. Renaudin, TAST compiler and TAST_CHP language, Version 0.6, TIMA Laboratory, CIS Group, 2005
[11] D. Borrione, M. Boubekeur, L. Mounier, M. Renaudin, A. Sirianni, Validation of asynchronous circuit specifications using IF/CADP, in: M. Glesner, R.A. da Luz Reis, H. Eveking, V.J. Mooney, L.S. Indrusiak, P. Zipf (Eds.), Proceedings of the International Conference on Very Large Scale Integration of System-on-Chip VLSI-SoC 2003 (Darmstadt, Germany), Darmstadt, 2003, pp. 86–91
[12] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes, Lecture notes in computer science 4590, 158-163 (2007)
[13] ISO/IEC, LOTOS – a formal description technique based on the temporal ordering of observational behaviour, International Standard 8807, International Organization for Standardization – Information Processing Systems – Open Systems Interconnection, Genève, Sep. 1989
[14] M. Renaudin, A. Yakovlev, From hardware processes to asynchronous circuits via Petri nets: An application to arbiter design, in: Proceedings of the Workshop on Token Based Computing TOBACO’04 (Bologna, Italy), 2004
[15] NIST, Data encryption standard (DES), Federal Information Processing Standards FIPS PUB 46-3, National Institute of Standards and Technology, Oct. 25, 1999
[16] Beigné, E.; Clermidy, F.; Vivet, P.; Clouard, A.; Renaudin, M.: An asynchronous noc architecture providing low latency service and its multi-level design framework, , 54-63 (2005)
[17] Salaün, G.; Serwe, W.: Translating hardware process algebras into standard process algebras – illustration with CHP and LOTOS, Lecture notes in computer science 3771, 287-306 (2005) · Zbl 1137.68454 · doi:10.1007/11589976_17
[18] De Boer, F. S.; Palamidessi, C.: A fully abstract model for concurrent constraint programming, Lecture notes in computer science 493, 296-319 (1991) · Zbl 0967.68516
[19] W. Serwe, On concurrent functional-logic programming, Thèse de doctorat, Institut National Polytechnique de Grenoble, Mar. 2002
[20] R.J. van Glabbeek, W.P. Weijland, Branching-time and abstraction in bisimulation semantics (extended abstract), CS R8911, Amsterdam, also in Proc. IFIP 11th World Computer Congress, San Francisco, 1989 (1989)
[21] Garavel, H.; Sifakis, J.: Compilation and verification of LOTOS specifications, Proceedings of the 10th international symposium on protocol specification, testing and verification (Ottawa, Canada), 379-394 (1990)
[22] Milner, R.: A calculus of communicating systems, Lecture notes in computer science 92 (1980) · Zbl 0452.68027
[23] Milner, R.: Communication and concurrency, (1989) · Zbl 0683.68008
[24] Hoare, C. A. R.: Communicating sequential processes, (1985) · Zbl 0637.68007
[25] Ehrig, H.; Mahr, B.: Fundamentals of algebraic specification 1 – equations and initial semantics, EATCS monographs on theoretical computer science 6 (1985) · Zbl 0557.68013
[26] Bolognesi, T.; Brinksma, E.: Introduction to the ISO specification language, Lotos 14, No. 1, 25-59 (1988)
[27] Garavel, H.; Serwe, W.: State space reduction for process algebra specifications, Theoretical computer science 351, No. 2, 131-145 (2006) · Zbl 1086.68091 · doi:10.1016/j.tcs.2005.09.064
[28] Groote, J.; Pol, J.: State space reduction using partial \({\tau}\)-confluence, Lecture notes in computer science 1893, 383-393 (2000) · Zbl 0996.68122
[29] Garavel, H.; Sighireanu, M.: A graphical parallel composition operator for process algebras, Proceedings of the joint international conference on formal description techniques for distributed systems and communication protocols, and protocol specification, testing, and verification, 185-202 (1999) · Zbl 0952.68097
[30] Bergamini, D.; Descoubes, N.; Joubert, C.; Mateescu, R.: Bisimulator: A modular tool for on-the-fly equivalence checking, Lecture notes in computer science 3440, 581-585 (2005) · Zbl 1087.68583 · doi:10.1007/b107194
[31] ISO/IEC, Enhancements to LOTOS (E-LOTOS), International Standard 15437:2001, International Organization for Standardization – Information Technology, Genève, Sep. 2001
[32] Garavel, H.; Lang, F.; Mateescu, R.: Compiler construction using LOTOS NT, Lecture notes in computer science 2304, 9-13 (2002) · Zbl 1051.68658
[33] Lang, F.: Compositional verification using SVL scripts, Lecture notes in computer science 2280, 465-469 (2002) · Zbl 1043.68547
[34] Beigné, E.; Vivet, P.: Design of off-chip and on-chip interfaces for a GALS noc architecture, , 172-181 (2006)
[35] Y. Durand, C. Bernard, D. Lattard, FAUST : On-chip distributed architecture for a 4G baseband modem SoC, in: Proceedings of Design and Reuse IP-SOC’05 (France), 2005, pp. 51–55
[36] Garavel, H.; Lang, F.: SVL: A scripting language for compositional verification, Proceedings of the 21st IFIP WG 6.1 international conference on formal techniques for networked and distributed systems, 377-392 (2001)
[37] Salaün, G.; Serwe, W.; Thonnart, Y.; Vivet, P.: Formal verification of CHP specifications with CADP – illustration on an asynchronous network-on-chip, , 73-82 (2007)
[38] Van Berkel, K.: Handshake circuits: an asynchronous architecture for VLSI programming, International series on parallel computation 5 (1993) · Zbl 0875.68551
[39] Wang, X.; Kwiatkowska, M. Z.; Theodoropoulos, G.; Zhang, Q.: Towards a unifying CSP approach for hierarchical verification of asynchronous hardware, Electronic notes in theoretical computer science 128, 231-246 (2004) · Zbl 1272.68278
[40] Baulch, G.; Hemmendinger, D.; Traver, C.: Analyzing and verifying locally clocked circuits with the concurrency workbench, , 144-147 (1995)
[41] B. Rahardjo, SPIN as a hardware design tool, in: J.-C. Gregoire (Ed.), Proceedings of the First SPIN Workshop SPIN 1995 (Quebec, Canada), 1995
[42] G. Clark, G. Taylor, The verification of asynchronous circuits using CCS, Tech. Rep. ECS-LFCS-97-369, University of Edinburgh, Department of Computer Science, Oct. 1997
[43] Kapoor, H. K.; Josephs, M. B.: Modelling and verification of delay-insensitive circuits using CCS and the concurrency workbench, Information processing letters 89, No. 6, 293-296 (2004) · Zbl 1183.68387 · doi:10.1016/j.ipl.2003.12.007
[44] He, J.; Turner, K. J.: Verifying and testing asynchronous circuits using LOTOS, Proceedings of the joint international conference on formal description techniques for distributed systems and communication protocols, and protocol specification, testing, and verification, 267-283 (2000)
[45] M. Yoeli, A. Ginzburg, LOTOS/CADP-based verification of asynchronous circuits, Technical Report TR CS-2001-09, Technion, Computer Science Department, Haifa, Israel, Mar. 2001
[46] Yoeli, M.; Kol, R.: Verification of systems and circuits using LOTOS, (2008)
[47] Wang, X.; Kwiatkowska, M. Z.: On process-algebraic verification of asynchronous circuits, , 37-46 (2006)
[48] Josephs, M. B.: Gate-level modelling and verification of asynchronous circuits using cspm and FDR, , 83-94 (2007)
[49] Bailey, A.; Mccaskill, G. A.; Milne, G. J.: An exercise in the automatic verification of asynchronous designs, Formal methods in system design 4, No. 3, 213-242 (1994) · Zbl 0795.94020 · doi:10.1007/BF01384047
[50] Cerone, A.; Milne, G. J.: Property verification of asynchronous systems, Innovations in systems and software engineering 1, No. 1, 25-40 (2005)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.