基于逻辑松弛的等价性检查
计算机科学中的逻辑
2016-07-12 v3
摘要
我们引入了一种用于布尔电路等价性检查（EC）的新框架，基于称为逻辑松弛（LoR）的通用技术。LoR的本质是松弛待求解的公式并计算新行为集合的超集S。即，S包含由于松弛而出现的所有新满足赋值，且不包含满足原始公式的赋值。集合S由称为部分量词消去的过程生成。如果所有可能的坏行为都在S中，则原始公式不可能有它们，因此该公式描述的属性成立。通过LoR进行EC的吸引力有两方面。首先，它促进强大的归纳证明的生成。其次，证明不等价归结为检查松弛公式中（即原始公式的更简单版本中）某些坏行为的存在。我们给出了一些支持我们方法的实验证据。
引用
@article{arxiv.1511.01368,
title = {Equivalence Checking By Logic Relaxation},
author = {Eugene Goldberg},
journal= {arXiv preprint arXiv:1511.01368},
year = {2016}
}