本文在介绍各种形式化验证技术的基础上，研究使用重写系统和归纳法相结合的方法对硬件电路的正确性进行验证，主要在以下方面取得了进展。 (1)论文用重写系统和归纳方法对基于线性表的串行进位加法器和基于幂表的并行进位加法器进行了形式化验证。这两种硬件电路都可以用简单类型的重写系统描述，证明过程也较为简单。对于串行进位加法器的验证，用Verilog进行模拟需要提供字长的指数多种输入才能穷尽模拟，用Lava只证明了串行进位加法器满足交换律，而没有给出其电路本身的正确性验证，用PVS定理证明系统在最佳情况下可以利用BDD和杂凑技术实现全自动证明，但是证明方案非常复杂，用Nqthm不能完成自动证明，需要很深入的人工干预。相对而言，本文给出的串行进位加法器的证明方案非常直观，容易理解。虽然我们的验证不能完全自动化，但证明过程只需要两条预备引理就能完成。对于并行进位加法器，我们给出了直接验证过程，把Adams和Kapur给出的间接验证工作向前推进了一步。 (2)在串行进位加法器的基础上，论文进一步研究了用重写归纳法对不恢复余数阵列除法器进行验证。我们给出的除法器的描述和验证都十分严格和直观，与传统的模拟和仿真相比，其明显的优点是证明过程不受字长或电路规模限制，解决了由于实际的计算机字长较长和状态较多而导致传统方法很难穷尽模拟这一问题。 (3)论文还研究了快速傅里叶变换电路的验证问题。Lava系统给出的模型与实际的硬件实现结合得不紧密，并且只给出了基2和基22的傅里叶变换的等价性证明；用幂表表示的快速傅里叶变换算法只是一个算法描述，不是硬件规范；Elan系统的模拟仅限于8点快速傅里叶变换硬件电路。本文给出的基2的流水式快速傅里叶变换处理机的形式化描述与硬件电路密切相关，适用于任意2n点的傅里叶运算，其通用性强而且可以利用规范给出形式化验证，比现有的方法有了较好的进步。 论文的研究工作表明，重写系统和归纳方法能够用于硬件电路的精确描述和有效的正确性验证。与传统方法相比，重写归纳技术的优点是非常明显的：一方面，它可以提供对被验证系统的严格数学证明，而且这种证明不受电路规模大小限制，很好地克服了“模拟”方法的不足；另一方面，与其他通过定理证明进行电路验证的方法相比，重写归纳技术具有较为直观简单和易于理解的特点。