Equational Theorem Proving Methods for Hardware Verification
Gopale Shyamsunder Ramesh,
M.Tech,
1999,
69 pp.
Department of
Computer Science and Engineering
Indian Institute of Technology Bombay,
Powai, Mumbai 400 076.
Supervisor(s):
G. Sivakumar
Hardware Verification is the process of verifying the design of a circuit
formally. The goal of Hardware Verification is to prove that a circuit will
work correctly if the input and output constraints are met. Equational Theorem
Proving is a method of proving theorems using rewrite systems.
Equational methods have an advantage over other methods that we can
specify an incomplete specification and it can be completed automatically
with little user interaction. RRL
(Rule Rewrite Laboratory) is a theorem prover which
implements many of these techniques.
In this report we will have a look at various equational theorem
proving methods. Also we will look at the recent developments
in the field of hardware verification. We also document our
attempt to verify the single pulser using equational theorem proving methods.
We were able to verify one of the three properties
of the single pulser using RRL.