Tool for Mechanized Design Verification
Shah Manish Vardhilal,
M.Tech,
1999,
62 pp.
Department of
Computer Science and Engineering
Indian Institute of Technology Bombay,
Powai, Mumbai 400 076.
Supervisor(s):
G. Sivakumar
In spite of the recent progress in formal verification of circuit
designs, there exists a big gap between the hardware designers and the
people who conduct formal verification. This gap caused due to the lack
of a common specification language widens with the increase in complexity
of circuits being designed. To solve this problem, we choose VHDL, a
standard hardware design language and enrich it properly so that the
designer and the verifier have a common platform to design and verify
circuits. We develop a denotational semantics for a subset of VHDL and
based on this semantics, implement a prototype translator which translates
a VHDL design into logic formulae. The logic formulae are then input to
the theorem prover which, with some assistance from the user proves the
required theorems.