BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
复制标题
具有未解释函数的等式理论的基于 BDD 的程序
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
V. Singhal
中科院分区：
文献类型：
--
作者：
A. Goel;K. Sajid;H. Zhou;A. Aziz;V. Singhal
具有未解释函数的等式逻辑已被提出用于验证抽象硬件设计。对这种逻辑执行快速可满足性检查的能力对于这种验证范例的成功是必要的。我们提出了用于该逻辑可满足性检查的符号方法。第一个过程是基于限制分析有限的实例的变量。第二个过程通过引入布尔值指示变量来直接推理等式。理论和实验证据表明第二种方法的优越性。
The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for such verification paradigms to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the variables. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach.