Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip

Abderahman Kriouile 1, 2 Wendelin Serwe 2
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : In this paper we report about a case study on the functional verification of a System-on-Chip (SoC) with a formal system-level model. Our approach improves industrial simulation-based verification techniques in two aspects. First, we suggest to use the formal model to assess the sanity of an interface verification unit. Second, we present a two-step approach to generate clever semi-directed test cases from temporal logic properties: model-based testing tools of the CADP toolbox generate system-level abstract test cases, which are then refined with a commercial Coverage-Directed Test Generation tool into interface-level concrete test cases that can be executed at RTL level. Applied to an AMBA 4 ACE-based cache-coherent SoC, we found that our approach helps in the transition from interface-level to system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.
Liste complète des métadonnées
Contributor : Wendelin Serwe <>
Submitted on : Wednesday, April 8, 2015 - 11:01:27 AM
Last modification on : Wednesday, December 14, 2016 - 1:08:45 AM
Document(s) archivé(s) le : Tuesday, April 18, 2017 - 1:36:17 PM


Files produced by the author(s)




Abderahman Kriouile, Wendelin Serwe. Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip. 21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2015, London, UK, France. <10.1007/978-3-662-46681-0_62>. <hal-01104747>



Record views


Document downloads