Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
复制标题
用于全自动分频器验证的符号计算机代数和基于 SAT 的信息转发
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Alexander Konrad
中科院分区：
文献类型：
--
作者：
Christoph Scholl;Alexander Konrad
在过去的几年中，符号计算机代数（SCA）在栅极级别验证大整数和有限的现场乘数方面取得了出色的结果。与那些令人鼓舞的进步相反，基于SCA的分隔验证仍处于起步阶段，并等待着一个重大突破。在本文中，我们分析了迄今为止基于SCA的分隔验证成功的基本原因，并且基于SAT的信息转发（SBIF）。 SBIF通过在相反方向上通过信息传播来增强基于SCA的向后重写。我们成功地将该方法应用于大型非恢复分隔线的全自动验证。
During the last few years Symbolic Computer Algebra (SCA) delivered excellent results in the verification of large integer and finite field multipliers at the gate level. In contrast to those encouraging advances, SCA-based divider verification has been still in its infancy and awaited a major breakthrough. In this paper we analyze the fundamental reasons that prevented the success for SCA-based divider verification so far and present SAT Based Information Forwarding (SBIF). SBIF enhances SCA-based backward rewriting by information propagation in the opposite direction. We successfully apply the method to the fully automatic formal verification of large non-restoring dividers.