论文部分内容阅读
大部分基于SAT的组合电路等价性检验方法是将两个待检验的电路组合成一个miter电路，将这个电路变换成CNF形式，然后调用一个SAT判定器来确定这个CNF是否是可满足的．但是，当miter电路被变换成CNF之后，就丢掉了电路的结构信息．针对这种方法的不足，先假定miter的输出为1，然后从miter的输出端开始，回溯检查是否存在冲突来判定miter的可满足性．利用AIG的特点，把每个节点的四种输入组合归结为一种，从而使推理得到了简化。实验表明，此方法有更快的处理速度。