Database of Case Studies Achieved Using CADP

Blitter Display

Organisation: INRIA Grenoble - Rhône-Alpes / VASY project-team and
STMicroelectronics (FRANCE)

Method: LOTOS
SystemC/TLM

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: 2008-2009

Size: 920 lines of LOTOS, 5,500 lines of SystemC/TLM, and 2,250 lines of C

Description: In the context of the MULTIVAL project, the VASY team studied whether the CADP tools could enrich with formal verification capabilities the current design flow of STMicroelectronics, which is based on SystemC/TLM. To this aim, STMicroelectronics provided the Blitter Display (BDisp for short), a 2D-graphics co-processor implementing BLIT (Block Image Transfer) and numerous graphical operators, such as rotations, alpha blending, or Blue Ray disc decoding. The BDisp is software-controlled through instructions written in nodes of up to four application queues and two real-time composition queues. It is described by more than 25,000 lines of SystemC/Tlm code.

First, to palliate the absence of the STMicroelectronics in-house development environment, VASY designed a minimal testbench, and was able to recompile the BDisp and pass all of the required tests within our own build environment. The next step was to obtain a LOTOS model of the BDisp. This was not immediate, because the SystemC/TLM model of the BDisp is mostly sequential and data-intensive, and because it is not primarily tailored to formal verification. For this reason, the effort was focused initially on the queue management part, which is responsible for triggering and ordering the execution of the queues according to their priorities. The queue management part was isolated from the rest (graphical data treatment) and the asynchronous concurrency that actually exists in the transactions between the BDisp and its environment was explicited.

The translation from SystemC/TLM to LOTOS was done manually, but according to systematic rules [Ponsini-Serwe-08]. The SystemC/TLM code modeling input/output communications and concurrency was translated to LOTOS (920 lines of LOTOS code), while the rest of the code (5,500 lines of plain C++ code) was kept unmodified and invoked from the LOTOS model via a newly developed interface (2,250 lines of C code). This novel, hybrid approach reuses large parts of the original SystemC/TLM model (so that the model under verification remains close to the original one) and leads to good performance using the CADP tools. After assembling all these code fragments together, an executable LOTOS/C++ model of the BDisp was obtained. The OCIS interactive simulator of CADP was used to perform step-by-step simulation, and the EVALUATOR model checker was used to prove correctness properties on several verification scenarios.

Conclusions: The novel approach proposed for applying model checking to SystemC/TLM models makes it possible to reuse a large part of the C++ code present in these models, while the remaining part of the SystemC/TLM code is translated into LOTOS according to the systematic rules of [Ponsini-Serwe-08], and subsequently verified using the CADP tools. Contrary to other approaches, the new approach avoids the complete translation of the SystemC/TLM model into the particular input language of the model checker considered. Thus, formal verification is better integrated in the design flow, the translation effort is reduced, and the confidence in the results is increased.

Publications: [Ponsini-Serwe-08] Olivier Ponsini and Wendelin Serwe. "A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS". Proceedings of the 15th International Symposium on Formal Methods FM'08, Lecture Notes in Computer Science vol. 5014, pages 278-293. Springer Verlag, May 2008.
Available on-line from http://cadp.inria.fr/publications/Ponsini-Serwe-08.html

[Garavel-Helmstetter-Ponsini-Serwe-09] Hubert Garavel, Claude Helmstetter, Olivier Ponsini, and Wendelin Serwe. "Verification of an Industrial SystemC/TLM Model using LOTOS and CADP". Proceedings of the 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2009, IEEE Computer Society Press, June 2009.
Available on-line from http://cadp.inria.fr/publications/Garavel-Helmstetter-Ponsini-Serwe-09.html
Contact:
Wendelin Serwe
INRIA Grenoble - Rhône-Alpes / VASY project-team
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
Email: Wendelin.Serwe@inria.fr
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page