System verification of concurrent RTL modules by compositional path predicate abstraction

A new methodology for formal system verification of System-on-Chip (SoC) designs is proposed. It does not only ensure correctness of the system-level models but also of the concrete implementation at the Register-Transfer-Level (RTL). For each SoC module at the RTL an abstract description is obtained by path predicate abstraction. Since this leads to time-abstract system models the main challenge is 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 as 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.