Abstract

Hardware verification is the process of verifying whether a system behaves as described by its specification. This report is based on the study of various techniques used in hardware verification. We studied three decision procedures viz., model checking, bit-vector arithmetic and linear arithmetic, that can be included in a theorem-prover to help automatic verification. While mechanizing proofs by induction, a crucial problem that often needs to be addressed is to decide on an induction scheme that leads to an appropriate induction hypothesis to carry out the proof. Cover set induction method using linear arithmetic is used for automation of such proofs. Experience with verification of commercial microprocessors has shown that the lack of specialized decision procedures for bit-vectors is the main impediment to effective automation in theorem proving techniques. Model checking builds a finite model of the system to verify its properties. But this may lead to state explosion problem and therefore advanced data structures like BMDs are used. We propose to work on integration of these three decision procedures in existing theorem provers and see how useful it is in verification of sample circuits.