DocumentCode :
2436780
Title :
Model checking a SystemC/TLM design of the AMBA AHB protocol
Author :
Pockrandt, Marcel ; Herber, Paula ; Glesner, Sabine
Author_Institution :
Tech. Univ. Berlin, Berlin, Germany
fYear :
2011
fDate :
13-14 Oct. 2011
Firstpage :
66
Lastpage :
75
Abstract :
Transaction Level Modeling (TLM) is gaining more and more importance to quickly evaluate design alternatives in multimedia systems and other mixed HW/SW systems. However, the comprehensive and automated verification of TLM models is still a difficult challenge. In previous work, we presented an approach for model checking of SystemC/TLM designs based on a transformation into Uppaal timed automata. In this paper, we present an optimized version of our previously proposed transformation, and show its effectiveness with experimental results from an industrial case study. The key idea is to generate a Uppaal model that is especially tailored for being model checked. This significantly reduces the semantic state space and makes model checking considerably faster and less memory-consuming. We demonstrate this by comparing the verification times of both versions for our previously used case study, and by presenting results from a new and larger case study, namely a TLM implementation of the AMBA Advanced High-performance Bus (AHB). The AMBA bus is one of the most popular on-chip bus architectures in IP-based embedded SoCs, and it is used in many multimedia applications. The case study shows that with the proposed optimizations, our approach is applicable for industrial real world examples. The detection of a serious bug, namely a deadlock situation in a certain scenario, and also the verification of some important safety, liveness, and timing properties provide evidence for the usefulness of our approach.
Keywords :
automata theory; formal verification; hardware-software codesign; logic design; system-on-chip; AMBA AHB protocol; IP-based embedded SoC; SystemC/TLM design; Uppaal model; advanced high-performance bus; mixed HW/SW system; model checking; multimedia system; on-chip bus architecture; semantic state space; serious bug; transaction level modeling; Automata; Clocks; Payloads; Semantics; Sockets; Time domain analysis; Time varying systems;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Embedded Systems for Real-Time Multimedia (ESTIMedia), 2011 9th IEEE Symposium on
Conference_Location :
Taipei
Print_ISBN :
978-1-4577-2123-6
Type :
conf
DOI :
10.1109/ESTIMedia.2011.6088527
Filename :
6088527
Link To Document :
بازگشت