Project Web Page: http://www.eee.kcl.ac.uk/~comfort/

Principal Investigators:

Prof. A.C. Davies King's College London tonydavies@kcl.ac.uk

Dr. S.A. Velastin King's College London

Dr A.V.Yakovlev Newcastle University Alex.Yakovlev@ncl.ac.uk

Dr A.M.Koelmans Newcastle University

Prof. D.J.Kinniment Newcastle University

Grant Refs: King's College London GR/L92471, Newcastle University GR/L93775

Start date: King's College London 01.04.98, Newcastle University 17.05.98

Duration : 36 months

1. Advancement in formal modelling and analysis of asynchronous communication mechanisms (ACMs) for real-time systems.

2. Development of methods and software for synthesis and verification of hardware implementations for ACMs.

3. Assessment of the effect of physical parameters, such as delays and metastability on the functionality of ACMs.

4. A case study in a safety critical application of asynchronous communications and/or demonstrator

1.1. New models of ACMs and their basic properties, such as coherence and freshness (timeliness) have been developed [1,2]. These models are based on the rigorous syntax and semantics of Petri nets. They

complement the previously known Simpson's role models that were built specially for a four-slot ACM, and address the issue of the genericity of modelling and analysis of ACMs by exploiting the analytic power of Petri net based techniques. Both reachability and partial order methods can be used to verify Petri net descriptions of ACMs at different levels of abstraction.

1.2. Initial work in this area concentrated on an extensive literature search. This identified existing published material, and gave insight in to terms and naming conventions otherwise unknown. The initial results expanded searching from asynchronous communications to include wait free communication, atomic communication, and snapshots etc. From these searches an online bibliography has been constructed, and is available on the WWW from the COMFORT web page.

It was apparent from the publications found that the majority of solutions had come from authors working in computer science departments, and in most cases no contribution had been made by any electronic engineering departments. This has the side effect that most solutions found ignore

the phenomenon of metastability, which is the major cause of algorithm failure during asynchronous operation, and must be a major concern to the operational correctness of many of the published solutions.

Metastability being such a big concern in this work, meant a second literature search in this field was necessary, and a second bibliography constructed and made available on the WWW, again available from

the COMFORT web page.

2.1. New algorithms and software for the Petri-net based verification of ACMs have been developed.

The nature of ACMs and the environments they are used dictate the way in which PN models are produced and the software used to analyse these models. ACMs are used in a cyclic environment, typically, {loop - produce data - write data - end loop} or {loop - read data - used data - end loop}.

This means that many PN analysis tools get stuck in infinite loops when generating the reachability tree. This means that a list of previously visited states needs to be maintained. Data coherence, data freshness and data sequencing are the properties implemented in PNs including timing constraints to allow certain

mechanisms to operate in non-true asynchronous ways. This helps to determine which parts of a particular algorithm are the cause of a failure of the above mentioned properties. Certain characteristics of the data freshness testing method have been observed and are under further investigation.

2.2. Stochastic techniques for the analysis of the quantified properties of ACMs (asynchrony, coherence, freshness, sequencing) based on Markov chains and stochastic process algebras (TIPP-tool) have been investigated [3]. Further work, involving modelling and analysis with stochastic Petri nets is under way.

2.3. Self-timed hardware implementations for two types of ACMs have been synthesized. The first one, a non-blocking FIFO, presents an ACM that can store data between the reader and the writer guaranteeing full coherence and sequencing [4,5]. The second one, a self-timed circuit for a four-slot ACM fulfils the main coherence and freshness criteria of the original Simpson's method [6,7]. Additionally, it provides a completely hazard-free solution in which metastability is completely resolved within special mutex devices, that protect the critical sections in accessing the binary control variables, implemented as self-timed latches. The circuit guarantees practically bounded reaction time and thus can be used in the real-time (wait-free) communication environment. Both implementations are suitable as generic asynchronous interface methods for intermodule communication on chips with 1 billion transistor VLSI technology of the next decade. Some parts of control logic in these circuits have been synthesised using software tool Petrify [8] (which takes an interpreted Petri net as an initial specification of a circuit).

3. New models for metastable behaviour of multi-stable devices (sometimes used to construct multi-way mutexes and arbiters) have been developed and analysed [9,10]. By using simple and idealised gate-models, the non-linear differential equations can easily be solved numerically and the trajectories displayed, giving a visual indication of the dynamic behaviour, and providing added insight into many qualititative aspects of the behaviour of multi-way arbiters and other building blocks subject to metastable behaviour.

