Towards Verifying Nonlinear Integer Arithmetic

被引：5
|
作者：
Beame, Paul [1 ]
Liew, Vincent [1 ]
机构：
[1] Univ Washington, Comp Sci & Engn, Seattle, WA 98195 USA
来源：
COMPUTER AIDED VERIFICATION (CAV 2017), PT II | 2017年 / 10427卷
关键词：
BIT-VECTORS; COMPLEXITY; SOLVER;
D O I：
10.1007/978-3-319-63390-9_13
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：238 / 258
页数：21
相关论文
共 50 条
  • [21] An arithmetic topos for integer matrices
    Hemelaer, Jens
    JOURNAL OF NUMBER THEORY, 2019, 204 : 155 - 184
  • [22] Using an induction prover for verifying arithmetic circuits
    Kapur D.
    Subramaniam M.
    International Journal on Software Tools for Technology Transfer, 2000, 3 (1) : 32 - 65
  • [23] Verifying and reflecting quantifier elimination for Presburger arithmetic
    Chaieb, A
    Nipkow, T
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 367 - 380
  • [24] Verifying Multithreaded Recursive Programs with Integer Variables
    Ben Rajeb, Narjes
    Nasraoui, Brahim
    Robbana, Riadh
    Touili, Tayssir
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 : 143 - 154
  • [25] Arithmetic transforms for verifying compositions of sequential datapaths
    Radecka, K
    Zilic, Z
    2001 INTERNATIONAL CONFERENCE ON COMPUTER DESIGN, ICCD 2001, PROCEEDINGS, 2001, : 348 - 353
  • [26] A NOTE ON PROBABILISTICALLY VERIFYING INTEGER AND POLYNOMIAL PRODUCTS
    KAMINSKI, M
    JOURNAL OF THE ACM, 1989, 36 (01) : 142 - 149
  • [27] Towards the verifying compiler
    Hoare, T
    FROM OBJECT-ORIENTATION TO FORMAL METHODS: ESSAYS IN MEMORY OF OLE-JOHAN DAHL, 2004, 2635 : 124 - 136
  • [28] Towards the verifying compiler
    Hoare, T
    FORMAL METHODS AT THE CROSSROADS: FROM PANACEA TO FOUNDATIONAL SUPPORT, 2003, 2757 : 151 - 160
  • [29] Lossless or Quantized Boosting with Integer Arithmetic
    Nock, Richard
    Williamson, Robert C.
    INTERNATIONAL CONFERENCE ON MACHINE LEARNING, VOL 97, 2019, 97
  • [30] A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
    Kremer, Gereon
    Corzilius, Florian
    Abraham, Erika
    COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING, CASC 2016, 2016, 9890 : 315 - 335
12345