Formal verification at higher levels of abstraction
Formal verification at higher levels of abstraction
复制标题
更高抽象级别的形式验证
DOI：
10.1109/iccad.2007.4397326
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
D. Kroening;S. Seshia
市场上的大多数形式化验证工具将高级寄存器传输级（RTL）设计转换为位级模型。在比特级操作的算法不能利用由更高的抽象级提供的结构，因此，可伸缩性较低。本教程调查最近的进展，在形式化验证使用高级模型。我们提出了词级验证谓词抽象和可满足性模理论（SMT）求解器。然后，我们描述了术语级建模技术和方法，结合联合收割机字级和术语级的方法，可扩展的验证。
Most formal verification tools on the market convert a high-level register transfer level (RTL) design into a bit-level model. Algorithms that operate at the bit-level are unable to exploit the structure provided by the higher abstraction levels, and thus, are less scalable. This tutorial surveys recent advances in formal verification using high-level models. We present word-level verification with predicate abstraction and satisfiability modulo theories (SMT) solvers. We then describe techniques for term-level modeling and ways to combine word-level and term-level approaches for scalable verification.