ISIMA/LIMOS and STMicroelectronics (FRANCE)
Translation from SoC architectural descriptions to LOTOS
CADP (Construction and Analysis of Distributed Processes)
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.).
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.
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,
Available from our FTP site in PDF or PostScript
F-63173 Aubière Cedex
Tel: +33 (0)4 73 40 50 12
Fax: +33 (0)4 73 40 50 01
|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|