一种利用增量SAT从仿真中进行性质检查的工具箱(扩展摘要)
软件工程
2018-11-07 v1 计算机科学中的逻辑
摘要
我们提出一个工具,主要支持从一次运行中的状态序列出发检查有界性质的能力。目标设计被编译为AIGNET,随后被选择性且迭代地翻译为增量SAT实例,其中为新项添加子句,并通过已有文字的赋值进行简化。该工具的其他应用可由用户提供约束函数的替代挂接而派生,这些挂接引导所执行的迭代和SAT检查。文中包含了一些Verilog RTL示例以供参考。
引用
@article{arxiv.1811.02005,
title = {A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract)},
author = {Rob Sumners},
journal= {arXiv preprint arXiv:1811.02005},
year = {2018}
}
备注
In Proceedings ACL2 2018, arXiv:1810.03762