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.