DocumentCode :
64267
Title :
Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs
Author :
Urdahl, Joakim ; Stoffel, Dominik ; Kunz, Wolfgang
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Kaiserslautern, Kaiserslautern, Germany
Volume :
33
Issue :
2
fYear :
2014
fDate :
Feb. 2014
Firstpage :
291
Lastpage :
304
Abstract :
A formal methodology for system verification of system-on-chip (SoC) designs is proposed. It ensures that system-level models are created that are sound abstractions of the concrete implementations at the register transfer level (RTL). For each SoC module at the RTL, an abstract description is obtained by path predicate abstraction. Path predicate abstraction is introduced based on the notion of operational graph coloring. It is shown to what extent the proposed abstraction mechanism is related to the notion of a stuttering bisimulation employed in the field of theorem proving. The proposed methodology, however, does not rely on theorem proving but is entirely based on standard techniques of property checking. Path predicate abstraction leads to time-abstract system models that can be composed into abstract system models. We demonstrate the practical feasibility of our approach by two comprehensive industrial case studies.
Keywords :
graph colouring; integrated circuit design; system-on-chip; RT-level circuit designs; SoC; abstract description; graph coloring; path predicate abstraction; register transfer level; sound system-level models; stuttering bisimulation; system-on-chip; theorem proving; Abstracts; Color; Concrete; Integrated circuit modeling; Logic gates; Standards; System-on-chip; Abstraction; formal verification; property checking; system-level design;
fLanguage :
English
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
0278-0070
Type :
jour
DOI :
10.1109/TCAD.2013.2285276
Filename :
6714585
Link To Document :
بازگشت