LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect

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. ...

• Type: Conference
• Year: 2003
• Where: MEMOCODE
• Authors: Pierre Wodey, Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Philippe Cousin
• Keywords: Code Generation, Deadlock Detection, LOTOS Code Generation, MEMOCODE 2003