Rhishikesh Shrikant Limaye and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2010-67

May 13, 2010

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.pdf

<p>This thesis presents Beaver -- an efficient SMT solver for the quantifier-free fixed-size bit-vector logic (QF_BV). Beaver is an eager solver, that is, given an SMT formula, it first performs word-level simplications and then bitblasts the simplified formula to a Boolean formula, which is then solved using any SAT solver. Several engineering techniques are behind its efficiency: 1) efficient constant/constraint propagation using event-driven approach, 2) several word-level rewrite rules, 3) efficient bitblasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplication techniques of ABC logic synthesis system. </p> <p>In this thesis, we highlight the implementation details of Beaver that distinguishes it from other solvers. We also present an experimental evaluation and analysis of the effectiveness of our solver against all available QF_BV solvers on the SMT-LIB benchmark suite. </p> <p>Beaver is an open-source tool implemented in OCaml, usable with any back-end SAT engine, and has a well-documented extensible code base that can be used to experiment with new algorithms and techniques. </p>

Advisors: Sanjit A. Seshia

---

BibTeX citation:

@mastersthesis{Limaye:EECS-2010-67,
    Author= {Limaye, Rhishikesh Shrikant and Seshia, Sanjit A.},
    Title= {Beaver: An SMT Solver for Quantifier-free Bit-vector Logic},
    School= {EECS Department, University of California, Berkeley},
    Year= {2010},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.html},
    Number= {UCB/EECS-2010-67},
    Abstract= {<p>This thesis presents Beaver -- an efficient SMT solver for the
quantifier-free fixed-size bit-vector logic (QF_BV). Beaver is an
eager solver, that is, given an SMT formula, it first performs
word-level simplications and then bitblasts the simplified formula to
a Boolean formula, which is then solved using any SAT solver. Several
engineering techniques are behind its efficiency: 1) efficient
constant/constraint propagation using event-driven approach, 2)
several word-level rewrite rules, 3) efficient bitblasting to SAT, by
first converting to and-inverter-graph (AIG) representation and using
Boolean simplication techniques of ABC logic synthesis
system.
</p>
<p>In this thesis, we highlight the implementation details of Beaver
that distinguishes it from other solvers. We also present an
experimental evaluation and analysis of the effectiveness of our
solver against all available QF_BV solvers on the SMT-LIB benchmark
suite.
</p>
<p>Beaver is an open-source tool implemented in OCaml, usable with any
back-end SAT engine, and has a well-documented extensible code base
that can be used to experiment with new algorithms and techniques.
</p>},
}

EndNote citation:

%0 Thesis
%A Limaye, Rhishikesh Shrikant 
%A Seshia, Sanjit A. 
%T Beaver: An SMT Solver for Quantifier-free Bit-vector Logic
%I EECS Department, University of California, Berkeley
%D 2010
%8 May 13
%@ UCB/EECS-2010-67
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.html
%F Limaye:EECS-2010-67