Re: VHDL, HOL

[thery@capa.inria.fr (Laurent Thery)]

>> We are currently working on "Formal Specifications" for Hardware design.
>> We have already been working on VHDL, developping a parser with Centaur and
>> we are
>> looking for more informations on HOL, CHOL, HOL & VHDL ....
>>
>> Could someone indicate to me, some pointers to these topics.

o HOL is a theorem prover initially developed at Cambridge  by Mike Gordon.
   HOL has been largely applied  to hardware verification (VHDL, ELLA etc..)  

   A  html pointer  for HOL is:
   http://lal.cs.byu.edu/lal/hol-documentation.html

   If you are interested in  papers, you can have a look at the proceedingss of their conference:
                       HOL: Higher Order Logic and its applications
   (the last two proceedings have been published as LNCS).

o CHOL is an interface for HOL that I've been developped using some components
   of the Centaur system. It only supports proof management.

   A html pointer for CHOL is:
   http://www.inria.fr/croap/chol/chol.html

o HOL & VHDL: an embedding of a subset of VHDL in HOL has been done 
   by John Van Tassel for his thesis. It is available as a Cambridge technical report 
   or by ftp:

   ftp://ftp.cl.cam.ac.uk/hvg/papers/JVTthesis/

   a shorter version has been published in the HOL conf in Lewen in 1992. 

-- 
Laurent Thery     Phone (33) 93 65 78 16 e-mail thery@inria.fr
Projet Croap INRIA - Sophia Antipolis,
2004, rte des Lucioles, 06565 Valbonne Cedex, FRANCE