System- versus RT-Level Verification of Systems-on-Chip by Compositional Path Predicate Abstraction

Prof. Wolfgang Kunz - Dept. of Electrical & Computer Engineering Technische Universität Kaiserslautern
Data e ora
lunedì 3 settembre 2012 alle ore 11.15 - 11:15 rinfresco; 11:30 inizio seminario -- Sala Verde
Tiziano Villa
Referente esterno
Data pubblicazione
9 agosto 2012


We propose a new methodology to create a formal relationship between a time-abstract system-level description of a System-on-Chip (SoC) and its Register-Transfer Level (RTL) implementation. This formal relationship, called path predicate abstraction, is a weak form of a bisimulation and can be obtained by standard property checking techniques when applied in a systematic way. The proposed concepts can be used for bottom-up system verification as well as for top-down design refinements.

Since our methodology considers time-abstract system models individually for each SoC module there is the challenge to deal with the concurrency between the individual RTL components. We propose a compositional scheme describing the communication between SoC modules independently of their individual processing speed. The composed abstract system is modeled by an asynchronous composition and can be verified using the SPIN model checker.

We demonstrate the practical feasibility of our approach by a comprehensive case study based on Infineon’s FPI Bus. We show that SPIN in combination with our methodology is able to prove global system properties for the RTL implementation consisting of several concurrent SoC modules and containing approximately 30,000 state variables.

© 2002 - 2021  Università degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234