基于逻辑松弛的性质检查
计算机科学中的逻辑
2016-01-13 v1
摘要
我们引入了用于时序电路性质检查（PC）的新框架。它基于一种称为逻辑松弛（LoR）的方法。给定安全性质，LoR方法松弛所处理的转移系统，从而扩展可达状态集合。对于第j时间帧，LoR方法计算仅由松弛系统经j次转移可达的坏状态集合的超集A_j。集合A_j通过称为部分量词消去的技术构建。若A_j不包含坏状态且该状态在松弛系统中经j次转移可达，则它在原系统中也可达。因此所讨论的性质不成立。通过LoR进行PC的吸引力如下。LoR生成的归纳不变式（或反例）是仅计算松弛系统中可达状态的结果。因此，通过寻找接近原系统的“错误”松弛，PC的复杂度可急剧降低。这类似于等价性检查，其复杂度强烈依赖于待比较设计的相似程度。
引用
@article{arxiv.1601.02742,
title = {Property Checking By Logic Relaxation},
author = {Eugene Goldberg},
journal= {arXiv preprint arXiv:1601.02742},
year = {2016}
}