Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking

YAN Xiao-lang; ZHENG Fei-jun; GE Hai-tong; Yang Jun

您当前的位置：

首页 >

文章列表页 >

Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking

更新时间：2025-07-16

- Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking
- Acta Electronica Sinica Vol. 32, Issue 8, Pages: 1233-1235(2004)
- 作者机构：
  
  浙江大学超大规模集成电路设计研究所,浙江,杭州,310027
- 作者简介：
- 基金信息：
- DOI：
  CLC： TN4
- Published：2004
- 稿件说明：
移动端阅览
YAN Xiao-lang, ZHENG Fei-jun, GE Hai-tong, et al. Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking[J]. Acta Electronica Sinica, 2004, 32(8): 1233-1235.
DOI：

YAN Xiao-lang, ZHENG Fei-jun, GE Hai-tong, et al. Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking[J]. Acta Electronica Sinica, 2004, 32(8): 1233-1235. DOI：

摘要

本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术.算法是在与/非图AIG中进行推理

并交替使用BDD扩展和基于电路SAT解算器简化电路.如尚未解决

将用基于合取范式SAT解算器进行推理.与已有算法相比主要有如下改进:在AIG中结合多种引擎进行简化

不存在误判可能;充分利用了基于电路解算器和基于合取范式解算器各自优点

减小了SAT推理的搜索空间.实验结果表明了本算法的有效性.

Abstract

A new combinational equivalence checking approach integrating Binary Decision Diagrams and Boolean Satisfiability is proposed.The algorithm works on the representation called And/Inverter Graph of the circuit.The BDD propogation and Circuit-based SAT Solver are applied in an intertwined manner to reduce the space of the miter circuit. If failed

CNF-based SAT Solver is used to solve the problem.The efficiency of the proposed approach is shown through its application on the LGsynth91 benchmark circuits.

关键词

Keywords

references

Views

1275

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

⁰