Assisting Refinement in System-on-Chip Design

Organisation:	Télécom ParisTech, LTCI CNRS, Sophia-Antipolis (FRANCE) LIP6, University Pierre et Marie Curie, Paris (FRANCE)
Method:	TML (Task Modelling Language) FIACRE CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design
Period:	2013
Size:	173,546,709 states and 472,413,097 transitions
Description:	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.
Conclusions:	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.
Publications:	[Mokrani-Boulifa-Encrenaz-13] Hocine Mokrani, Rabéa Ameur-Boulifa, and Emmanuelle Encrenaz-Tiphene. "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
Contact:	Rabéa Ameur-Boulifa Inria / OASIS project-team 2004, route des Lucioles BP 93 F-06902 Sophia Antipolis France Tel: +33 (0)4 92 38 50 52 Fax: +33 (0)4 92 38 76 44 Email: Rabea.Boulifa@sophia.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