Model Checking for Systems on Chip (SoC).

Organisation:	ISIMA/LIMOS and STMicroelectronics (FRANCE)
Functionality:	Translation from SoC architectural descriptions to LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2003
Description:	Nowadays, most System on Chip (SoC) architectures are built around a system bus, and consist of several complex blocks providing a high level of communication and programmability. Consequently, the communication engine of a SoC becomes complex (increased number of transactions between blocks and asynchronism at system level), making functional verification the most costly and critical activity in the design process. Therefore, formal methods, assisted by verification tools, are introduced since the early design phases. This work proposes an approach for deadlock detection in SoC architectures. The approach consists in translating a high-level SoC description into a LOTOS specification, which is subsequently analysed using the CADP toolbox. The choice of LOTOS as formal language to perform verification was motivated by its capability of representing the SoC communication infrastructure accurately, in particular by preserving deadlocks. This cannot be achieved using other formal description techniques such as SDL, which (due to the semantics of communication) does not respect the fine-grained atomicity of receive, compute, and send actions associated to a communication medium. The appropriate level of abstraction is TLM (Transaction Level Management), which can be represented in LOTOS precisely by using processes to specify both the individual blocks and the interconnection mechanisms (e.g., FIFO queues) with their associated communication protocols. The approach proposed was applied to the design of SoC based on STBus, an STMicroelectronics proprietary on chip bus protocol. STBus is dedicated to SoC designed for high bandwidth applications such as audio/video processing. The components interconnected by an STBus are either initiators (which initiate transactions on the bus by sending requests), or targets (which respond to requests). The bus architecture is decomposed in nodes (sub-buses in which initiators and targets can communicate directly), internode communications being performed through FIFO buffers. The example considered was a SoC for a Set Top Box application designed using STBus. The LOTOS code generator, implemented in C++, takes as input a structural description of a SoC architecture based on STBus, consisting of the identification of the nodes, the protocol associated to each node, the identification of initiators and targets, all possible internode communications, and the sizes of the associated buffers. Standard STBus components (buffers, converters, etc.) are specified as instances of generic, predefined LOTOS processes. Individual nodes of an STBus SoC are translated in LOTOS in two different ways: in channel-oriented models explicit communication media (e.g., arbiters) are introduced between the initiator and target components of a node, whereas in system-oriented models initiator and target components are connected directly. The global SoC architecture is specified by introducing internode FIFO buffers (built from two independent FIFO buffers handling requests and responses) between the initiators and targets of different nodes. The LOTOS code generator consists of two parts: code generator for the top-level SoC architectural description and code generator for individual processes described at TLM level (currently under development). The LOTOS specification produced from the Set Top Box architecture was analysed by simulation and model checking using CADP. The complete LOTOS specification was obtained by instantiating the initiators and targets with arbitrary LOTOS processes. This allowed to validate both the LOTOS code generator and the models of generic STBus components (internode buffers, converters, etc.).
Conclusions:	The approach proposed shows the benefits of using LOTOS and the CADP toolbox for deadlock detection in SoC architectures designed using STBus. Future work regards the translation in LOTOS of SoC components described at TLM level using e.g., SystemC.
Publications:	[Wodey-Camarroque-Baray-et-al-03] Pierre Wodey, Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, and Jean-Philippe Cousin. "LOTOS Code Generation for Model Checking of STBus Based SoC: The STBus Interconnect". In Rajesh K. Gupta, Sandeep Shukla, and Jean-Pierre Talpin, editors, Proceedings of the 1st ACM and IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'03 (Mont Saint-Michel, France), pp. 204-213, June 2003. Available from the CADP Web site in PDF or PostScript
Contact:	Pierre Wodey ISIMA BP 10125 F-63173 Aubière Cedex FRANCE Tel: +33 (0)4 73 40 50 12 Fax: +33 (0)4 73 40 50 01 E-mail: Pierre.Wodey@isima.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software The verification of the STBus Interconnect is presented on the following Web Page: http://cadp.inria.fr/case-studies/03-k-stbus.html

Back to the CADP research tools page