Verifying Properties of Bitvector Multiplication Using Cutting Planes Reasoning
(2020) 20th International Conference on Formal Methods in ComputerAided Design, FMCAD 2020 In Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020 p.194204 Abstract
Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bitlevel reasoning. We propose that pseudoBoolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimallength cutting planes... (More)
Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bitlevel reasoning. We propose that pseudoBoolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimallength cutting planes proofs for a large class of bitlevel properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bitlevel consequences of wordlevel equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudoBoolean solvers can verify the wordlevel equivalence of adderbased multiplier architectures, as well as commutativity of bitvector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bitlevel. Finally, we find examples of simple nonlinear bitvector inequalities that are intractable for current bitvector and SAT solvers but easy for pseudoBoolean solvers.
(Less)
 author
 Liew, Vincent ; Beame, Paul ; Devriendt, Jo ^{LU} ; Elffers, Jan ^{LU} and Nordstrom, Jakob ^{LU}
 organization
 publishing date
 2020
 type
 Chapter in Book/Report/Conference proceeding
 publication status
 published
 subject
 keywords
 bitvector arithmetic, cutting planes, Gröbner bases, Multiplier circuits, pseudoBoolean solving, SAT solving, verification
 host publication
 Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020
 series title
 Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020
 editor
 Ivrii, Alexander ; Strichman, Ofer ; Hunt, Warren A. and Weissenbacher, Georg
 article number
 9283622
 pages
 11 pages
 publisher
 IEEE  Institute of Electrical and Electronics Engineers Inc.
 conference name
 20th International Conference on Formal Methods in ComputerAided Design, FMCAD 2020
 conference location
 Virtual, Haifa, Israel
 conference dates
 20200921  20200924
 external identifiers

 scopus:85099214613
 ISBN
 9783854480426
 DOI
 10.34727/2020/isbn.9783854480426_27
 language
 English
 LU publication?
 yes
 id
 e59a307b50334079b21427bb8b76719e
 date added to LUP
 20210126 11:36:36
 date last changed
 20220512 18:03:47
@inproceedings{e59a307b50334079b21427bb8b76719e, abstract = {{<p>Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bitlevel reasoning. We propose that pseudoBoolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimallength cutting planes proofs for a large class of bitlevel properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bitlevel consequences of wordlevel equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudoBoolean solvers can verify the wordlevel equivalence of adderbased multiplier architectures, as well as commutativity of bitvector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bitlevel. Finally, we find examples of simple nonlinear bitvector inequalities that are intractable for current bitvector and SAT solvers but easy for pseudoBoolean solvers. </p>}}, author = {{Liew, Vincent and Beame, Paul and Devriendt, Jo and Elffers, Jan and Nordstrom, Jakob}}, booktitle = {{Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020}}, editor = {{Ivrii, Alexander and Strichman, Ofer and Hunt, Warren A. and Weissenbacher, Georg}}, isbn = {{9783854480426}}, keywords = {{bitvector arithmetic; cutting planes; Gröbner bases; Multiplier circuits; pseudoBoolean solving; SAT solving; verification}}, language = {{eng}}, pages = {{194204}}, publisher = {{IEEE  Institute of Electrical and Electronics Engineers Inc.}}, series = {{Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020}}, title = {{Verifying Properties of Bitvector Multiplication Using Cutting Planes Reasoning}}, url = {{http://dx.doi.org/10.34727/2020/isbn.9783854480426_27}}, doi = {{10.34727/2020/isbn.9783854480426_27}}, year = {{2020}}, }