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 obtaine...

Full description

Saved in:
Bibliographic Details
Main Authors: Urdahl, Joakim, Stoffel, Dominik, Wedler, Markus, Kunz, Wolfgang
Format: Conference Proceeding
Language:English
Subjects:
Abstraction
Abstracts
Concrete
Formal System Verification
Hardware
Hardware > Electronic design automation > High-level and register-transfer level synthesis
Logic gates
Synchronization
System-on-a-chip
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0738-100X
DOI:10.1145/2228360.2228422