Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 26 Sep 1995 10:32:07 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA294344865; Tue, 26 Sep 1995 02:41:05 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA294194847; Tue, 26 Sep 1995 02:40:47 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 26 Sep 1995 09:40:05 +0100 X-Mailer: exmh version 1.6.1 5/23/95 X-Uri: To: Ching-Tsun Chou Cc: info-hol@leopard.cs.byu.edu, Richard.Boulton@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 09:39:58 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:081850:950926084016"@cl.cam.ac.uk> Ching-Tsun Chou writes: > Where can I get a copy of John Van Tassel's work on > formalizing VHDL in HOL? His PhD thesis can be found at URL: http://www.cl.cam.ac.uk/ftp/hvg/papers/JVTthesis/ > Also, are there other works on formalizing VHDL in > other theorem provers? Ralf Reetz and Thomas Kropf at Karlsruhe have been working on formalizing VHDL in HOL. The following paper contains a survey of related work: R. Reetz and T. Kropf "A flowgraph semantics of VHDL: Toward a VHDL verification workbench in HOL" Formal Methods in System Design, 7(1/2):73-99, August 1995. In fact, that whole issue is devoted to VHDL semantics. Richard. ------------------------------------------------------------------------------ Richard J. Boulton, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom Telephone: +44 (0)1223 334729, Fax: +44 (0)1223 334678 E-mail: Richard.Boulton@cl.cam.ac.uk, URL: http://www.cl.cam.ac.uk/users/rjb/ ------------------------------------------------------------------------------