Logics for digital circuit verification : theory, algorithms, and applications
Gljm Geert Janssen · TU/e Research Portal · 1999
This thesis presents the results of investigating various logies with respect to their application 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 verifieation problems in the area of combinational circuits, part II focuses on sequentia!circuit verification, and part III presents the software tools that have been developed and discusses details of their implementations.Also, part III contains a number of test cases that exhibit the typieal modeHing of problems in terms of the investigated logies and shows how they are solved by the presented tools: • bdd -a boolean function manipulation package • ptl-a temporallogic satisfiability checker • mu -a propositional .u-calculustool • bsn2veri -a combinational circuit equivalence checker • bsn2mc -a Fair-CTL model checkerThis thesis focuses on techniques for hardware verification.The approach is formal, i.e., mathematica!theories will be presented that form the basis for mod-eHing the hardware and reasoning about its behaviour.The work concentrates on decidabie 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.