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.