Formal Verification of the STBus Interconnect

Organisation:	LIMOS laboratory, Aubiere (FRANCE) Advanced Systems Technology, STMicroelectronics, Grenoble (FRANCE)
Method:	LOTOS SDL
Tools used:	CADP (Construction and Analysis of Distributed Processes) STBus
Domain:	System on Chip.
Period:	2003
Size:	n/a
Description:	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.
Conclusions:	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 "the inadequation of an SDL model due to the non respect of atomicity properties in the channels."
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 LIMOS Laboratory BP 10125 F-63173 AUBIERE Cedex FRANCE Tel: +(33) 4 73 40 50 12 Fax: +(33) 4 73 40 50 01 E-mail: Pierre.Wodey@isima.fr
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

Back to the CADP case studies page