Formal verification has been successfully used to verify different types of digital circuits, including combinational and sequential logic, arithmetic circuits, and datapath designs. However, the verification techniques concentrate on confirming whether the circuit performs its intended function, while the issue of debugging, i.e., detection and correction of functional errors of the design, remains an open problem. Elaborate testing techniques have been developed that target certain types of manufacturing faults, but there are no general techniques that address the debugging issue for functional bugs. This paper addresses the issue of debugging of arithmetic circuits that due to their large size and complexity are particularly hard to verify and debug. Current debugging techniques handle only simple types of bugs: gate replacement, wrong gate polarity, or a missing gate, but cannot handle more realistic faults, such as wrong wiring or using a wrong combination of logic gates. We describe a novel method that combines formal verification and testing techniques to enable efficient identification and correction of faults. The technique involves setting select signals to some predefined constants to reduce the design to easily verifiable circuit components; these components are then verified using logic equivalence checking and SAT tools. The fault can then be identified in form or a small logic area (with a few logic gates) to be replaced by a new, functionally correct logic. The proposed technique is illustrated with debugging of different types of divider circuits up to 1024 bit-wide.

This paper describes an original approach to formal verification of a special class of modular multipliers, namely modulo$(2^{n}-1)$multipliers, critical components of cryptographic and error correction circuits. The proposed method completely avoids the expensive SAT, symbolic computer algebra, and rewriting techniques, typically used in formal verification of arithmetic circuits. Instead, recognizing a regular structure of such multipliers, constructed as an array of adders, the problem is modeled as a system of linear equations. Each adder is represented by a linear equation with an appropriate and easy to compute weight; the resulting linear system is solved by eliminating the intermediate signals, exposing the direct relation between the primary inputs and outputs. The results obtained for large$(2^{n}-1)$modular multiplier circuits show several orders of magnitude improvement in CPU time compared to those in the published literature.

The paper describes a formal verification method for hardware implementation of restoring divider circuits. The method is based on setting select signals to predefined constants to reduce the design to easily verifiable circuit components, followed by their verification using standard equivalence checking and SAT. It is then concluded by a global proof that the composition of those components indeed implements a divider. In contrast to previous approaches, the verification is done on a functional level without any reverse engineering of the internal structure. The results show significant improvement in verification time compared to other methods. The proposed approach can also be used in debugging by localizing the source of a bug. This feature is currently not available in the existing verification tools and will be a subject of future work.

This paper proposes an efficient verification and debugging method for arithmetic divider circuits. The technique involves setting select signals to some predefined constants in order to reduce the design to easily verifiable circuit components. These components are then verified using logic equivalence checking and SAT tools. An important feature of the proposed approach is that it naturally enables debugging by identifying and localizing bugs through proper selection of accessible signals. This method can verify and debug large restoring dividers within single minutes using synthesis and verification tools, such as ABC. The general debugging concept proposed here is applicable to both the restoring and non-restoring dividers. To the best of our knowledge the proposed debugging capability is not offered by any of the existing verification tools.

This paper gives a brief survey of current state-of-the-art techniques for formal verification of arithmetic circuits with suggestions for future work. In contrast to standard BDD or SAT-based approach that require a reference circuit it concentrates on Symbolic Computer Algebra (SCA) and related techniques that verify the circuits w.r.t. its abstract arithmetic specification. We examine the original computer algebra method; review the algebraic techniques of forward and backward rewriting; and AIG rewriting. We also propose a "hardware rewriting" method, which replaces algebraic rewriting by hardware synthesis of the circuit under verification appended with an inverse of the circuit, expecting it to be reduced to a redundant one.