Programming Languages Lunch Talk

Friday, December 6, 2019 - 12:00pm to 1:00pm


7501 Gates Hillman Centers



Digital circuits are extensively used in computers and digital systems and it is extremely important to guarantee that these circuits are correct. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques and in practice still require substantial manual effort. The currently most effective approach relies on computer algebra. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gatelevel representation of the circuit. This reduction returns zero if and only if the circuit is correct. However parts of the multiplier, i.e., final stage adders, are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage address 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. We rely 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 to verify not only large unsigned and signed multipliers much more efficiently, but also truncated multipliers.

Faculty Host: Marijn Heule

For More Information, Contact:


Seminar Series