形式化验证技术起源于20世纪60年代软件危机。直至整个70年代，形式化验证技术所针对的一般是转换型程序，即单纯进行科学计算、计数等功能的软件。形式化验证的巨大成功首先来自于80年代后期符号模型检验(Symbolic ModelChecking)方法的提出和在硬件验证中的实现。1987年，McMillan在博士论文中，首次将发表于前一年的二分决策图(Binary Decision Diagram)技术应用于模型检验中，从而大大地缓解了空间爆炸问题。其后的一系列改进更增强了对符号模型检验技术的信心。然而，人们很快就发现，对于复杂系统，空间爆炸问题仍是符号模型检验技术难以克服的障碍，这导致了在1999年定界模型检验技术的提出。总的来说，模型检验方法在硬件验证上是成功的，其根本原因是硬件通常有层次性且比较规整，相比于软件的复杂程序结构，更易于描述和验证。本文主要介绍形式化验证技术在集成电路自动化设计中的应用。首先介绍了形式化验证技术的发展现状和集成电路自动化设计流程，然后介绍了框架时序逻辑程序设计语言，本文利用这种语言实现了简单时序电路的描述。随后本文介绍了模型检验工具的设计原理和移植框架，并使用移植后的模型检验工具对采用框架时序逻辑程序设计语言描述的电路进行模拟验证。最后本文介绍了可满足性验证和等价性验证。本文详细阐述了集成电路自动化设计中的逻辑综合过程，设计原则，综合工具，并在此基础上完成了组合电路逻辑综合前后的等价性验证。