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. WoLFram supports the design flow by providing applications on different level of abstraction.
The input of WoLFram is a word level netlist that contains Boolean as well as word level operations. Synthesis tools for hardware description languages like SystemC and Verilog 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 Satisfiable Modulo Theories (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.
In focus of this thesis are applications that support an engineer in pre-processing and post-processing of verification. Applications for synthesis, debugging, and robustness computation are presented, discussed, and empirically evaluated with the focus on hardware designs. Additional studies on the verification of software running on Programmable Logic Controllers (PLCs) show the overall stability and applicability of WoLFram on industrial problems.
Overall, WoLFram provides a stable and extensible framework for formal applications and allows the usage and the development of formal applications.
