Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving
Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving
复制标题
使用可满足性模理论求解的 SystemC 的位精确形式验证
DOI：
10.1007/978-3-319-90023-0_5
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Paula Herber
中科院分区：
文献类型：
--
作者：
Lydia Jaß;Paula Herber
硬件/软件协同设计通常使用系统级设计语言SystemC来建模。尤其是对于安全关键的应用，确保这样的设计符合其要求是至关重要的。在本文中，我们提出了一种使用UCLID可满足性模理论(SMT)求解器形式化验证系统设计的方法。UCLID支持有限精度位向量运算。因此，我们可以在位精度级别上处理系统C设计，这使我们能够正式验证组成详细硬件模型的深度集成的硬件/软件系统。同时，我们利用UCLID处理符号变量的能力，并对系统C设计使用k-归纳不变量检查。利用这种归纳法，我们可以抵消模型检验方法所面临的状态空间爆炸问题。我们通过一个由位和周期精确的UART模型和从UART读取数据的软件组成的SystemC设计来展示我们方法的实际适用性。
Hardware/software codesigns are often modeled with the system level design language SystemC. Especially for safety critical applications, it is crucial toguaranteethat such a design meets its requirement. In this paper, we present an approach to formally verify SystemC designs using the UCLID satisfiability modulo theories (SMT) solver. UCLID supports finite precision bitvector arithmetics. Thus, we can handle SystemC designs on a bit-precise level, which enables us to formally verify deeply integrated hardware/software systems that comprise detailed hardware models. At the same time, we exploit UCLID’s ability to handle symbolic variables and use k-inductive invariant checking for SystemC designs. With this inductive approach, we can counteract the state space explosion problem, which model checking approaches suffer from. We demonstrate the practical applicability of our approach with a SystemC design that comprises a bit- and cycle-accurate model of a UART and software that reads data from the UART.
登录
查看更多内容
使用 SPIN 改进 SystemC 模型的系统级验证
DOI：
--
发表时间：
2013
期刊：
French Singaporean Workshop on Formal Methods and Applications
影响因子：
--
作者：
Martin Elshuber;Susanne Kandl;P. Puschner
通讯作者：
P. Puschner
使用可满足性模理论对 SpecC 模型进行形式化死锁分析
DOI：
--
发表时间：
2013
期刊：
International Conference on Exploring Services Science
影响因子：
--
作者：
Che;R. Dömer
通讯作者：
R. Dömer
模型检查硬件/软件协同设计的内存相关属性
DOI：
10.1007/978-3-642-38853-8_9
发表时间：
2013
期刊：
2018 19th International Symposium on Quality Electronic Design (ISQED)
影响因子：
--
作者：
Marcel Pockrandt;Paula Herber;V. Klös;S. Glesner
通讯作者：
S. Glesner
使用 LOTOS 和 CADP 验证工业 SystemC/TLM 模型
DOI：
--
发表时间：
2009
期刊：
2009 7th IEEE/ACM International Conference on Formal Methods and Models for Co-Design
影响因子：
--
作者：
H. Garavel;C. Helmstetter;Olivier Ponsini;Wendelin Serwe
通讯作者：
Wendelin Serwe
从系统 C 生成有限状态机
DOI：
--
发表时间：
2006
期刊：
Proceedings of the Design Automation & Test in Europe Conference
影响因子：
--
作者：
A. Habibi;Haja Moinudeen;S. Tahar
通讯作者：
S. Tahar