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

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

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.