随着制程节点的缩小和电路复杂性的增加,在集成电路设计过程中,逻辑等价性检查在确保功能正确性方面起着重要作用。在集成电路设计周期中,无论是前端还设计是后端实现,验证是其中必不可少的环节。除此之外,越来越多的业内人士也指出了验证测试已经成为了集成电路设计发展周期中的一个亟需解决问题。在实际工程中,当面对规模更大的集成电路时,一般需要进行分割处理从而使得后续对电路的操作更方便,这时就需要验证分割前后电路的逻辑功能是否发生变化。由于分割前后的电路设计都为RTL级电路,通过在实际工程中对传统验证方式以及采取等价性检查的方式对比后,最终得出了相比于传统验证方式,采取等价性检查的方式进行验证可以达到减少验证所花费的时间。同时,由于国产EDA软件在等价性检查这块仍然有一定的空缺,因此对电路等价性检查进行研究也是必要的。本论文工作来源于企业合作项目,重点研究RTL级电路的等价性检查技术。提出一种基于改进的SAT（Boolean satisfiability problem,SAT）求解器的电路等价性检查方案用于实际工程中RTL级组合电路等价性检查。本方案不需要额外使用国外已有的等价性检查工具,可以直接集成到实际项目中。同时对比已有的相关算法求解器以及方案,本方案能够有效提升电路等价性检查的速度特性,同时在面对规模较大的电路时,本方案可以更有效的解决等价性检查的问题。结合组合电路等价性检查的一般框架,由于其存在速度较慢,且与实际工程项目贴合度较小的问题,设计了一种基于可满足问题求解的RTL级电路等价性检查方案。所提出的方案通过合取范式（Conjunctive Normal Form,CNF）的方式建立起被验证电路的逻辑表达,对CNF表示的电路逻辑进行数学逻辑推理,将其视为一个可满足性问题(进行求解得到等价性检查结果。在构建基本的电路等价性检查方案后,进一步针对Davis-Putnam-Logemann-Loveland（DPLL）算法和Conflict Driven Clause Learning（CDCL）算法存在的搜索求解空间过大,搜索效率过低的问题进行了改进,提出一种基于蒙特卡罗树搜索（Monte Carlo Tree Search,MCTS）的CDCL算法。该算法通过加入MCTS算法的搜索求解以及模拟回溯过程,对SAT算法求解过程进行了优化,有效提升了面对大型电路进行等价性检查时求解效率低下以及因为求解空间过大而导致内存占用过多的问题。搭建测试平台,将已有的DPLL算法、CDCL算法,以及所提出的优化后的算法嵌入提出的等价性检查方案中,进行了对比验证与分析。通过在ISCAS85和LGSynth91测试集的部分子集上进行结果验证以及对比,表明所提出的等价性检查算法在面对规模较大的电路验证时,速度提升了25%左右。表明该方案可以有效的用于逻辑电路等价性检查,同时本文提出的算法相对于传统算法在解决电路等价性检查问题上表现的更好。