LOTOS code generation for model checking of STBus based SoC: the STBus interconnection
P. Wodey, G. Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Gabriel Cousin · International Conference on Formal Methods and Models for Co-Design · 2003
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 behavior 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 formula, either on-the-fly or after the generation of a labeled transition system (LTS). The automatic LOTOS code generation is decomposed in two parts, the code generation of the processes behavior (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.