Algebraic approach to arithmetic design verification

The paper describes an algebraic approach to functional verification of arithmetic circuits specified at bit level. The circuit is represented as a network of half adders, full adders, and inverters, and modeled as a system of linear equations. The proof of functional correctness of the design is obtained by computing its algebraic signature using standard LP solver and comparing it with the reference signature provided by the designer. Initial experimental results and comparison with SMT solvers show that the method is efficient, scalable and applicable to large arithmetic designs, such as multipliers.