On Process-algebraic Verification of Asynchronous Circuits

• Autorzy: Wang X. , Kwiatkowska M.
• Języki publikacji: EN

Abstrakty

EN

Asynchronous circuits have received much attention recently due to their potential for energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis of asynchronous circuits. This paper develops a theoretical basis for using process algebra and associated model checking tools to verify asynchronous circuits. We formulate a model that extends existing verification theory for asynchronous circuits, and integrate it into the framework of standard process algebra theory. Our theory permits analysis of safeness (i.e. choke) and progress (i.e. illegal stop, divergence and relative starvation) conditions. We show how the model can be translated into CSP, and how the satisfaction of safeness and progress requirements can be reduced to refinement checks in CSP. Finally, the correspondence of our theory with trace theory (i.e. prefix-closed trace structures), receptive process theory and the XDI model is investigated.

Słowa kluczowe

EN

process algebras; asynchronous circuitis; assume/guarantee verification; progress/liveness; CSP/FDR2

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 283--310
• Opis fizyczny: bibliogr. 31 poz.

Twórcy

autor

Wang X.

autor

Kwiatkowska M.

• Oxford University Computing laboratory, Parks Road, Oxford OXI 3QD, UK,

Bibliografia

• [1] K. van Berkel. Handshake circuits - an Asynchronous Architecture for VLSI Programming. CUP, 1993.
• [2] T. A. Chu. Synthesis of Self-Timed VLSI Circuits from Graph-Theoretic Specifications. PhD thesis, MIT, 1987.
• [3] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno and A. Yakovlev. Logic Synthesis of Asynchronous Controllers and Interfaces. Springer-Verlag, 2002.
• [4] A. Davis and S. M. Norwick. An Introduction to Asynchronous Circuit Design. In The Encyclopedia of Computer Science and Technology: Volume 38, A. Kent and J. Williams, eds. Marcel Dekker, 1998.
• [5] D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-IndependentCircuits. MIT Press, 1988.
• [6] D. Edwards and A. Bardsley. Balsa: An Asynchronous Hardware System. In Principles of Asynchronous Circuit Design, Part II, J. Sparso and S. Furber, eds. Springer, 2002.
• [7] Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, 1999.
• [8] J. He and K. J. Turner. Verifying and Testing Asynchronous Circuits using LOTOS. FORTE XIII/PSTV XX, pp 267-283. Kluwer, 2000.
• [9] M. B. Josephs. An Analysis of Determinacy Using a Trace-Theoretic Model of Asynchronous Circuits. ASYNC 2003: 121-131, IEEE CS Press, 2003.
• [10] M. B. Josephs. Receptive Process Theory. Acta Informatica 29(1):17-31, 1992.
• [11] H. K. Kapoor and M. B. Josephs. Modelling and verification of delay-insensitive circuits using CCS and the concurrency workbench. Information Processing Letters 89(6):293-296, 2004.
• [12] V. Khomenko and M. Koutny. Towards an Efficient Algorithm for Unfolding Petri Nets. CONCUR 2001, LNCS 2154, pp. 366-380, Springer, 2001.
• [13] Y. Liu. Amulet1: Specification and verification in CCS. PhD thesis, University of Calgary, Canada, 1996
• [14] W. C. Mallon, J. T. Udding and T. Verhoeff. Analysis and Applications of the XDI model. ASYNC 1999: 231-242, IEEE CS Press, 1999.
• [15] A. Mazurkiewicz. Trace Theory. Advances in Petri Nets, LNCS 255. Springer, 1987.
• [16] K. L. McMillan. Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195, LNCS 939, Springer, 1995.
• [17] R. Negulescu. Process spaces. CONCUR 2000: 199-213, Springer, 2000.
• [18] R. Negulescu. Process Spaces and Formal Verification of Asynchronous Circuits. PhD Thesis, University of Waterloo, Canada, 1998.
• [19] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1998.
• [20] A. W. Roscoe. Seeing beyond divergence. 25 Years Communicating Sequential Processes 2004: 15-35, LNCS 3525. Springer, 2004.
• [21] A. Semenov. Verification and Synthesis of Asynchronous Control Circuits using Petri Net Unfoldings. PhD Thesis, University of Newcastle upon Tyne, July 1997.
• [22] M.W. Shields. Semantics of Parallelism: Noninterleaving Representation of Behaviour. Springer, 1997.
• [23] K. Stevens. Practical Verification And Synthesis Of Low Latency Asynchronous Systems. PhD Thesis, University of Calgary, 1994.
• [24] T. Verhoeff. Analyzing Specifications for Delay-Insensitive Circuits. ASYNC 1998: 172-183, IEEE CS Press, 1998.
• [25] T. Verhoeff. A Theory of Delay-Insensitive Systems. Dissertation, Eindhoven University of Technology, May 1994.
• [26] X. Wang, M. Kwiatkowska, G. Theodoropoulos and Q. Zhang. Towards a unifying CSP approach for hierarchical verification of asynchronous hardware. AVOCS 2004, ENTCS 128(6): 231-246, Elsevier, 2004.
• [27] X. Wang, M. Kwiatkowska, G. Theodoropoulos and Q. Zhang. Opportunities and challenges in processalgebraic verification of asynchronous circuit designs. FMGALS 2005, ENTCS 146(2): 189-206, Elsevier, 2006.
• [28] X. Wang and M. Kwiatkowska. On process-algebraic verification of asynchronous circuits. ACSD 2006: 37-46. IEEE CS Press, 2006.
• [29] X. Wang and M. Kwiatkowska. Compositional state space reduction using untangled actions. EXPRESS 2006, ENTCS 175(3): 27-46, Elsevier, 2007.
• [30] M. Nielsen, G. Plotkin and G. Winskel. Petri Nets, Event Structures and Domains: Part I. Theor. Comput. Sci. 13(1), 1981.
• [31] A. Yakovlev, M. Kishinevsky, A. Kondratyev, L. Lavagno and M. Pietkiewicz-Koutny. On the Models for Asynchronous Circuit Behaviour with OR Causality. FMSD 9(3): 189-234, 1996.