|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 |
Back to the CADP case studies page