The demand for compute-intensive applications such as AI/ML has led to the development of processors with complex functionalities. The Multiply Accumulate (MAC) unit is a vital component in these processors, but its verification is very challenging due to the highly optimized designs used to implement the MAC operation. In this paper, we show some interesting results for optimized MAC design verification using a formal proof engine, Symbolic Computer Algebra (SCA). For the first time, we exploit the combined benefit of phase and dynamic ordering in verifying MAC circuits, a capability not possible using state-of-the-art SCA proof engines.

Floating-point multipliers play a crucial role in accelerating modern computing and are therefore implemented regularly, e.g., as part of AI accelerators or FPUs. They are built as a complex combination of control flow and integer arithmetic elements. This requires fast and easily applicable formal verification methods to ensure correctness. While formal verification is required to prove 100% correctness of the circuit, state-of-the-art methods fail to provide bounds for the resource and time consumption of the verification.We introduce an automated approach for formally verifying an IEEE-754-compliant floating-point multiplier with polynomial bound complexity. While state-of-the-art verification approaches based on SAT and Binary Decision Diagrams (BDDs) fail, our technique based on an adapted symbolic simulation using BDDs enables a fast and predictable verification process. Extensive case splitting is performed to prevent exponential BDD growth. The applicability is proven by verifying a single precision floating-point multiplier used in a popular floating-point unit.

Decision Diagrams (DDs) are among the most popular representations for Boolean functions. They are widely used in the synthesis and verification of digital circuits. The size (i.e., number of nodes) and computation time (required time for performing operations) are two important parameters that determine the efficiency of a DD in different applications. It has been proven that some DDs can represent specific functions in polynomial space or perform certain operations in polynomial time. For example, Binary Decision Diagrams (BDDs) are capable of representing a wide variety of functions (e.g. integer addition) in polynomial space with respect to the input size. However, there are also some functions (e.g., integer multiplication) for which the exponential lower-bounds have been proven for the BDD sizes. In this paper, we investigate the space complexity of representing an integer addition, where one of the operands is shifted to the right by an arbitrary value. We call this function the shifted addition. This function is widely used in many digital circuits, e.g., floating point adders. We prove that the size of the BDD representing a shifted addition has exponential space complexity with respect to the input size. It is an important step towards clarifying the reasons behind the failure of BDD-based verification and synthesis when they are applied to the circuits containing shifted addition, e.g., floating point adders. • BDDs reach exponential size when symbolically simulating a floating point adder. • The lower bound for BDDs representing a shifted addition is exponential ( 2 n / 4 ). • The proof is performed by using fooling sets.

In this paper, we present our verifier that takes advantage of Binary Decision Diagrams (BDDs) with case splitting to fully verify a floating point adder. We demonstrate that the traditional symbolic simulation using BDDs has an exponential time complexity and fails for large floating point adders. However, polynomial bounds can be ensured if our case splitting technique is applied in the specific points of the circuit. The efficiency of our verifier is demonstrated by experiments on an extensive set of floating point adders with different exponent and significand sizes.

Only formal methods can guarantee the correctness of a circuit, but are usually very time and memory consuming. Therefore, efficient formal verification is key in the design of complex circuits. Many verification techniques have been introduced, which mostly fail to give bounds for the time complexity of the verification process. To overcome this issue, Polynomial Formal Verification (PFV) was introduced. This paper introduces a novel approach to PFV of circuits, by leveraging the concept of constant cutwidth. We divide the circuit into subgraphs, one for every output. This makes the verification of every subgraph only dependent on the cutwidth of the circuit and independent of the bitwidth. One main problem we solve is the passing of information between those subgraphs. The approach enables formal verification in linear time for circuits with constant cutwidth.