J4 ›› 2009, Vol. 36 ›› Issue (5): 877-884.

• 研究论文 • 上一篇    下一篇

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

范全润;段振华;徐国培   

  1. (西安电子科技大学 计算机学院,陕西 西安  710071)
  • 收稿日期:2008-12-16 出版日期:2009-10-20 发布日期:2009-11-30
  • 通讯作者: 范全润
  • 基金资助:

    国家自然科学基金资助(60373103,60433010)

Combinational equivalence checking based on AIG reasoning

FAN Quan-run;DUAN Zhen-hua;XU Guo-pei   

  1. (School of Computer Science and Technology, Xidian Univ., Xi'an  710071, China)
  • Received:2008-12-16 Online:2009-10-20 Published:2009-11-30
  • Contact: FAN Quan-run

摘要:

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

关键词: 组合电路, 等价性检验, 电路推理, 与非图

Abstract:

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 experiments demonstrate the efficiency of our approach.

Key words: combinational circuits, CEC, circuit reasoning, AIG

中图分类号: 

  • TN47