Verification and Implementation of Delay-Insensitive Processes in Restrictive Environments

• Autorzy: Kapoor H.K. , Josephs M.B. , Furey D.P.
• Języki publikacji: EN

Abstrakty

EN

A delay-insensitive module communicates with its environment through wires of unbounded delay. To avoid transmission interference, the absorption of a signal transition must be acknowledged before another one is propagated along the same wire. The environment may guarantee, however, to interact with the module in an even more restrictive way. It is worthwhile taking this into account when synthesising the module because it may allow for a cheaper, faster implementation. The concept of restriction has been built into our translation tool, di2pn (to help in synthesis), and our analysis tool, diana (to perform equivalence and refinement checking). Formally, DI-Algebra is equipped with a new operator that weakens the specification of a module by taking its environment into account. This operator is a useful instance of divergence extension, a concept introduced by Mallon. Divergence extension in general, and restriction and alternation in particular, can be represented with the parallel composition operator and so are amenable to algebraic reasoning.

Słowa kluczowe

EN

delay-insensitive circuits; verification; process algebras; restrictive environments; closed systems; asynchronous circuitis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 21--48
• Opis fizyczny: bibliogr. 37 poz.

Twórcy

autor

Kapoor H.K.

autor

Josephs M.B.

autor

Furey D.P.

• Dhirubhai Ambani Institute of Information and Communication Technology, Near Indroda Circle, Gandhinagr 382 007, India,

Bibliografia

