Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 2 Jun 1993 17:10:56 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07693; Wed, 2 Jun 93 08:53:02 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from stroma.dcs.ed.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA07688; Wed, 2 Jun 93 08:52:52 -0700 Received: from godel.dcs.ed.ac.uk by dcs.ed.ac.uk id aa03393; 2 Jun 93 16:43 BST Message-Id: <4452.9306021543@godel.dcs.ed.ac.uk> Received: from kgg.localhost.dcs.ed.ac.uk by godel.dcs.ed.ac.uk; Wed, 2 Jun 93 16:43:17 +0100 To: info-hol@ted.cs.uidaho.edu Subject: Thesis available by FTP Date: Wed, 02 Jun 93 16:43:14 +0100 From: Kees Goossens The thesis "Embedding Hardware Description Languages in Proof Systems" by Kees Goossens at the Laboratory for Foundations of Computer Science, University of Edinburgh is now available by anonymous ftp. ftp machine: ftp.dcs.ed.ac.uk file name: pub/kgg/thesis.ps.Z Note that due to local thesis regulations the (300 page) file is in 12pt, 1.5 spacing. It may be printed two pages on one A4 page with no loss of readability (in fact, this is the format in which printed theses are distributed by the department). Abstract: The aim of this thesis is to investigate the integration of hardware description languages (\hdl s) and automated proof systems. Simulation of circuit designs written in an \hdl\ is an important method of testing their correctness. However, due to the combinatorial explosion of possible inputs it is not feasible to verify designs using simulation alone. Formal hardware verification, using a proof system, has tried to address this issue. Whilst some medium-sized designs have been (partially) verified, industrial take-up of formal methods has been slow. This is partly due to the use of specialised, non-standard notations employed in various formalisms. By embedding a hardware description language in a proof system we hope to clarify the semantics of the particular \hdl, and present a more standard interface to formal methodologies. We have given a new static structural operational semantics for a subset of the \ella\ hardware description language. The formal dynamic semantics of this subset is based on an existing informal model. We embedded the semantics of this \hdl\ in the \llambda\ higher-order logic proof system. The embedding allows meta-theoretical results to be proved about this and other semantics. It has been proved that the semantics computes the least fixed point solution of the circuit description. Another semantics which computes a more defined output has also been embedded, and the relationship between both semantics has been proved formally. A number of paradigms such as operational semantics based formal symbolic simulation, formal interactive (top-down and bottom-up) synthesis, formal hardware generators, proved correct transformations and traditional hardware verification are presented as small case studies. However, scaling up of the examples turned out to be difficult, and verification tended to be slow.