Télécom ParisTech, LTCI CNRS, Sophia-Antipolis (FRANCE)
LIP6, University Pierre et Marie Curie, Paris (FRANCE)
TML (Task Modelling Language)
CADP (Construction and Analysis of Distributed Processes)
173,546,709 states and 472,413,097 transitions
When designing a System-on-Chip (SoC), one has to explore huge design
spaces due to the increasing complexity of architectures and the
number of parameters. This issue can be overcome by using abstract
models and splitting the design flow into multiple levels, in order to
guide the designer in the design process, from the most abstract model
down to a synthesizable model.
This work proposes a method for assisting the process of refinement along the design flow, based on transformation rules representing concretisation steps. The transformation rules are coupled with formal verification to guarantee the preservation of stuttering linear-time properties, and hence to alleviate the verification process and facilitate the design space exploration. The approach is based on the Y-chart design scheme and focuses on data-flow applications, modelled as a set of abstract concurrent tasks.
The functional behaviour of the application is written in TML (Task Modelling Language), whose computation model extends the Kahn networks model with non-determinism and various kinds of communication. A TML model is a set of asynchronous tasks, representing the computations of the application, and communicating through channels, events, or requests. An abstract behavioral model, defined as an LTS (Labeled Transition System) is attached to each of the architectural components. This behavioral model, which is hidden to the designer, exhibits the synchronizations and resource constraints imposed by the corresponding component.
The proposed approach provides guidelines for formally refining the tasks and the communication medium (from the simple channels to concrete infrastructures). After generating the initial model, the guidelines suggest three steps: (1) refinement of data granularity; (2) refinement of channel management; (3) introduction of an abstract bus. The approach is illustrated for the design and functional verification of a digital camera. The functional specification is partitioned into five modules described in TML. The architecture consists of five processing elements equipped with local memory. The code of the LTSs in each refined model is written in FIACRE, and the property verification and refinement checking between successive levels are performed using CADP. Complete and infinite trace inclusion between lower levels and higher levels is established by proving the existence of simulation relations between two successive models, which ensures the preservation of stuttering linear-time properties. Five temporal properties were expressed in MCL and checked, using EVALUATOR 4.0, on the different models obtained after the refinement steps.
The refinement-based methodology proposed for design space exploration
of a SoC provides guidelines to assist the designer in the refinement
process, focusing on communication refinement. Each abstraction level
can be associated with a verification environment to prove functional
properties or refinement properties between different abstraction
levels. In this way, the validity of functional properties of concrete
descriptions can be established by checking a property on the most
abstract level and proving the refinement, which is less costly than
verifying the property on the concrete model directly.
Hocine Mokrani, Rabéa Ameur-Boulifa, and
"Assisting Refinement in System-on-Chip Design".
Proceedings of the 2013 Forum on Specification and Design Languages
FDL'2013 (Paris, France), pages 1-6. IEEE CS Press, September 2013.
Available on-line at: http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=06646624
[Mokrani-14] Hocine Mokrani. "Assistance au raffinement et à la vérification formels dans la conception des systèmes embarqués". PhD Thesis, TÉLÉCOM ParisTech, June 2014.
Available on-line at: https://pastel.archives-ouvertes.fr/tel-01466740
or from the CADP Web site in PDF and PostScript
[Mokrani-Boulifa-Encrenaz-15] Hocine Mokrani, Rabéa Ameur-Boulifa, and Emmanuelle Encrenaz-Tiphene. "Assisting Refinement in System-on-Chip Design". In selected contributions from FDL 2013, Lecture Notes in Electrical Engineering, vol. 311, pp. 21-42, Springer Verlag, 2015.
Available on-line at: http://doi.org/10.1007/978-3-319-06317-1_2
Inria / OASIS project-team
2004, route des Lucioles
F-06902 Sophia Antipolis
Tel: +33 (0)4 92 38 50 52
Fax: +33 (0)4 92 38 76 44
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|