• [1] Balemi, S.: Communication Delays in Connections of Input/Output Discrete Event Processes, IEEE Proceedings of 31st Conference on Decision and Control, IEEE, December 1992, 3374-3379.
• [2] Balemi, S., Hoffmann, G. J., Gyugyi, P., Wong-Toi, H., Franklin, G. F.: Supervisory Control of a Rapid Thermal Multiprocessor, IEEE Transactions on Automatic Control, 38(7), July 1993, 1040-1059.
• [3] Clarke, E.M., Long, D. E.,McMillan, K. L.: CompositionalModel Checking, Proceedings of Fourth Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society, June 1989, 353-362.
• [4] Cortadella, J., Kishinevsky,M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: A Tool forManipulating Concurrent Specifications and Synthesis of Asynchronous Controllers, IEICE Transactions on Information and Systems, 3(E80-D), 1997, 315-325.
• [5] Furber, S. B., Garside, J. D., Riocreux, P., Temple, S., Day, P., Liu, J., Paver, N. C.: AMULET2e: An Asynchronous Embedded Controller, Proceedings of the IEEE, 87(2), 1999, 243-256.
• [6] Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall International Series in Computer Science, 1985.
• [7] Josephs, M. B.: Receptive Process Theory, Acta Informatica, 29(1), 1992, 17-31.
• [8] Josephs, M. B.: Verification of a Loadable Counter, Lecture Notes of Summer School on Asynchronous Circuit Design, TIMA Laboratory, Grenoble, France, July 2002.
• [9] Josephs,M. B., Furey, D. P.: Delay-Insensitive Interface Specification and Synthesis, Proceedings of Design, Automation and Test in Europe (DATE), March 2000, 169-173.
• [10] Josephs, M. B., Hoare, C. A. R., He, J.: A Theory of Asynchronous Processes, Technical Report PRG-TR-6-89, Oxford University Computing Laboratory, Oxford, England, 1989.
• [11] Josephs, M. B., Lucassen, P. G., Udding, J. T., Verhoeff, T.: Formal Design of an Asynchronous DSP Counterflow Pipeline: A Case Study in Handshake Algebra, Proceedings of International Symposiumon Advanced Research in Asynchronous Circuits and Systems (ASYNC'94), IEEE Computer Society, 1994, 206-215.
• [12] Josephs, M. B., Udding, J. T.: Delay-Insensitive Circuits: An Algebraic Approach to their Design, CONCUR' 90, Lecture Notes in Computer Science, 458, 1990, 342-366.
• [13] Josephs, M. B., Udding, J. T.: An Overview of D-I Algebra, System Sciences, 1993, IEEE Proceeding of the Twenty-Sixth Hawaii International Conference, 1, January 1993, 329-338.
• [14] Josephs, M. B., Udding, J. T., Yantchev, J. T.: Handshake Algebra, Technical Report SBU-CISM-93-1, School of Computing, Information Systems and Mathematics, South Bank University, London, December 1993.
• [15] Kapoor, H. K., Josephs, M. B.: Decomposing Specifications with Concurrent Outputs to Resolve State Coding Conflicts in Asynchronous Logic Synthesis, Proceedings of the 41st Design Automation Conference (DAC), ACM, June 2004, 830-833.
• [16] Kapoor, H. K., Josephs, M. B.: Controllable Delay-Insensitive Processes and their Reflection, Interaction and Factorisation, Proceedings of the 5th International Conference on Application of Concurrency to System Design (ACSD), IEEE Computer Society, 2005, 58-67.
• [17] Kessels, J., van Berkel, K., Burgess, R., Roncken, M., Schalij, F.: An Error Decoder for the Compact Disc Player as an example of VLSI Programming, Proceedings of European Conference on Design Automation (EDAC), IEEE Computer Society, 1992, 69-75.
• [18] Li, Y., Wonham, W. M.: Control of Vector Discrete-Event Systems I - The Base Model, IEEE Transactions on Automatic Control, 38(8), August 1993, 1214-1227.
• [19] Lucassen, P. G.: A Denotational Model and Composition Theorems for a Calculus of Delay-Insensitive Specifications, Ph.D. Thesis, Dept. of C.S., Univ. of Groningen, The Netherlands, May 1994.
• [20] Mallon, W. C.: On Directed Transformations of Delay-Insensitive Specifications, Alternations and Dynamic Nondeterminism, Sixth International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society, 2000, 12-22.
• [21] Mallon, W. C.: Theories and Tools for the Design of Delay-Insensitive Communicating Processes, Ph.D. Thesis, Dept. of C.S., Univ. of Groningen, The Netherlands, January 2000.
• [22] Mallon,W. C., Udding, J. T.: Building Finite Automata from DI Specifications, Fourth International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society, 1998, 184-193.
• [23] Mallon, W. C., Udding, J. T., Verhoeff, T.: Analysis and Applications of the XDI Model, Proceedings of the Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC), IEEE Computer Society, 1999, 231-242.
• [24] Martin, A. J., Burns, S. M., Lee, T. K., Borkovic, D., Hazewindus, P. J.: The Design of an Asynchronous Microprocessor, Proceedings of Decennial Caltech Conference on VLSI, MIT Press, 1989, 351-373.
• [25] Molnar, C. E., Fang, T. P., Rosenberger, F. U.: Synthesis of Delay-Insensitive Modules, in: Chapel Hill Conference on Very Large Scale Integration (H. Fuchs, Ed.), Computer Science Press, 1985, 67-86.
• [26] Nowick, S. M., Yun, K. Y., Dill, D. L.: Practical Asynchronous Controller Design, International Conference on Computer Design, ICCD, IEEE Computer Society, October 1992, 341-345.
• [27] Peng, H., Mokhtari, Y., Tahar, S.: Environment Synthesis for Compositional Model Checking, Proceedings of International Conference on Computer Design: ICCD, IEEE Computer Society, September 2002, pp.70.
• [28] Ramadge, P. J. G., Wonham, W. M.: Supervisory Control of a class of Discrete-Event Processes, SIAM Journal of Control and Optimization, 25(1), 1987, 206-230.
• [29] Ramadge, P. J. G.,Wonham,W. M.: The Control of Discrete Event Systems, Proceedings of the IEEE, 77(1), January 1989, 81-98.
• [30] Su, R., Wonham, W. M.: Supervisor Reduction for Discrete-Event Systems, Journal of Discrete Event Dynamic Systems, 14(1), January 2004, 31-53.
• [31] Udding, J. T.: A Formal Model for Defining and Classifying Delay-Insensitive Circuits, Distributed Computing, 1(4), 1986, 197-204.
• [32] Vaz, A. F., Wonham, W. M.: On Supervisor Reduction in Discrete Event Systems, International Journal of Control, 44(2), August 1986, 474-491.
• [33] Verhoeff, T.: Encyclopedia of Delay-Insensitive Systems (EDIS), http://edis.win.tue.nl/edis.html.
• [34] Verhoeff, T.: A Theory of Delay-Insensitive Systems, Ph.D. Thesis, Dept. ofMath. and C.S., Eindhoven Univ. of Technology,May 1994.
• [35] Yakovlev, A. V.: Structural Technique for Fault-Masking in Asynchronous Interfaces, IEE Proceedings (Computers and Digital Techniques), 140(2),March 1993, 81-91.
• [36] Yun, K. Y., Dill, D. L.: Automatic Synthesis of 3D Asynchronous Controllers, International Conference on Computer-Aided Design, ICCAD, IEEE Computer Society, November 1992, 576-580.
• [37] Yun, K. Y., Dill, D. L.: A High-Performance Asynchronous SCSI Controller, International Conference on Computer Design, ICCD, IEEE Computer Society, October 1995, 44-49.