RTL-datapath verification using integer linear programming

Satisfiability of complex word-level formulas often arises as a problem in formal verification of hardware designs de-scribed at the register transfer level (RTL). Even though most designs are described in a hardware description lan-guage (HDL), like Verilog or VHDL, usually this problem is solved in the Boolean domain, using Boolean solvers. These engines often show a poor performance for data path veri-fication. Instead of solving the problem at the bit-level, a method is proposed to transform conjunctions of bitvector equali-ties and inequalities into sets of integer linear arithmetic constraints. It is shown that it is possible to correctly model the modulo semantics of HDL operators as linear constraints. Integer linear constraint solvers are used as a decision procedure for bitvector arithmetic. In the imple-mentation we focus on verification of arithmetic properties of Verilog-HDL designs. Experimental results show con-siderable performance advantages over high-end Boolean SAT solver approaches. The speed-up on the benchmarks studied is several orders of magnitude.