loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)
LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect
Mont Saint-Michel, France
June 24-June 26
ISBN: 0-7695-1923-7
Pierre Wodey, ISIMA - LIMOS
Geoffrey Camarroque, ISIMA - LIMOS
Fabrice Baray, ISIMA - LIMOS
Richard Hersemeule, STMicrolectronics
Jean-Philippe Cousin, STMicrolectronics
In the design process of SoC (System on Chip), validation is one of the most critical and costly activity. The main problem for industrial companies like STMicroelectronics, stands in validation at the complete system level. At this level, the properties to verify concern the well behaviour composed of the different processes interconnected around the system bus. In our work we consider the deadlock-free property. In this paper we present an approach for deadlock detection consisting in generating automatically a LOTOS description of the system. Then, by using CADP toolbox developed at INRIA by the VASY team, the LOTOS description can then be used for the evaluation of temporal logic formul?, either on-the-fly or after the generation of a Labelled Transition System (LTS). The automatic LOTOS code generation is decomposed in two parts, the code generation of the processes behaviour (work under progress) and the code generation for the interconnection of processes on a given SoC bus. This paper presents the principles of interconnect abstraction showing that deadlock detection has to take into account properties of the implemented communication channel, avoiding the possibility to build a general deadlock detection tool. The resulting principles are then applied on the STMicroelectronics proprietary SoC bus, the STBus, leading in the development of the LOTOS code generation software.
Citation:
Pierre Wodey, Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Philippe Cousin, "LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect," memocode, pp.204, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003
Usage of this product signifies your acceptance of the Terms of Use.