4. A preliminary discussion of a demonstrator of ACMs has been carried out. Potential application domains have been identified, such as asynchronous interfacing for real-time systems and for 1 billion transistor VLSI technology. A specification of the ACM demonstrator has been prepared.

Continued collaboration in the area of Petri net modelling, analysis and synthesis of asynchronous control circuits, with Polytechnic of Turin (Italy), Polytechnic University of Catalunya (Spain), University of Aizu (Japan), and within the UK Asynchronous Design community (particularly with

Universities of Manchester, Edinburgh and South Bank) and with the ESPRIT-funded ACiD-WG Working Group on Asynchronous Circuit Design. Further collaboration started with Matra/BAe Dynamics on a number of topics related to Petri net modelling of asynchronous communication mechanisms, Butler technology, asynchronous circuit synthesis and design of devices with metastability. There have been two meetings at BAe (Stevenage and Bristol) and one meeting with E. Campbell (Matra/BAe Dynamics) at Newcastle.

An application for a new EPSRC project on visualisation support for asynchronous circuit synthesis, which will directly benefit from the COMFORT work has been prepared at Newcastle. A collaborative project on generic methods for the automatic synthesis of concurrent systems, involving the synthesis of ACMs as its important application, has been proposed for Framework 5.

The results of COMFORT work have been widely publicised. The work has been presented at two Async UK forums. The COMFORT project meeting held at Newcastle in January 1999 was part of the Third ACiD-WG workshop and attracted interest of the workshop attendees. The COMFORT project has been represented at both international workshops on Hardware Design and Petri Nets (1998, 1999) held in Lisbon and Williamsburg [11,12].

[1] Fei Xia and Ian Clark, Complementing role models with Petri nets in studying asynchronous data communications, Proc. First Int. Workshop on Hardware Design and Petri Nets (HWPN'98), Lisbon, June 1998, pp. 66-85 (accepted for publication in a book "Hardware Design and Petri Nets", to be published by Kluwer AP in 2000)

[2] Fei Xia, Ian Clark, Complementing the role model method with Petri Net techniques in studying issues of data freshness of the four-slot mechanism, Technical Report No. 654, Department of Computing Science, University of Newcastle upon Tyne, Newcastle, UK. October 1998.

[3] Fei Xia and Bin Liu. Quantitative investigation of certain properties of slot mechanisms. Proc. of 5th UK Asynchronous Forum, Computer Laboratory, University of Cambridge, December 1998.

[4] A. Yakovlev, D.J. Kinniment, F. Xia and A.M. Koelmans. A FIFO buffer with non-blocking interface. Proc. of 5th UK Asynchronous Forum, Computer Laboratory, University of Cambridge, December 1998.

[5] A. Yakovlev, D.J. Kinniment, F. Xia and A.M. Koelmans. A FIFO buffer with non-blocking interface. IEEE Computer Society TCVLSI Technical Bulletin, Fall 1998, pp. 11-14.

[6] F. Xia, D. Shang, A. Yakovlev, A. Koelmans. An Asynchronous Communication Mechanism using self-timed circuits, 6th UK Asynchronous Forum, University of Manchester, 12-13th July 1999.

[7] A. Bystrov, D. Shang, F. Xia, A. Yakovlev. Self-timed and speed independent latch circuits, 6th UK Asynchronous Forum, University of Manchester, 12-13th July 1999.

[8] A. Kondratyev, J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev. Logic decomposition of speed-independent circuits (invited paper). Proceedings of IEEE, vol. 87, no.2, pp. 347-362, Feb. 1999.

[9] A. C. Davies. Metastability in Latches, Arbiters and Data-Convertors. Invited Paper, IEEE International Symposium on Signals, Circuits and Systems (SCS'99), pp1-4, Iasi, Romania, July 6-7 1999.

[10] A. C. Davies. Multi-Flops - A View of the Dynamical Behaviour, 7th International Specialist Workshop on NonLinear Dynamics of Electronic Systems (NDES'99), pp133-136, Rønne, Island of Bornholm, Denmark, 15-17th July 1999.

[11] A. Yakovlev and L. Gomes (Eds.) Proceedings of the ICATPN'98 Workshop on Hardware Design and Petri Nets, (HWPN'98), June 1998, Lisbon.

[12] A. Yakovlev and L. Lavagno (Eds.) Proceedings of the ICATPN'99 Workshop on Hardware Design and Petri Nets (HWPN'99), June 1999, Williamsburg.