Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Wendelin Serwe Connect in order to contact the contributor
Submitted on : Wednesday, April 8, 2015 - 11:01:27 AM
Last modification on : Wednesday, July 6, 2022 - 4:21:31 AM
Long-term archiving on: : 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. pp.708--722, ⟨10.1007/978-3-662-46681-0_62⟩. ⟨hal-01104747⟩



Record views


Files downloads