纵观整个芯片设计流程,从最初的架构设计到最后的投片,验证是用时最长且重要性最高的环节。对目前纳米级的设计规模而言,传统的动态验证方式已经不足以完成对整体设计的验证工作。形式验证方法因为验证覆盖的完备性,面对大规模设计的高效性,非常切合芯片后端物理实现的验证需求,因而越发广泛地被业界采用。如何对验证失败的情况进行分析,快速准确地定位问题,并提供可行的调试方案,已成为实际工程领域关注的重点。本论文在较为全面地研究总结当前广泛应用于芯片后端设计实现的形式验证技术的基础上,结合自身在实习期间的项目经历,对形式验证在数字LTE芯片实际工程中所采用的逻辑等价性对比进行了分析,取得了较为理想的结果。主要内容包括:首先在数字LTE芯片形式验证的流程方面,论文将芯片形式验证的流程细化为环境搭建、初始化、读入文件和约束、选项设置和等价性对比五个步骤,使后续工作中对结果进行分析和调试的范围更加清晰。结合LEC工具的指令对具体的运行脚本进行规范,明确了验证过程中必要的指令及相关选项。并且基于平展化和层次化这两种不同的逻辑等价性对比方式,分别对其各自的原理、实现方法和特点进行分析。然后在逻辑等价性对比结果方面,论文根据平展化模式的原理及特点确立了该模式下的调试思路,对引起形式验证失败的几种情况进行讨论并提出了解决问题的调试方案。结果表明,导致失败的原因主要有文件缺失、名称错误、扫描信号参与逻辑、UPF问题和设计综合问题。其中前三者能够在形式验证的调试阶段解决,后两者则需要与相关设计人员协同处理。接着根据层次化模式的原理及特点明确了该模式下的调试方法。基于层次化模式下验证对象规模庞大、结构复杂的特点,分析该模式中两种特有的失败情况并提出了相应的调试方案。结果表明,由于验证对象的特点,层次化模式下存在DesignWare和实例化这两种特有的问题,二者可以通过预读文件和添加约束的方法来解决。最后对逻辑等价性对比结果里的中断现象进行分析。针对传统方法在平展化模式中处理大量中断点时效率低、耗时长的这一问题,;论文对现有方法进行改良,称之为隔离对比法。该方法结合了传统基于工具指令的中断点处理方法,利用层次化模式处理中断问题时的高效性,将中断点在设计内部的子模块中进行集中的隔离处理,从而缩短验证耗时提高了验证效率。