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

摘要： 目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题，转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中，与一般的启发式SAT算法相比，该算法在求解速度和求解问题的规模等方面都明显地改进了，实验结果表明了该算法的可行性和有效性。

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