BARC talk by Daniela Kaufmann

Wednesday, 27 November 2019, Daniela Kaufmann, PhD student at the Institute for Formal Models and Verification, Johannes Kepler University, Austria, will give a talk on "Combining SAT and Computer Algebra to successfully verify Large Multiplier Circuits".

Title:
Combining SAT and Computer Algebra to successfully verify Large Multiplier Circuits

Abstract:
Fully automated verification of gate-level multiplier circuits remains an important  problem and is still considered to be a challenge. The currently most effective approach relies on computer algebra. However parts of the multiplier, i.e., final stage adders, are a real challenge for the computer algebraic approach.  In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers.  Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques.  Our dedicated reduction engine relies on a Gröbner basis theory for coefficient rings which in contrast to previous work no longer are required to be fields. Modular reasoning allows us to verify not only large unsigned and signed multipliers much more efficiently but also truncated multipliers.

Bio:
Since 2016 Daniela has been a PhD student supervised by Prof. Armin Biere at the Institute of Formal Models and Verification at the Johannes Kepler University Linz in Austria. Her current research focuses on developing and improving formal verification techniques of gate-level arithmetic circuits. In particular she is interested in applying  computer algebraic techniques in order to evolve fully automated circuit verification.

The talk will be followed by 1-1½ hours of more informal, technical discussions in The Creative Room (BARC, 1st floor). The purpose is to go over the material in more detail, and to have the opportunity to ask lots of questions and discuss ideas. After a theoretical talk, we go deeper into technicalities, look at the actual definitions, and prove at least some of the key ingredients in the results including all (or at least some of) the gory technical details glossed over in a polished seminar presentation. For a more applied talk, we might discuss questions of implementation or discuss detailed experimental results. As usual, this second part is entirely optional, and can safely be skipped by everybody who feels that a regular 1-hour talk is sufficient to meet their needs. No excuses needed; no questions asked...