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

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.