Combining SAT and Computer Algebra for Circuit Verification

          @misc{ scivideos_17231,
            doi = {},
            url = {https://simons.berkeley.edu/talks/tbd-262},
            author = {},
            keywords = {},
            language = {en},
            title = {Combining SAT and Computer Algebra for Circuit Verification},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {feb},
            note = {17231 see, \url{https://scivideos.org/index.php/Simons-Institute/17231}}
          }
          

Abstract

Even more than 25 years after the Pentium FDIV bug, automated verification of arithmetic circuits, and most prominently gate-level integer multipliers, still imposes a challenge. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In this talk, we will demonstrate a verification technique that is based on algebraic reasoning and is currently considered to be one of the most successful verification techniques for circuit verification. In this approach the circuit is modelled as a set of polynomial equations. For a correct circuit we need to show that the specification is implied by the polynomial representation of the given circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using only computer algebra. We will present a hybrid approach which combines SAT and computer algebra to tackle this issue.