SPEAR: Hardware-based Implicit Rewriting for Square-root Circuit Verification
SPEAR: Hardware-based Implicit Rewriting for Square-root Circuit Verification
复制标题
SPEAR：基于硬件的隐式重写，用于平方根电路验证
DOI：
10.23919/date48585.2020.9116194
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
M. Ciesielski
中科院分区：
文献类型：
--
作者：
Atif Yasin;Tiankai Su;S. Pillement;M. Ciesielski
该论文介绍了门级方形 - 根电路的正式验证。除法和平方根函数是实施和证明其硬件实现正确性的最复杂的算术操作，这至关重要。与使用满意度和等价检查技术的标准方法相反，所提供的方法验证了栅极级方形 - 根电路是否实际执行根操作，而不是使用参考设计检查等效性。该方法扩展了较早为乘数开发的代数重写技术，并引入了一种新颖的隐式硬件重写技术。基于硬件重写的称为Spear的工具可以在不到18分钟的时间内验证256位栅极级别的正方根电路，该电路具有206万门。
The paper addresses the formal verification of gate-level square-root circuits. Division and square root functions are some of the most complex arithmetic operations to implement and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use satisfiability and equivalence checking techniques, the presented method verifies whether the gate-level square-root circuit actually performs a root operation, instead of checking equivalence with a reference design. The method extends the algebraic rewriting technique developed earlier for multipliers and introduces a novel technique of implicit hardware rewriting. The tool called SPEAR based on hardware rewriting enables the verification of a 256-bit gate-level square-root circuit with 0.26 million gates in under 18 minutes.