Database of Case Studies Achieved Using CADP

Formal Analysis and Co-simulation of a Dynamic Task Dispatcher

Organisation: INRIA Rhône-Alpes / VASY, Grenoble (FRANCE)
STMicroelectronics

Method: LNT

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

Domain: Hardware Design.

Period: 2011-2013

Size: 155,616,354 states and 825,243,444 transitions.

Description: Multi-media applications require complex multiprocessor architectures, even for mobile terminals such as smartphones or netbooks. Due to physical constraints, in particular the distribution of a global clock on large circuits, modern multiprocessor architectures for mobile multi-media applications are implemented using a globally asynchronous, locally synchronous (GALS) approach, combining a set of synchronous blocks using an asynchronous communication scheme. Due to the high cost of chip-fabrication, errors in the architecture have to be found as early as possible. Therefore, architects are interested in applying formal methods in the design phase. In addition, a formal model has to take into account both hardware and software, because a part of the system's functionality is implemented in software to provide the flexibility required by the rapidly evolving market. However, even if the software part can be updated easily, the basic functionalities implemented in hardware have to be thoroughly verified.

This case-study illustrates the application of CADP for the formal modeling and verification of a hardware block of an industrial architecture developed by STMicroelectronics, namely the Dynamic Task Dispatcher (DTD). The DTD serves to dispatch data-intensive applications on a cluster of processors for parallel execution. Given that the considered design is a GALS architecture, the interfaces between the processors and the DTD can be considered asynchronous. Processors may have different extensions, e.g., to (re-)align bitstreams to word boundaries or to perform vector operations. Similarly, tasks may be annotated with information about a required processor extension; in this case, the DTD has to assign the task to a processor with the required extension.

After modeling the DTD in LNT, the CADP toolbox was used to generate the LTSs corresponding to 19 scenarios each for four, six, and eight processors. Three variants of the model were considered: the original unconstrained model, a constrained model where all processors are forced to boot before the handling of the first task, and a model where some processors might never boot. These constraints were enforced taking advantage of the constraint-oriented specification style of LNT.

Five correctness properties were expressed in MCL and verified using the EVALUATOR 4.0 model checker of CADP. For some properties and some scenarios, these verifications generated counterexamples illustrating the possibility of a livelock under heavy application load.

The DTD has been designed by the architect directly as a C++ model suitable for high level synthesis tools. To investigate the issue discovered by model checking, the EXEC/CAESAR framework was used to experiment with the co-simulation of the C++ and LNT models, using a configuration of the DTD involving 16 processors. Unfortunately, although this revealed that the C++ model did not behave correctly for some particular scenarios, the issues could not be fully investigated, because the architecture has been redefined and the DTD has been discarded.

Conclusions: Developing a formal model of the DTD in LNT proved to be practically feasible. The LNT model is easily understandable by architects and can serve as a basis for trying alternate designs, i.e., for experimenting with complex performance optimizations that would otherwise be discarded as too risky. The automatic analysis capabilities offered by CADP (e.g., step-by-step simulation, model checking, co-simulation) helped to pinpoint subtle issues in the architecture.

Publications: [Lantreibecq-Serwe-11] Etienne Lantreibecq and Wendelin Serwe. "Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP". Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2011 (Trento, Italy), Lecture Notes in Computer Science vol. 6959, pages 180-195. Springer Verlag, August 2011.
Available on-line from
http://cadp.inria.fr/publications/Lantreibecq-Serwe-11.html

[Lantreibecq-Serwe-14] Etienne Lantreibecq and Wendelin Serwe. "Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP". Science of Computer Programming, volume 80, pages 130-149, 2014.
Available on-line from
http://cadp.inria.fr/publications/Lantreibecq-Serwe-14.html
or from:
http://dx.doi.org/10.1016/j.scico.2013.01.003
Contact:
Wendelin Serwe
INRIA Rhône-Alpes / VASY
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