Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: Ching-Tsun Chou <chou@CS.UCLA.EDU>
Cc: info-hol@leopard.cs.byu.edu, Paul.Curzon@cl.cam.ac.uk
Subject: Re: VHDL
In-Reply-To: Your message of "Mon, 25 Sep 1995 12:21:07 PDT." <199509251921.MAA20398@pelican.cs.ucla.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Tue, 26 Sep 1995 13:03:04 +0100
From: Paul Curzon <Paul.Curzon@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:180500:950926120337"@cl.cam.ac.uk>


>> Also, are there other works on formalizing VHDL in
>> other theorem provers?

>Yes.  I believe that some work has been done with the Boyer-Moore system,
>among others.  Can anyone be more precise?

David Russinoff has done some work on VHDL with the Boyer-Moore System:

Specification and Verification of Gate-level VHDL Models of
Synchronous and Asynchronous Circuits
David Russinoff
in Specification and Validation Methods edited by Egon B\"orger. Oxford 
Science Publications, 1995. 

The same book contains another paper on VHDL which uses model checking for 
verification:
Specification and Verification of VHDL-based System-level Hardware Designs
Werner Damm, Bernhard Josko and Rainer Schl\"or


Paul.

-----------------------------------------------------------------------
Paul Curzon, University of Cambridge Computer Laboratory,
New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom.
Telephone: +44 1223 334688, Fax: +44 1223 334678
Email: Paul.Curzon@cl.cam.ac.uk, URL: http://www.cl.cam.ac.uk/users/pc/