Model checking a SystemC/TLM design of the AMBA AHB protocol
Model checking a SystemC/TLM design of the AMBA AHB protocol
复制标题
对 AMBA AHB 协议的 SystemC/TLM 设计进行模型检查
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
S. Glesner
中科院分区：
文献类型：
--
作者：
Marcel Pockrandt;Paula Herber;S. Glesner
交易水平建模（TLM）越来越重要，以快速评估多媒体系统和其他混合HW/SW系统中的设计替代方案。但是，TLM模型的全面和自动验证仍然是一个困难的挑战。在先前的工作中，我们提出了一种基于转换为Uppaal定时自动机的SystemC/TLM设计模型检查的方法。在本文中，我们提出了先前提出的转型的优化版本，并通过工业案例研究的实验结果显示了其有效性。关键的想法是生成一个尤其是为了检查模型而量身定制的Uppaal模型。这大大降低了语义状态空间，并使模型检查速度大大更快，减少记忆力消耗。我们通过比较我们先前使用的案例研究的两个版本的验证时间，并通过提出了新的和更大的案例研究的结果，即AMBA高级高性能总线（AHB）的实施来证明这一点。 AMBA巴士是基于IP的嵌入式SOC中最受欢迎的芯片总线体系结构之一，它用于许多多媒体应用中。案例研究表明，通过拟议的优化，我们的方法适用于工业现实世界的例子。检测严重的错误，即在某种情况下发生僵局，以及对某些重要的安全性，livice和定时属性的验证，为我们方法的有用性提供了证据。
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.