Formal verification of LTL formulas for SystemC designs
Formal verification of LTL formulas for SystemC designs
复制标题
SystemC 设计的 LTL 公式的形式验证
DOI：
10.1109/iscas.2003.1206243
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Daniel Große;R. Drechsler
为了处理当今的复杂性，现代电路和系统必须在高抽象级别上进行指定。最近，SystemC被提出作为一种语言，它允许在高抽象级别上进行快速模拟，并在RTL上高效地实现。为了保证设计的正确行为，必须开发一种简明的验证方法。我们给出了第一种形式验证方法，该方法允许证明线性时态逻辑(LTL)中指定的属性的正确性。与基于模拟的技术相比，可以确保完整性。我们的证明引擎是基于符号操作的，一个可伸缩的总线仲裁器的案例研究表明了该方法的有效性。
To handle today's complexity, modern circuits and systems have to be specified at a high level of abstraction. Recently, SystemC has been proposed as a language that allows a fast simulation on a high level of abstraction and an efficient realization on RTL. To guarantee the correct behavior of a design, a concise verification methodology has to be developed. We present the first formal verification approach for SystemC that allows to prove the correctness of properties specified in linear temporal logic (LTL). In contrast to simulation-based techniques, completeness can be ensured. Our proof engine is based on symbolic manipulation, and a case study of a scalable bus arbiter shows the efficiency of the approach.