Towards Verifying Nonlinear Integer Arithmetic
| Autor: | Paul Beame, Vincent Liew |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Discrete mathematics
Integer arithmetic Diagonal 02 engineering and technology Binary logarithm Mathematical proof Wallace tree 020202 computer hardware & architecture Multiplier (Fourier analysis) Nonlinear system 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Hardware_ARITHMETICANDLOGICSTRUCTURES Mathematics |
| Zdroj: | Computer Aided Verification ISBN: 9783319633893 CAV (2) |
| DOI: | 10.1007/978-3-319-63390-9_13 |
| Popis: | We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give \(n^{O(1)}\) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and \(n^{O(\log n)}\) size proofs for these identities on Wallace tree multipliers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|