1 ALGEBRAIC APPROACH TO ARITHMETIC DESIGN VERIFICATION
Mohamed Abdul Basith, Tariq Ahmad, André Rossi, Maciej J. Ciesielski · 2011
Abstract—The paper describes an algebraic approach to functional verification of arithmetic circuits specified at bit level. The circuitis representedas anetwork of half adders,fulladders, 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 withSMT solvers show that the method is efficient,scalable and applicableto large arithmetic designs, such as multipliers. I.