Functional Verification of Hardware Dividers using Algebraic Model
Functional Verification of Hardware Dividers using Algebraic Model
复制标题
使用代数模型验证硬件分频器的功能
DOI：
10.1109/vlsi-soc.2019.8920335
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
M. Ciesielski
中科院分区：
文献类型：
--
作者：
Atif Yasin;Tiankai Su;S. Pillement;M. Ciesielski
划分是要实施的最复杂的算术操作之一，其硬件实现需要在门级上进行彻底的验证。 “在比特级网络名单上，例如定理的其他方法，主要是证明了分区算法的正确性。实施仅受到了有限的关注，通过扩展代数模型来验证门级分隔电路的问题，成功地证明了乘数和其他算术电路。执行一个部门，无需参考设计。
Division is one of the most complex arithmetic operations to implement and its hardware implementation requires thorough verification at the gate level. Dividers are difficult to verify using standard Boolean methods, such as equivalence checking or SAT-based techniques, as they require “bit-blasting” onto bit-level netlists. Other methods, such as theorem provers, concentrate mostly on proving correctness of the division algorithm. However, verification of low-level hardware implementations has received only a limited attention. This paper addresses the problem of verifying gate-level divider circuits by extending an algebraic model, successfully used to prove multipliers and other arithmetic circuits, to dividers. The method verifies whether the gate-level divider circuit actually performs a division, without a need for a reference design.