Cooperative Bounded Model Checking Using STE and Hybrid Three-Valued SAT Solving

This paper presents a cooperative bounded model checking (BMC) method for RTL designs. The method firstly extends the Boolean DPLL algorithm into a unified procedure to solve hybrid satisfiability problems for RTL circuits, and then changes this solver to a hybrid three-valued SAT solver. Symbolic trajectory evaluation (STE) assertions are transformed to a three-valued problem combining the expansion method in BMC and the abstraction of STE. The experimental results comparing with ordinary BMC which based on an ordinary hybrid SAT solver demonstrate the efficiency of our approach