Specification and Verification of Synchronous Hardware using LOTOS.

Organisation:	University of Stirling (SCOTLAND)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design.
Period:	1999.
Size:	about 17500 lines of LOTOS and m4 (DILL library and examples) 260 lines of LOTOS (the two benchmarks in this case-study)
Description:	DILL (Digital Logic In LOTOS) is an approach, developed over five years, to allow formal specification of digital hardware using LOTOS at various levels of abstraction. DILL offers a rigorous specification method, accompanied by a higher-level library of typical components and by several tools. The general approach of modelling hardware in DILL consists of encoding a schematic circuit as a LOTOS behaviour expression, by using a library of simple hardware components (logic gates, latches, counters, registers, etc.). Circuits (including library components) can be specified in DILL both behaviourally (at different abstraction levels) and structurally (by integrating all their sub-components). The use of DILL in conjunction with CADP is illustrated by means of two benchmark hardware designs: a single pulser and a bus arbiter. Both benchmarks have been specified in DILL and then analysed using the ALDEBARAN equivalence/preorder checker and the XTL temporal logic model-checker of CADP. For the single pulser, the corresponding LTS model has been generated with CAESAR, then minimized using ALDEBARAN and checked to be deadlock free. Moreover, 4 correctness properties have been expressed as ACTL formulas and verified on the LTS model using XTL. For the bus arbiter, a higher-level specification of the arbitration algorithm was developed directly in LOTOS. Using CAESAR and ALDEBARAN, this specification has been translated into a minimized LTS, on which 3 temporal properties encoded as ACTL formulas have been verified using XTL. To circumvent state explosion, the LTS model of the lower-level DILL specification has been generated compositionally using CAESAR and ALDEBARAN and the 3 properties have been checked using XTL. Moreover, using ALDEBARAN, it was found that the LOTOS and DILL specifications were not observationally equivalent, which (after step-by-step simulation of the error trace produced by ALDEBARAN) uncovered an error in the design. The error has been corrected, leading to a more robust design of the bus arbiter.
Conclusions:	By using LOTOS, DILL enherits the well-developed theory of process algebras, thus being more suitable for analysis than other semi-formal hardware description languages such as VHDL, Verilog or ELLA. Moreover, compared to other hardware description languages with formal semantics such as CIRCAL, DILL benefits from the expressiveness of the LOTOS data types, the abstraction mechanisms, and the state-of-the-art verification features provided by toolsets such as CADP.
Publications:	[He-Turner-99-a] Ji He and Kenneth J. Turner. "Modelling and Verifying Synchronous Circuits in Dill." Technical Report CSM-152, Department of Computing Science and Mathematics, University of Stirling, Scotland, April 1999. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/staff/kjt/research/pubs/sync-dill.ps.gz or also from the CADP Web site in PDF or PostScript [He-Turner-99-b] Ji He and Kenneth J. Turner. "Specification and Verification of Synchronous Hardware using LOTOS". In Jianping Wu, Samuel T. Chanson, Quiang Gao, editors, Proceedings of Formal Methods for Protocol Engineering and Distributed Systems (FORTE XII/PSTV XIX), pages 295-312, Kluwer Academic Publishers, London, UK, October 1999. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/staff/kjt/research/pubs/sync-lot.ps.gz or also from the CADP Web site in PDF or PostScript
Contact:	Prof. Kenneth J. Turner Room 4B78, Computing Science and Mathematics University of Stirling Stirling FK9 4LA Scotland Tel: +44 1786 467 420 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