摘要
大部分基于SAT的组合电路等价性检验方法是将两个待检验的电路组合成一个miter电路,将这个电路变换成CNF形式,然后调用一个SAT判定器来确定这个CNF是否是可满足的.但是,当miter电路被变换成CNF之后,就丢掉了电路的结构信息.针对这种方法的不足,先假定miter的输出为1,然后从miter的输出端开始,回溯检查是否存在冲突来判定miter的可满足性.利用AIG的特点,把每个节点的四种输入组合归结为一种,从而使推理得到了简化.实验表明,此方法有更快的处理速度.
Most SAT based combinational equivalence checking algorithms combine two circuits into a miter, and then convert the miter into a CNF formula. After that, an SAT solver is invoked to check whether the CNF formula is satisfiable. However, when a miter is converted into a CNF formula, the structure information of the circuit is lost. In this paper, we assume the output of the miter is 1, and then the backtracking method is used for conflict checking to decide the satisfiability of the miter. By using the character of AIG, four input combinations of each node can be reduced into one to simplify the deducing procedure. Preliminary exlgeriments demonstrate the efficiency of our approach.
出处
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2009年第5期877-884,共8页
Journal of Xidian University
基金
国家自然科学基金资助(60373103
60433010)
