Verification and Testing of Asynchronous Circuits.

Organisation:	University of Stirling (SCOTLAND, UNITED KINGDOM)
Method:	LOTOS
Tools used:	VeriConf and TestGen (University of Stirling) CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design.
Period:	1999/2000
Size:	n/a
Description:	DILL (Digital Logic in LOTOS) is an approach, a language, and a toolset for specifying, analysing and testing digital hardware designs. An extensive library of typical hardware components and methods for dealing with synchronous (clocked) circuits has been developed. Since DILL is built on top of LOTOS, it can exploit the rich theories and tools available for this language. Recently, DILL has been extended to handle asynchronous (unclocked) circuits, which are increasingly attracting attention. These circuits operate at the speed of individual components, without artificially limiting them to some clock rate, and therefore they may be capable of faster operation than synchronous circuits. On the other hand, asynchronous circuits are much harder to design and analyse: many design strategies are available, aiming to achieve different goals, such as independence from the delays or speed of circuit elements. The challenge is to allow each component to operate as fast as possible while preserving the circuit function. The goal of extending DILL with asynchronous circuits is to perform formal verification and rigorous test derivation starting from the specifications of those circuits. A special attention is payed to speed-independent designs (having gates with unbounded delay and wires with zero delay), for which LOTOS operators are particularly suitable. A set of hardware components is thus specified using DILL and LOTOS: wires, forks, C-elements, merge components, selectors, sequencers, latches, arbiters, etc. To perform analysis of designs, the authors developed two tools using the OPEN/CAESAR environment provided by CADP: VeriConf, which checks design equivalence modulo the confor and strongconfor relations, designed by the authors in order to assess the conformance of an implementation w.r.t. its specification; and TestGen, which generates hardware test suites automatically from a DILL specification. These tools, together with CADP, have been used to verify several hardware designs, in particular a asynchronous FIFO, an or-and circuit, and a selector. Among the CADP tools, the CAESAR compiler was used to generate the LTS of the specifications, the XTL model-checker was used to verify temporal logic properties expressed in ACTL, and ALDEBARAN was used to check the observational equivalence of specifications and implementations.
Conclusions:	The DILL environment assessed that real hardware can be effectively modelled and analysed using LOTOS. The approach builds upon the well-studied theory of process algebras and underlying transition system models, and new tools are constructed using the OPEN/CAESAR environment provided by CADP. The work also constitutes a novel application of protocol design techniques (conformance testing of LOTOS specifications) to a new domain that is exciting industrial interest.
Publications:	[He-Turner-00] J. He and K.J. Turner. "Verifying and Testing Asynchronous Circuits using LOTOS". In T. Bolognesi and D. Latella, editors, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV'2000 (Pisa, Italy), pp. 267-283, Kluwer Academic Publishers, October 2000. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/staff/kjt/research/pubs/async-lot.ps.gz or from the CADP Web site in PDF or PostScript [He-00] J. He. "Formal Specification and Analysis of Digital Hardware Circuits in LOTOS". PhD thesis, Technical Report CSM-158, University of Stirling, Scotland, August 2000. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/tr/cs/2000/TR158.ps.gz or from the CADP Web site in PDF or PostScript [Turner-He-01] Kenneth J. Turner and Ji He. "Formally-Based Design Evaluation". In T. Margaria and T. Melham, editors, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods CHARME'2001 (Livingston, Scotland, UK), LNCS vol. 2144, Springer-Verlag, September 2001. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/staff/kjt/research/pubs/form-des.ps.gz or from the CADP Web site in PDF or PostScript
Contact:	Prof. Kenneth J. Turner Computing Science and Mathematics Room 4B78 University of Stirling Stirling FK9 4LA Scotland, United Kingdom Tel: +44-1786-467-423 Fax: +44-1786-464-551 Web: http://www.cs.stir.ac.uk/~kjt
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page