随着大型集成电路设计和SOC芯片设计的不断进步,电路的规模,硬件的复杂度不断增大。今天,70%的设计时间是花费在验证错综复杂的系统上,传统的验证方法已经不能完全满足现今的要求,而形式验证则变得越来越重要,现在2种使用最广泛的形式验证技术相等性检查和模块检查成为研究的突破方向。本文研究工作是针对可满足问题(SAT)在组合电路验证和测试中的应用展开的。本文提出了一种能提高基于SAT的组合相等性检测,研究出一个低损耗的预处理器,可以静态地引入全局信号关系到原先的需要验证的Miter电路CNF公式,来减低SAT语句的复杂性,有效快速的建立蕴涵图,产生大量的直接,非直接和扩展回溯蕴含,加入到Miter电路的CNF公式中,来减少分析的时间。本文主要的价值之处在于:(1)通过全局信号关系引入恰当的语句,快速建立蕴含图,并且转换蕴含表达式为二进制子句。(2)利用加入的子句来约束SAT解决器的搜索空间,提供各个变量之间的关系,来增强布尔约束传递,大幅减少SAT公式的复杂性。