随着集成电路复杂度的增长，传统的仿真验证方法越来越难以确保电路的正确性。形式化验证方法已经成为学术界研究的热点，并且逐步开始在工业界得到应用。在集成电路中普遍存在着一类针对数据处理的电路。它们输入数据，对数据进行计算、排列、路由等操作，然后将结果输出。数据从输入到输出流经的路径形成了数据通路。我们称这类电路为数据通路型电路。本文对数据通路型电路的形式化验证方法进行了系统的研究，制定了一套行之有效的验证方法学。该方法学综合使用多种自动化程度较高的形式化验证技术，并使用分治、裁剪、抽象等辅助技术弥补这些形式化验证技术在处理规模上的不足。本文的主要贡献和创新点包括：　　 1．给出了一种使用*PHDD稳定处理除法运算和取模运算的方法。*PHDD的除法操作和取模操作被认为是不稳定的，容易引发空间爆炸，这在一定程度上限制了*PHDD的应用。本文认为在一般情况下，*PHDD的除法操作和取模操作的确是不稳定的，但是在特殊情况下，*PHDD也许存在着稳定的除法操作和取模操作。我们对整除的情况进行了一系列测试，发现非整除的节点数呈指数增长，而整除的节点数呈线性增长，就此得到一个经验性的结论：*PHDD的除法操作和取模操作在整除时具有稳定性。这一结论被应用于龙芯3号浮点乘加部件的形式化验证，成功解决了Booth编码器中取模运算所引发的*PHDD空间爆炸问题。　　 2．给出了一种称为时间标记方法的数据标记方法。在数据通路型电路的形式化验证中，数据通常需要一个唯一标识，以便识别该数据所对应的结果。传统的数据标记方法借助于外部提供的某种ID，其唯一性由电路环境保证，因此在验证电路时必须施加ID唯一性的假设。这种假设不但会增加验证的复杂度，而且容易导致电路和环境之间形成假设循环。时间标记方法不必借助于外部ID，而是利用电路自身的数据通路对数据进行标记，从而避免了外部假设所带来的困扰。该方法为每个数据字附加一个标识变量，用于传递标识，并且使用场景构造方法为标识输入产生不确定性激励，使标识输入的行为具有一般性。这些附加部分所带来的开销较小，并且借助于数据抽象，标识变量的开销可以被进一步消除。时间标记方法被应用于龙芯3号浮点乘加部件的形式化验证，使控制部分的验证不必依赖于外部提供的标志ID。　　 3．改进了基于属性的自动机裁剪方法。基于属性的自动机裁剪方法是一种模型检测辅助技术，通过删除自动机中与指定属性无关的部分，减小自动机的体积，从而抑制模型检测的状态爆炸问题。传统的自动机裁剪方法将待验证属性分解为一系列非全称性基本公式，然后依次为每个基本公式计算自动机的轻量版本。本文认为传统方法单独处理各个基本公式的模式忽略了基本公式之间存在的固有联系，而这种联系有助于挖掘自动机中更多的可裁剪部分。为此我们对传统方法进行了改进，首先将基本公式的裁剪规则扩展至全称性基本公式，然后将待验证属性分解为一系列基本公式（可能含有全称性基本公式），并同时推进所有基本公式的裁剪过程，以便利用基本公式之间的联系获得更好的裁剪效果。传统方法和改进方法在一个ATA控制器上进行了对比。实验结果表明，通过精心设计属性，使各个基本公式仅描述系统的一小部分，可以充分发挥改进方法的优势，带来上百倍的效率提升。　　 本文的方法已经应用于龙芯3号浮点乘加部件的验证，发现了3处仿真验证未能发现的错误，这些错误均在流片之前得到了修正。