不恢复余数阵列除法器的形式化描述和验证方法

Formal Specification & Verification of Non Restoring Array Divider

本文使用重写技术对不恢复余数阵列除法器进行了形式化描述并结合归纳法对该除法器的正确性进行了验证,整个工作是建立在串行加法器的描述和验证基础上的。不恢复余数阵列除法器的运算和控制有一定的复杂度,适合用大规模集成电路实现。本文成功地用重写归纳法对它进行了描述和验证,说明重写归纳法在硬件电路正确性验证方面有广阔的应用前景。

Non restoring array divider is a complex arithmetic circuit that can be built using very large scale integrated circuit. In this paper, a specification of non restoring array divider is established using rewrite rules. Rewriting induction techniques are directly used to verify the correctness of the division circuit by proving that it can compute the correct middle result at each step. The specification and verification are based on the correctness of ripple carry adders we have discussed elsewhere in an earlier paper. It shows that rewriting induction has wide applications in the area of complex hardware verifications.