Computer Engineering Cider Seminars

In past solvers for Boolean satisfiability (SAT solver) have become great success in dozens of areas as for example formal verification, automatic test pattern generation or logic synthesis. A reason for that was the development of several sophisticated SAT techniques as e.g. learning, efficient implications strategies and branch heuristics. However, common SAT solvers work on the Boolean level. Due to the increasing complexity of the considered problems (e.g. exponential growth of the design sizes in circuit verification) in the last years several approaches have been studied which lift the solve engine to higher levels of abstractions. Thus, a new generation of SAT solvers - namely word-level solvers and SAT modulo theories (SMT) - have been introduced. The talk gives a survey of the different kinds of SAT-like proof techniques. The main concepts of engines exploiting word-level descriptions or specialized theory solvers are introduced. In particular the word-level solver SWORD (SAT-like word level solver) is described. Applications in circuit verification and logic synthesis show how higher abstractions can be utilized during the solve process.

Robert Wille received his Diploma degree in computer science from the University of Bremen, Bremen, Germany in 2006. Since November 2006 he is pursuing the Ph.D. degree at the University of Bremen. His research interests include formal methods, verification and logic synthesis.