【摘要】 介绍布尔可满足性 (SAT)求解程序在测试向量自动生成、符号模型检查、组合等价性检查和RTL电路设计验证等电子设计自动化领域中的应用 着重阐述如何在算法中有机地结合电路拓扑结构及其与特定应用相关的信息 ,以便提高问题求解效率 最后给出下一步可能的研究方向更多还原

【Abstract】 Boolean Satisfiability is probably the most studied of combinatorial search problems and finds a number of applications in electronic design automation (EDA). In recent years, quite a few new and efficient SAT solvers have been developed, which make it possible solving much larger problem instances. We highlight the use of SAT algorithm to solve lots of EDA problems in such diverse areas as test pattern generation, symbolic model checking, combinational equivalence checking, and verification for RTL design. In addition, it is stressed how the useful information of circuit structure and specific problems to be solved is introduced to accelerate the SAT based algorithms.更多还原