SHF: Small: Network Flow Approach to Functional Verification of Arithmetic Circuits

SHF：小型：算术电路功能验证的网络流方法

• 批准号: 1319496
• 负责人: Maciej Ciesielski
• 金额: $ 35万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319496&HistoricalAwards=false
• 关键词: SHF; Small; Network; Flow; Approach

With the ever-increasing size and complexity of microelectronic systems, hardware verification has become a dominating factor of the overall design flow. One promising approach is formal functional verification of arithmetic circuits, which attempts to prove correctness of the design with respect to its intended arithmetic function. This problem is particularly challenging since Boolean techniques, traditionally used in verification of control logic, are not scalable to complex arithmetic designs. Efficient solutions to this problem will contribute to the development of state-of-the-art tools for circuit verification, increase design productivity, and lower the design development cost and consumer prices. The goal of this project is to develop efficient solution to verification of arithmetic circuits without resorting to expensive Boolean techniques. It will be accomplished by modeling the problem as a Network Flow problem, in which the circuit is represented as a network of standard arithmetic components. The computation performed by the circuit is modeled as a flow of binary data and represented as an algebraic, pseudo-Boolean expression. Functional correctness of the circuit is proved by transforming the algebraic flow expression at the primary inputs into an expression at the primary outputs and checking if it matches the binary encoding of the output. The method also offers a way to extract the arithmetic function implemented by the circuit and identify bugs in the design. The technique are applicable to complex arithmetic circuits, such as newly developed adders, large multipliers, arithmetic logic units, and other components of combinational and sequential data paths implementing complex instructions.

随着微电子系统的尺寸和复杂性不断增加，硬件验证已成为整个设计流程的主导因素。一种有前途的方法是算术电路的形式功能验证，它试图证明设计相对于其预期算术功能的正确性。这个问题特别具有挑战性，因为传统上用于验证控制逻辑的布尔技术不能扩展到复杂的算术设计。该问题的有效解决方案将有助于开发最先进的电路验证工具，提高设计生产率，并降低设计开发成本和消费者价格。该项目的目标是开发有效的解决方案来验证算术电路，而无需诉诸昂贵的布尔技术。它将通过将问题建模为网络流问题来完成，其中电路表示为标准算术组件的网络。电路执行的计算被建模为二进制数据流，并表示为代数伪布尔表达式。通过将主输入处的代数流表达式转换为主输出处的表达式并检查其是否与输出的二进制编码匹配来证明电路的功能正确性。该方法还提供了一种提取电路实现的算术函数并识别设计中的错误的方法。该技术适用于复杂的算术电路，例如新开发的加法器、大型乘法器、算术逻辑单元以及实现复杂指令的组合和顺序数据路径的其他组件。