Bugs in hardware are expensive!
Digital circuits are extensively used in computers and digital systems. They are able to represent models for various digital components and arithmetic operations. The basic function of such a circuit is to compute binary digital values for the logical function it implements, given binary values at the input. The computation of the logical function is usually realized by logic gates. These gates represent simple Boolean functions such as negation, conjunction or disjunction.
A subclass of digital circuits are combinational logic circuits where the output is a function of the present input only. That is, the output does not depend on previous input values. Computer circuits use combinational logic to perform Boolean algebra. For example, the part of an arithmetic logic unit (ALU) in a CPU, which is responsible for mathematical calculations, is constructed using combinational logic. These circuits are also called arithmetic circuits.
Proving the correctness, i.e., formal verification, of arithmetic circuits is important to help to prevent issues like the famous Pentium FDIV bug. This bug affected the floating point unit (FPU) of the early Intel Pentium processors . The processor might return incorrect binary floating point results when dividing a number.
Even more than 25 years after the Pentium FDIV bug, automatically verifying an arithmetic circuit, and more prominently multiplier circuits, is still a challenge.
Automated Reasoning
Formal verification allows proving or disproving the correctness of a given software or hardware system with respect to a certain specification. To this end the system is first translated into a mathematical model. Then we apply automated decision processes to derive the desired correctness properties. The different formal verification approaches can be distinguished by the mathematical formalism used in the verification process.
One of the currently most effective approaches for fully automated verification of arithmetic circuits uses computer algebra. In this method the given circuit is modeled as a set of polynomials and it is checked, whether the specification, also given as a polynomial, is implied by the circuit polynomials. The main issue of the algebraic approach is that the size of the intermediate polynomials grows drastically during the verification process.
In our line of research we developed several techniques to overcome this issue. We use a combination of satisfiability checking (SAT solving) and computer algebra. Certain parts of arithmetic circuits are hard to verify using computer algebra, but are easy for SAT solvers. Furthermore, we use preprocessing techniques and eliminate certain variables from the polynomial model of the circuit. By that we gain a simpler representation of the arithmetic circuit. Finally, we use an incremental verification algorithm, which allows us to split the verification problem into smaller more manageable subproblems. We implemented this technique in our tool AMulet 2.0. The CDF plot below gives an indication of the potential of our approach.
