随着集成电路设计复杂度的与日俱增，而芯片的更新换代速度也在不断加快，使得集成电路芯片的验证越来越困难。传统的芯片验证主要是基于仿真模拟的验证，其验证周期长，无法做到全覆盖的用例验证。形式化验证是根据规范化语言描述的属性，使用数学的方法证明其是否满足给定的系统模型，具有完备性，从而避免了仿真验证的缺点。尽管如此，该方法本身就是计算复杂度敏感的，它只能验证较小的集成电路芯片模型，当规模过大时，将造成状态爆炸问题。所以为了达到更好的性能，需要采用抽象来减少用于形式验证所需的状态数，与此同时需要保证抽象后的模型对于要验证的属性保持与原模型具有相同的功能性，只有这样才能保证模型抽象的正确性。本文从形式化验证的基础理论出发，对模型抽象技术和一些验证平台进行了讨论，并对其应用范围进行了扩展和补充，以期在模型检验的过程中，达到加速验证过程的目的。文中首先介绍形式化验证方法、时态逻辑和模型抽象的基础理论，其次介绍了GSTE验证方法，并对其扩展的部分如支持-regular的性质、断言图等做详细的阐述。通过对VIS平台采用的规范化描述语言CTL的详细介绍，讨论了CTL与断言图的表达的范围的关系，从而最终确立了只对不变属性进行对比测试。通过以上的学习和比较分析，将介绍在VIS平台以及在该平台上开发的基于GSTE验证方法的Whale工具，并通过引入非阻塞赋值算法解决了VIS无法处理非阻塞赋值语句的缺陷，完成了对UART的寄存器传输级模型的FSM的状态转移的验证和对发送的数据是否与输入数据一致的符号化验证。实验表明，该方法能够完成测试用例的全覆盖，说明了该方法在实际例子中所具有的重要意义。针对状态爆炸问题，本文将模型抽象中的模型划分技术引入到GSTE验证方法中，通过采用基于断言图的模型抽象技术，在对不变属性的验证过程中取得了重要的性能提升。通过与VIS中各种模型检验算法的性能比较结果，证明，在引入抽象技术后，GSTE验证方法通过缩短到达不动点的步数，使得在验证无反例的不变属性例子时，具有更快的速度。