Combining SAT and Computer Algebra to successfully verify Large Multiplier Circuits

Description

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.

Period	27 Nov 2019
Event title	BARC Talk
Event type	Other
Location	DenmarkShow on map