Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <26228-0@swan.cl.cam.ac.uk>; Wed, 18 Mar 1992 16:21:41 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26117; Wed, 18 Mar 92 07:02:10 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from Sunset.AI.SRI.COM by ted.cs.uidaho.edu (16.6/1.34) id AA26113; Wed, 18 Mar 92 07:02:06 -0800 Received: from cam.sri.com by Sunset.AI.SRI.COM (4.1/SMI-4.1) id AA06187 for info-hol@ted.cs.uidaho.edu; Wed, 18 Mar 92 07:05:39 PST Received: from chepstow.cam.sri.com by cam.sri.com (4.1/4.16) id AA25058 for info-hol@ted.cs.uidaho.edu; Wed, 18 Mar 92 15:04:34 GMT Received: by chepstow.cam.sri.com (4.1/4.16) id AA21011 for info-hol@ted.cs.uidaho.edu; Wed, 18 Mar 92 15:04:31 GMT Date: Wed, 18 Mar 92 15:04:31 GMT From: Mike Gordon Message-Id: <9203181504.AA21011@chepstow.cam.sri.com> To: info-hol@edu.uidaho.cs.ted Subject: Embedding HDLs in HOL TPCD92 Paper ------------ The following paper, which will be presented at TPCD92 by Mike Gordon, is available by anonymous FTP from ftp.cl.cam.ac.uk. It is EmbeddingPaper.ps.Z in the directory hol. For more details about TPCD92 send email to: germaine@cs.kun.nl. Please send any comments on the paper to Mike Gordon (mjcg@uk.ac.cam.cl). He will try to take account of any feedback in the talk. TITLE: Experience with embedding hardware description languages in HOL AUTHORS: Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, John Van Tassel University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge, CB2 3QG England ABSTRACT The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.