ACV: an arithmetic circuit verifier
ACV: an arithmetic circuit verifier
复制标题
ACV：算术电路验证器
DOI：
10.1109/iccad.1996.569822
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
R. Bryant
中科院分区：
文献类型：
--
作者：
Yirng;R. Bryant
基于层次验证方法，我们提出了一个算术电路验证器ACV，其中用硬件说明语言表达的电路（也称为ACV）使用布尔函数的二进制决策图和多种二进制二进制矩图（BMD）进行了象征性验证。水平功能。在ACV中将电路描述为模块的层次结构。每个模块的结构定义是逻辑门和其他模块的互连。模块也可能具有功能描述，声明输入和输出的数字编码，并根据算术表达式指定其功能。然后，验证递归进行，证明层次结构中的每个模块具有功能描述，包括顶级级别，都实现了其规范。语言和验证者包含其他增强功能，以克服将基于BMD的验证应用于电路计算功能（例如除法和平方根）的一些困难。 ACV已成功验证了许多电路，实现了乘法，除法和平方根等功能，单词大小最大为256位。
Based on a hierarchical verification methodology, we present an arithmetic circuit verifier ACV, in which circuits expressed in a hardware description language, also called ACV, are symbolically verified using binary decision diagrams for Boolean functions and multiplicative binary moment diagrams (BMDs) for word-level functions. A circuit is described in ACV as a hierarchy of modules. Each module has a structural definition as an interconnection of logic gates and other modules. Modules may also have functional descriptions, declaring the numeric encodings of the inputs and outputs, as well as specifying their functionality in terms of arithmetic expressions. Verification then proceeds recursively, proving that each module in the hierarchy having a functional description, including the top-level one, realizes its specification. The language and the verifier contain additional enhancements for overcoming some of the difficulties in applying BMD-based verification to circuits computing functions such as division and square root. ACV has successfully verified a number of circuits, implementing such functions as multiplication, division, and square root, with word sizes up to 256 bits.