WoLFram - A Word Level Framework for Formal Verification and its Application

In this thesis a framework for the generic development of formal applications that are independent of the underlying proof technique, called WoLFram (Word Level Framework), is presented. The framework is partitioned into an application layer, a core engine and a solver back-end. The motivation for this is on the one hand the easy adaptation of existing methods for new proof techniques. On the other hand, by building new applications on top of core data structures, both, the parsing front-ends and the solver back-end, can be reused. In this way, for a new algorithm there are a number of input languages (like SystemC [Syn08] and Verilog TM [Ver93]) and numerous state-of-the-art solvers directly available. WoLFram supports the design flow by providing applications on different level of abstraction. The input of WoLFram is a word level netlist (wlnetlist) that contains Boolean as well as word level operations. Synthesis tools for SystemC, Verilog TM , and Blif [Ele93] are available. Integrated applications are ranging from simulation, property checking and equivalence checking to algorithms for analyzing coverage, debugging and computing robustness. For each of these applications, several proof engines are available, in particular solvers for Boolean SAT, Pseudo Boolean SAT (PBS) as well as word level techniques, like SMT or Constraint Satisfaction Problem (CSP). WoLFram allows for a fair and easy evaluation of proof techniques to find the best suited solving paradigm for newly developed applications. Even for a single application it may be useful to apply alternative proof techniques on different types of designs.