LIMOS laboratory, Aubiere (FRANCE)
Advanced Systems Technology, STMicroelectronics, Grenoble (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
System on Chip.
This case study describes the validation of industrial SoC (System on
Chip) designs at the system level. In order to deal with the
complexity of a complete SoC, the approach consists in introducing
verification at a high level at the beginning of the design process
using formal description techniques, such as LOTOS, instead of
undertaking verification on the RTL level very late in the design
process. Since the communication engine is arguably the most
error-prone area, special focus is given to the verification of
communication protocols and absence of deadlocks.
The approach is illustrated by the STBus bus protocol developed by STMicroelectronics and dedicated to high bandwidth SoCs for applications such as audio/video processing. An STBus connects initiator components (which send requests) to targets (which respond to requests). The bus architecture is decomposed in nodes or sub-buses, inter-node communication being performed through FIFO buffers.
Two different possibilities for modeling STBus in LOTOS are considered, namely the system-oriented model, where initiators and targets synchronise directly, and the channel-oriented model, where each channel is modeled by a separate process. The case study shows that the system-oriented model yields state spaces about an order of magnitude smaller than channel-oriented models, while preserving the interesting properties at the system level.
A tool has been developed that for a structural description of an STBus interconnect automatically generates the corresponding (system-oriented) LOTOS model. This generator has been validated using CADP (by means of simulation and verification of temporal logic formulae) of the state spaces generated for different kinds of interconnects and arbitrary initiators and targets.
The case study shows that LOTOS models at the transaction level are
suitable for the verification of interesting properties of a system
interconnect, such as absence of deadlocks. Furthermore, the use of
CADP for the verification of a Set Top Box application using the STBus
interconnect allowed to discover an error in the design.
The authors of the case study also give an example that shows
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 AUBIERE Cedex
Tel: +(33) 4 73 40 50 12
Fax: +(33) 4 73 40 50 01
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies The tool for automatic generation of LOTOS models is described on the following Web Page: http://cadp.inria.fr/software/03-a-stbus.html|