Date: Tue, 12 Mar 91 14:12:13 GMT
From: Mike Gordon <mjcg%com.sri.cam@com.sri.ai>
Message-Id: <9103121412.AA06094@harlech.cam.sri.com>
To: info-hol@edu.uidaho.cs.ted
Cc: mjcg <mjcg%com.sri.cam@com.sri.ai>
Subject: Position available at Cambridge


The University of Cambridge Hardware Verification Group is looking
for a researcher to work on a new project exploring the semantics of
VHDL.  The project is expected to last at least two years beginning in
September 1991.

The project will involve the use of higher order logic in formalising
the semantics of VHDL.  Since VHDL is a simulation language, a
significant effort will be spent on specifying the simulation cycle
and timing model employed.  It is expected to couple this research
with the development of a tractable subset of the language suitable
for real designs, as well as a suite of proof tools to allow for
easier reasoning about the language within the HOL system.

It is expected that the work on VHDL will closely interact with other
research at Cambridge on supporting embedded languages in HOL.
A project to apply theorem-proving to ELLA designs is already in
progress and has produced syntax processing tools that will be used
for VHDL. The SAFEMOS project, which is joint with SRI, Inmos, Oxford
University and Cambridge University is already exploring the embedding
of VHDL in HOL and it is hoped the new researcher will interact with
the SAFEMOS team.

Interested parties should contact me (mjcg@cl.cam.ac.uk) for further
information. However, since I expect to be away quite a lot during the
next few months, please CC any messages to John Van Tassel (jvt@cl.cam.ac.uk).

                                                                  Mike Gordon
                                                                 March 12 1991