Verifying SystemC using an intermediate verification language and symbolic simulation
Verifying SystemC using an intermediate verification language and symbolic simulation
复制标题
DOI：
10.1145/2463209.2488877
复制
发表时间：
2013-05
期刊：
影响因子：
--
通讯作者：
H. M. Le;Daniel Große;V. Herdt;R. Drechsler
中科院分区：
文献类型：
--
作者：
H. M. Le;Daniel Große;V. Herdt;R. Drechsler
SystemC的正式验证具有挑战性。在处理符号输入和并发语义之前，需要将设计转换为正式模型。到目前为止，缺乏这种前端阻碍了高效后端的发展。在本文中，我们通过使用中间验证语言（IVL）提出了一种孤立的方法。这使SystemC-to-IVL翻译器（FROND-END）和IVL验证者（后端）可以独立开发。我们提出了一个紧凑但一般的IVL，与广泛的基准集合一起将有助于未来的研究。此外，我们提出了一个有效的符号模拟器，该模拟器整合了部分订单减少。与现有方法的实验比较表明了其潜力。
Formal verification of SystemC is challenging. Before dealing with symbolic inputs and the concurrency semantics, a front-end is required to translate the design to a formal model. The lack of such front-ends has hampered the development of efficient back-ends so far. In this paper, we propose an isolated approach by using an Intermediate Verification Language (IVL). This enables a SystemC-to-IVL translator (frond-end) and an IVL verifier (back-end) to be developed independently. We present a compact but general IVL that together with an extensive benchmark set will facilitate future research. Furthermore, we propose an efficient symbolic simulator integrating Partial Order Reduction. Experimental comparison with existing approaches has shown its potential.