AbstractsComputer Science

This thesis presents the results of investigating various logics with respect to their appli- cation to verification of digital hardware design. The approach highlights both the end- user aspects and the implementor’s aspects. The thesis is structured in 3 parts: part I discusses verification problems in the area of combinational circuits, part II focuses on sequential circuit verification, and part III pre- sents the software tools that have been developed and discusses details of their implemen- tations. Also, part III contains a number of test cases that exhibit the typical modelling of problems in terms of the investigated logics and shows how they are solved by the pre- sented tools: • bdd - a boolean function manipulation package • ptl - a temporal logic satisfiability checker • mu - a propositional -calculus tool • bsn2veri - a combinational circuit equivalence checker • bsn2mc - a Fair-CTL model checker This thesis focuses on techniques for hardware verification. The approach is formal, i.e., mathematical theories will be presented that form the basis for modelling the hardware and reasoning about its behaviour. The work concentrates on decidable theories, for which algorithms exist that can be used to prove certain properties of the circuit. Central to this thesis are the application of the theory and the development of efficient algorithms.