Verification of an industrial SystemC/TLM model using LOTOS and CADP
Verification of an industrial SystemC/TLM model using LOTOS and CADP
复制标题
使用 LOTOS 和 CADP 验证工业 SystemC/TLM 模型
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Wendelin Serwe
中科院分区：
文献类型：
--
作者：
H. Garavel;C. Helmstetter;Olivier Ponsini;Wendelin Serwe
SystemC/TLM是用于复杂体系结构的系统级描述的广泛使用的标准。它对于快速模拟特别有用，从而允许对目标软件进行早期开发和测试。通常，对SystemC/TLM的正式验证依赖于将完整模型转换为验证工具接受的语言。在本文中，我们提出了一种通过转换为Lotos来验证SystemC/TLM描述的方法，并尽可能多地重复使用原始SystemC/TLM C ++代码。为此，我们利用正式验证工具箱CADP提供的功能，即在Lotos模型中导入外部C代码。我们在BDISP上报告了我们方法的实验，BDISP是由Stmicroelectronics设计的复杂图形处理单元。
SystemC/TLM is a widely used standard for system level descriptions of complex architectures. It is particularly useful for fast simulation, thus allowing early development and testing of the targeted software. In general, formal verification of SystemC/TLM relies on the translation of the complete model into a language accepted by a verification tool. In this paper, we present an approach to the validation of a SystemC/TLM description by translation into LOTOS, reusing as much as possible of the original SystemC/TLM C++ code. To this end, we exploit a feature offered by the formal verification toolbox CADP, namely the import of external C code in a LOTOS model. We report on experiments of our approach on the BDisp, a complex graphical processing unit designed by STMicroelectronics.