用AIG推理检验组合电路的等价性

摘要

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