Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
(2020) 20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 p.194-204- Abstract
Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector 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 bit-level reasoning. We propose that pseudo-Boolean 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 optimal-length cutting planes... (More)
Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector 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 bit-level reasoning. We propose that pseudo-Boolean 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 optimal-length cutting planes proofs for a large class of bit-level 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 bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean 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
- bit-vector arithmetic, cutting planes, Gröbner bases, Multiplier circuits, pseudo-Boolean solving, SAT solving, verification
- host publication
- Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
- series title
- Proceedings of the 20th Conference on Formal Methods in Computer-Aided 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 Computer-Aided Design, FMCAD 2020
- conference location
- Virtual, Haifa, Israel
- conference dates
- 2020-09-21 - 2020-09-24
- external identifiers
-
- scopus:85099214613
- ISBN
- 9783854480426
- DOI
- 10.34727/2020/isbn.978-3-85448-042-6_27
- language
- English
- LU publication?
- yes
- id
- e59a307b-5033-4079-b214-27bb8b76719e
- date added to LUP
- 2021-01-26 11:36:36
- date last changed
- 2022-05-12 18:03:47
@inproceedings{e59a307b-5033-4079-b214-27bb8b76719e,
abstract = {{<p>Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector 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 bit-level reasoning. We propose that pseudo-Boolean 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 optimal-length cutting planes proofs for a large class of bit-level 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 bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean 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 Computer-Aided Design, FMCAD 2020}},
editor = {{Ivrii, Alexander and Strichman, Ofer and Hunt, Warren A. and Weissenbacher, Georg}},
isbn = {{9783854480426}},
keywords = {{bit-vector arithmetic; cutting planes; Gröbner bases; Multiplier circuits; pseudo-Boolean solving; SAT solving; verification}},
language = {{eng}},
pages = {{194--204}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
series = {{Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020}},
title = {{Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning}},
url = {{http://dx.doi.org/10.34727/2020/isbn.978-3-85448-042-6_27}},
doi = {{10.34727/2020/isbn.978-3-85448-042-6_27}},
year = {{2020}},
}