Test Generation and Execution for Synchronous Hardware

Organisation:	University of Stirling (SCOTLAND)
Functionality:	Automatic test generation for synchronous hardware
Tools used:	OPEN/CAESAR
Period:	1999
Description:	As modern digital circuits become extremely complex, they require substantial effort to ensure design correctness prior to manufacture. DILL (Digital Logic in LOTOS) [He-Turner-99-a] is an approach and a language for specifying digital circuits using LOTOS. Besides offering the benefits of rigorous specification and analysis using tools like CADP, this approach also opens the way for harware testing by applying the methodologies used for protocol conformance testing. The authors have extended CADP with a prototype tool for generating hardware test suites automatically starting from LOTOS specifications. The tool implements the ioconf conformance relation and has been built using the OPEN/CAESAR generic environment for on-the-fly exploration of labelled transition systems (LTSs). The test generation algorithm used is a slightly modified version of a generic algorithm proposed by Jan Tretmans for producing tests according to various implementation relations. An additional algorithm for generating tests (transition tours) that cover all transitions in an LTS has also been implemented using OPEN/CAESAR. Moreover, a testbench has been developed, which allows to execute the test suites in a VHDL simulator that handles a lower-level implementation of the circuit. The test generation tool has been used on several benchmark examples of synchronous hardware designs, such as a JK flip-flop, a Single pulser, and a Black-Jack dealer (about 120 lines of LOTOS in total). For the latter design, the tool produced a test suite that, when executed in the VHDL simulator, revealed a reset problem in a flag register of the circuit. After locating the error, the design has been corrected in order to successfully pass the test suite.
Conclusions:	The framework of formal methods in protocol testing provides a successful way for testing digital circuits. A prototype tool for generating tests from LOTOS specifications of digital circuits has been developed using the OPEN/CAESAR environment of CADP. The facilities provided by the OPEN/CAESAR programming API allow to parameterize the order in which LTS transitions are traversed, and thus to obtain a better test coverage by running the test generator several times, with different transition orderings. Moreover, when the specifications are sufficiently close to the real implementation (as was the case for the examples handled in this study), it is straightforward to map test cases to the actual implementation, because there is a one-to-one correspondence between the gates present in the LOTOS specification and the signals at the implementation level.
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-c] Ji He and Kenneth J. Turner. "Protocol-Inspired Hardware Testing." In Gyula Csopaki, Sarolta Dibuz and Katalin Tarnay, editors, Proceedings of the 12th International Working Conference on Testing of Communicating Systems WCTCS'99, pages 131-147, Kluwer Academic Publishers, London, UK, September 1999. Available on-line at: ftp://ftp.cs.stir.ac.uk/pub/staff/kjt/research/pubs/hard-test.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 tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page