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

Supervisor
Prof. Wolfgang Kunz - Dept. of Electrical & Computer Engineering Technische Universit├Ąt Kaiserslautern
Date and time
Monday, September 3, 2012 at 11:15 AM - 11:15 rinfresco; 11:30 inizio seminario -- Sala Verde
Programme Director
Tiziano Villa
External reference
Publication date
August 9, 2012
Department
Computer Science  

Summary

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  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234