关键词: 形式验证, 等价性验证, 布尔可满足性, 二叉判决图

Abstract: The paper gives the study of binary decision diagrams and Boolean satisfiability algorithms in formal verification method.It improves on Boolean satisfiability algorithms，and gives the DC&DS algorithms.The paper gives equivalence checking algorithms in combinational circuit based on SAT，the arithmetic integrates the strongpoint of BDD and SAT，by restricting the size of constructing BDD，avoids EMS memory exploding.Reasoning minishes searching space of SAT.And apply this new algorithm in formal verification method based on BDD-SAT.Theoretical research and experimence results have proved the correctness of algorithms and design methods proposed in this paper.

Key words: formal verification, simulation, Boolean satisfiability, binary decision diagrams