[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Automating proofs

Hi Tamarah Arons,

A number of people (David Cyrluk, Harald Ruess, etc., including
myself) at SRI have undertaken a number of hardware verification
efforts.  The examples we have looked at have ranged from small, but
paradigmatic in nature, to medium to large and real microprocessor
designs.  Generally speaking, verification in the hardware area is
amenable for more automation using PVS than most other applications.
The degree of automation you can achieve depends, of course, on a
number of factors.

(1) The level of representation: Is the design at gate,
register-transfer, or architecture levels?  Verifications at gate and
register-transfer levels are more automatic than at other levels.

(2) The specification against which the design is being compared.  For
example, verifying a multiplier or divider circuit against its arithmetic
specification is less automatic than a more logic-oriented verification.

(3) But most importantly, the style of specifying the design in PVS
very much influences the level of automation you can get.  Through
experimentation we have arrived at a few different styles of
specification that allow us to achieve a high level of automation in
most of our hardware verification exercises.

To get more details about our work in hardware verification, please
visit our Formal Methods page at www.csl.sri.com and go to the "our
papers" section.  In a separate message, I will mail you references to
some of the tutorials we have written on hardware verification.  In
the meantime, if I can be of some help to you with your current
examples, let me know by giving more information about your examples.

Sincerely yours