Abstract
This work addresses the analysis and validation of modular CHP specifications for asynchronous circuits, using formalisms and tools coming from the field of distributed software. CHP specifications are translated into an intermediate format (IF) based on communicating extended finite state machines. They are then validated using the IF environment, which provides model checking and bi-simulation tools.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
8. References
M. Renaudin, “Asynchronous Circuits and Systems: a promising design alternative”, Microelectronics-Engineering Journal, Elsevier Science, Vol. 54, No 1–2, Dec 2000, pp. 133–149.
A.J. Martin, “Programming in VLSI: from communicating processes to delay-insensitive circuits”, in C.A.R. Hoare, editor, Developments in Concurrency and Communication, UT Year of Programming Series, 1990, Addison-Wesley, p. 1–64.
H. Zheng, E. Mercer, and C. Myers, “Automatic abstraction for verification of timed circuits and systems”, Proc. CAV’01, LNCS 2102, Springer, pp. 182–193, July, 2001.
A. Cerone, G. Milne: “A Methodology for the Formal Analysis of Asynchronous Micropipelines”, Proc. FMCAD 2000, LNCS No 1954, Springer Verlag, pp.246–262
D. Borrione et al. “An Approach to the Introduction of Formal Validation in an Asynchronous Circuit Design Flow”. Proc. 36th Hawai Int. Conf. on System Sciences (HICSS’03). Jan. 2003
G. Delzanno and A. Podelski, “Model Checking in CLP”. Proc. 5th Int. Conf. TACAS’99. R. Cleaveland, ed., Springer Verlag LNCS No 1579, pp.223–239, 1999.
http://www.inrialpes.fr/vasy/caclp/
J. Cortadella et al. “Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers.” IEICE Trans. on Information and Systems, E80-D(3): 315–325, Mar. 97.
K. Van Berkel, “Handshake Circuits — An Asynchronous Architecture for VLSI Programming”, Cambridge University Press, 1993, ISBN: 0-521-45254-6
M. Bozga, J.-C. Fernandez, et al. “IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems”. Proc. FM’99, Toulouse, LNCS, 1999.
M. Bozga, H. Jianmin, O. Maler, S. Yovine, “Verification of Asynchronous Circuits using Timed Automata”, Proc. TPTS’02 Workshop, Elsevier Science Pub. April 2002.
A Dinh Duc, L. Fesquet, M. Renaudin, “Synthesis of QDI Asynchronous Circuits from DTL-style Petri-Net”, IEEE/ACM Int. Workshop on Logic & Synthesis, New Orleans, June 4–7, 02.
A. Kondratyev, J. Cortadella, M. Kishinevsky, et al.: “Checking signal transition graph implementability by symbolic bdd traversal”. Proc. EDTC’95, pp 325–332, Paris, March 95.
M. Renaudin, J.B. Rigaud, A. Dinhduc, A. Rezzag, A. Sirianni, J. Fragoso: “TAST CAD Tools”, ASYNC’02 TUTORIAL, ISRN: TIMA-RR-02/04/01-FR, 2002
R. Manohar, T.K. Lee, A.J. Martin. “Projection: a synthesis technique for concurrent systems”. 5th Int. Symp. Advanced. Research in Asynchronous Circuits and Systems, Apr. 99.
V. Khomenko and M. Koutny: “Towards An Efficient Algorithm for Unfolding Petri Nets”. Proc. CONCUR’01. Springer-Verlag, LNCS No 2154 (2001) 366–380.
M. Yoeli and A. Ginzburg, “LOTOS-based Verification of Asynchronous Circuits”, Tech. Report, Dept. of Computer Science, Technion, Haifa, 2001.
M. Bozga et al. “Automated validation of distributed software using the IF environment”, Proc. Workshop on Software Model-checking, El. Notes in TCS vol. 55 Elsevier Science Pub. July 00.
http://www.agedis.de and http://www-omega.imag.fr
NIST, Data Encryption Standard (DES), FIPS PUB 46-3, National Institute of Standards and Technology, Reaffirmed 1999 October 25. http://csrc.nist.gov/csrc/fedstandards.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Borrione, D., Boubekeur, M., Mounier, L., Renaudin, M., Siriani, A. (2006). Validation of Asynchronous Circuit Specifications Using IF/CADP. In: Glesner, M., Reis, R., Indrusiak, L., Mooney, V., Eveking, H. (eds) VLSI-SOC: From Systems to Chips. IFIP International Federation for Information Processing, vol 200. Springer, Boston, MA. https://doi.org/10.1007/0-387-33403-3_6
Download citation
DOI: https://doi.org/10.1007/0-387-33403-3_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-33402-8
Online ISBN: 978-0-387-33403-5
eBook Packages: Computer ScienceComputer Science (R0)