BV Constraints Solving Using SAT-based Model Checking

Solving Constraints over BV with SAT-based MC Alexander Nadel Sharad Malik Yakir Vizel Princeton University Intel, Israel Princeton University

SMT Formula over a theory T SMT Solver for T SAT UNSAT 3

BVMC Formula in QF_BV (LIA subset) Reduce to Safety Verification SMT Solver for T Model Checker UNSAFE SAFE SAT UNSAT 4

QF_BV Defined by the following grammar: ? = ???? ????? ? ? ? ? ? ? ???? ????|???(?1,?2,?3) ???? = ? ? ?(????,????)|? ????,? |???????(????,?,?)|???(?,????,????) Where: {<, ,>, ,=} F {+, , , , shl, shr, concat, &, |, } G {sign_extend, zero_extend}

QF_BV: LIA subset Defined by the following grammar: ? = ???? ????? ? ? ? ? ? ? ???? ????|???(?1,?2,?3) ???? = ? ? ???? + ????|???? ????|? ????|???(?,????,????) Where: {<, ,>, ,=} - Currently, BVMC works for one width for all the BV variables - Can be easily extended to arbitrary widths - BVMC also supports all the bit-wise operators

Example Consider the following formula where x,y,z are bit-vectors of size 4: ? = (? = ? + ?) (? > 0) (? > 0) (? < 0) A traditional BV solver encodes this formula to SAT by means of bit-blasting: A full-adder: FA(a, b, s, ci, co) ?) ??(?1,?1,?1,?0 ((?3= 0) (?0 ?1 ?2)) ((?3= 0) (?0 ?1 ?2)) (?3= 1) ?,?0 ?,?1 ?) ??(?2,?2,?2,?1 ?,?2 ?) ??(?3,?3,?3,?2 ?,?3 ?) ??(?0,?0,?0,?0

Example ?) ??(?1,?1,?1,?0 ((?3= 0) (?0 ?1 ?2)) ((?3= 0) (?0 ?1 ?2)) (?3= 1) ?,?0 ?,?1 ?) ??(?2,?2,?2,?1 ?,?2 ?) ??(?3,?3,?3,?2 ?,?3 ?) ??(?0,?0,?0,?0 x0 y0 x1 y1 x3 y3 x2 y2 FA FA FA FA z0 z1 z2 z3

Reduction to Safety Verification 9

Width Time x0 y0 x1 y1 x3 y3 x2 y2 FA FA FA FA z0 z1 z2 z3

Width Time Treat bit-vectors as streams of bits over time Starting from the LSB The i-th bit is available at the i-th clock cycle xi yi co FA zi

Comparators a = b: bits should be equal at every cycle Sequential circuit: track all bits up to this point Monotonic: once 0, always 0 x a b & =

Comparators a < b: the sign bit changes at each cycle Sequential circuit: unsigned comparison ULT: ( a b) [ (a b) x] Combinational circuit: take care of the sign bit x a b ULT a b 1 MUX 0 a b

Reduction to Safety Verification A formula ? is translated to a sequential circuit C Assume ? is a DAG: For each leaf of sort bit-vector create an input terminal For each leaf of sort Boolean, create an uninitialized latch x x = x For a leaf of a constant type use a counter The counter determines the cycle For each cycle the value is known a-priori Boolean operations the corresponding logical gates Arithmetic operations and comparators sequential circuit Multiplication by a constant shift-lefts and additions The output of C is assigned to true when ? is satisfiable 14

Reduction to Safety Verification Find the maximal number of bits required to represent constants in ? - kmin ? is not well defined for k < kmin When creating the property, add a guard wmin wmin is initialized to false and becomes true after kmin cycles The property Bad := wmin C.output() 15

BVMC: the Model Checking- based Algorithm 16

Safety Verification A transition system T=(V, INIT, Tr, Bad) T is UNSAFE if and only if there exists a path in T from a state in INIT to a state in Bad, or if ? 1 ? ?,? = ????(?0) ?? ??,??+1 ???(??) ?=0 T is SAFE if and only if there exists a safe inductive invariant Inv s.t. ???? ??? ??? ? ?? ?,? ??? ? ??? ???

SAT-based Model Checking (SATMC) Search for a counterexample for a specific length Bounded Model Checking (BMC) Checking satisfiability of ?(T,N) If a counterexample does not exist, generalize the bounded proof into a candidate Inv Check if Inv is a safe inductive invariant 18

BMC vs. Traditional BV Solvers Time correlates to width Unrolling depth therefore correlates to width x y co FA z 19

BMC and Traditional BV Solvers Time correlates to width Unrolling depth therefore correlates to width x0 y0 x1 y1 x3 y3 x2 y2 FA FA FA FA z0 z1 z2 z3 20

BMC and Traditional BV Solvers Time correlates to width Unrolling depth therefore correlates to width BMC till target depth Eager BV Solver 21

Generalization - UNSAT If ? is UNSAT when interpreted over bit-vectors of width k Can we generalize this result for bit-vectors of width N > k? 22

Generalization - UNSAT If ? is UNSAT when interpreted over bit-vectors of width k Can we generalize this result for bit-vectors of width N > k? Free lunch for us : the ability of a MC to generalize a bounded proof to an unbounded proof When finding an inductive invariant at depth k, ? is UNSAT for all N > k 23

Generalization - SAT If ? is SAT when interpreted over bit-vectors of width k Can we generalize this result for bit-vectors of width N > k? 24

Generalization - SAT ? = (? = ? + ?) (? > 0) (? > 0) (? < 0) For k=2, a satisfying assignment: x=1, y=1, z=-2 x=01, y=01, z=10 For k=3, a satisfying assignment: x=3, y=3, z=-2 x=011, y=011, z=110 For k=4, a satisfying assignment: x=7, y=7, z=-2 x=0111, y=0111, z=1110 25

Extending a satisfying assignment If ? is SAT when interpreted over bit-vectors of width k Then, ?(T,k) is satisfiable There exists a counterexample of length N Satisfying assignment ? Try to extend it incrementally ?(T,k+1) ? If extension of ? works till the target depth SAT Otherwise continue without ? from the current depth Other strategies are also possible 26

Experiments 27

Implementation LIAMC: supports all bit-wise operation and the LIA subset of QF_BV Implemented on top of ABC and open source SMT-LIB parser Benchmarks translated all the LIA benchmarks to QF_BV Using varying bit-vector widths: 32, 64, and 128 28

29

30

900 Boolector? 32bit 800 Z3? 32bit LIAMC? 32bit 700 600 Runtime? [s] 500 400 300 200 100 0 0 500 1000 1500 31

900 Boolector? 64bit 800 Z3? 64bit LIAMC? 64bit 700 600 Runtime? [s] 500 400 300 200 100 0 0 500 1000 1500 32

900 Boolector? 128bit 800 Z3? 128bit LIAMC? 128bit 700 600 Runtime? [s] 500 400 300 200 100 0 0 500 1000 1500 33

Related Work Fr hlich, Kov sznai, Biere, Efficiently solving bit-vector problems using model checkers , SMT 13 Solves a restricted subset of QF_BV with BDD-based model checking Bitwise operators, addition, subtraction, shift by one, indexing and comparators Translates the formula to a circuit Keeps a guard counter to verify the formula only at the target depth Our contribution: The guard counter is not required! Generalization to higher widths for SAT and UNSAT Support multiplication by a constant 34

Future Work More QF_BV operators: Sign/zero extension and extraction can be added fairly easily Non-linear: multiplication, division, shl/shr by variable Recall yesterday's talk by Alberto Griggio on linearization Improve UNSAT performance Dedicated MC algorithms? Better scalability for LIA Our method works can be extended to LIA Paper accepted to FMCAD 17 Less efficient than LIA solvers overall, but solves instances none can solve 35

Conclusion A novel decision procedure for an important subset of QF_BV: LIA subset Important in the context of SW/HW validation Superior to state-of-the-art BV solvers on satisfiable instances Unsatisfiable instances: work-in-progress Working on extending the support for QF_BV 36

Thank you for your attention 37

Backup 38

Reduction to Safety Verification A formula ? is translated to a sequential circuit C Assume ? is a DAG 39

Extending a satisfying assignment ? a counterexample of length k 40