Neue Beweistechniken für die Eigenschaftsprüfung von arithmetischen Datenpfaden

The increasing complexity of modern SoC designs makes tasks of SoC formal verification a lot more complex and challenging. This motivates the research community to develop more robust approaches that enable efficient formal verification for such designs. It is a common scenario to apply a correctness by integration strategy while a SoC design is being verified. This strategy assumes formal verification to be implemented in two major steps. First of all, each module of a SoC is considered and verified separately from the other blocks of the system. At the second step – when the functional correctness is successfully proved for every individual module – the communicational behavior has to be verified between all the modules of the SoC. In industrial applications, SAT/SMT-based interval property checking(IPC) has become widely adopted for SoC verification. Using IPC approaches, a verification engineer is able to afford solving a wide range of important verification problems and proving functional correctness of diverse complex components in a modern SoC design. However, there exist critical parts of a design where formal methods often lack their robustness. State-of-the-art property checkers fail in proving correctness for a data path of an industrial central processing unit (CPU). In particular, arithmetic circuits of a realistic size (32 bits or 64 bits) – especially implementing multiplication algorithms – are well-known examples when SAT/SMT-based formal verification may reach its capacity very fast. In cases like this, formal verification is replaced with simulation-based approaches in practice. Simulation is a good methodology that may assure a high rate of discovered bugs hidden in a SoC design. However, in contrast to formal methods, a simulation-based technique cannot guarantee the absence of errors in a design. Thus, simulation may still miss some so-called corner-case bugs in the design. This may potentially lead to additional and very expensive costs in terms of time, effort, and investments spent for redesigns, refabrications, and reshipments of new chips. The work of this thesis concentrates on studying and developing robust algorithms for solving hard arithmetic decision problems. Such decision problems often originate from a task of RTL property checking for data-path designs. Proving properties of those designs can efficiently be performed by solving SMT decision problems formulated with the quantifier-free logic over fixed-sized bit vectors (QF-BV). This thesis, firstly, proposes an effective algebraic approach based on a Gröbner basis theory that allows to efficiently decide arithmetic problems. Secondly, for the case of custom-designed components, this thesis describes a sophisticated modeling technique which is required to restore all the necessary arithmetic description from these components. Further, this thesis, also, explains how methods from computer algebra and the modeling techniques can be integrated into a common SMT solver. Finally, a new QF-BV SMT solver is introduced