VerA: Fully Automatic Formal Verification of Arithmetic Circuits

• Applicants: Professor Dr. Rolf Drechsler; Professor Dr.-Ing. Daniel Große; Professor Dr.-Ing. Christoph Scholl
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: from 2020 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 436285168

• Final Report Year: 2025

Final Report Abstract

Our project started from the observation that arithmetic circuits play a crucial role in many computationally intensive applications today (e.g. signal processing and cryptography) as well as in upcoming AI architectures (e.g. for machine learning and deep learning), but the verification of arithmetic circuits still formed a major challenge for automatic verification technologies – although a lot of research efforts went into the verification of arithmetic circuits since the famous Pentium bug in 1994. Our main objective was to provide a fully automatic formal verification methodology that goes beyond incomplete simulation-based approaches and semi-automatic approaches based on theorem proving which are still the state-of-the-art for arithmetic circuit verification in industrial practice. Only formal verification is able to provide rigorous guarantees concerning the correctness of arithmetic circuits. Full automation is needed, since the design of (application specific) circuits containing arithmetic is nowadays not only confined to the major processor vendors, but is also done by many different vendors of embedded hardware who can not afford to employ large teams of specialized verification engineers being able to provide human-assisted theorem proofs. Full automation enables also non-experts to carry out the verification of arithmetic circuits. In this project we were able to advance the state-of-the-art in fully automatic formal verification of multipliers and dividers to a great extent. Our work was built on recent advances in Symbolic Computer Algebra (SCA) based approaches to arithmetic circuit verification. With a multitude of improvements like efficient data structures for polynomials, novel minimization methods for polynomials, and improved construction methods for polynomials, we were able to provide a highly robust and fully automatic formal verification method for large, complex and highly optimized multipliers. We were able to successfully attack divider verification as well. Here we could show that a divider verification cannot be performed using SCA-based backward rewriting methods only, which start with a specification polynomial and basically replace signals of the circuit in a reverse topological order by polynomials for the corresponding gates. For a successful verification of large dividers, SCA-based backward rewriting has to be enhanced by forward information propagation from the inputs into the direction of the outputs. Based on this insight and based on a number of optimization methods, we were finally able to provide (fully automatically) correctness proofs for large dividers containing non-trivial optimizations on the architectural level.

Publications

• Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification. 2020 57th ACM/IEEE Design Automation Conference (DAC), 1-6. IEEE.
  Scholl, Christoph & Konrad, Alexander
  
• Towards Formal Verification of Optimized and Industrial Multipliers. 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), 544-549. IEEE.
  Mahzoon, Alireza; Grose, Daniel; Scholl, Christoph & Drechsler, Rolf
  
• GenMul: Generating Architecturally Complex Multipliers to Challenge Formal Verification Tools. Recent Findings in Boolean Techniques, 177-191. Springer International Publishing.
  Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization. 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE), 1110-1115. IEEE.
  Scholl, Christoph; Konrad, Alexander; Mahzoon, Alireza; Grobe, Daniel & Drechsler, Rolf
  
• Divider verification using symbolic computer algebra and delayed don’t care optimization. In Int’l Conf. on Formal Methods in CAD, pages 108–117
  Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große & Rolf Drechsler
  
• Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability. Proceedings of the 59th ACM/IEEE Design Automation Conference, 1183-1188. ACM.
  Mahzoon, Alireza; Große, Daniel; Scholl, Christoph; Konrad, Alexander & Drechsler, Rolf
  
• RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 41(5), 1573-1586.
  Mahzoon, Alireza; GroBe, Daniel & Drechsler, Rolf
  
• Formal Verification of Structurally Complex Multipliers. Springer International Publishing.
  Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation. Formal Methods in System Design, 67(1), 106-142.
  Konrad, Alexander; Scholl, Christoph; Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Symbolic computer algebra for multipliers revisited - it’s all about orders and phases. In Int’l Conf. on Formal Methods in CAD, 2024
  Alexander Konrad & Christoph Scholl