Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Thu, 5 Mar 92 15:11:33 GMT
From: John.Van-Tassel@uk.ac.cam.cl
Message-Id: <9203051511.AA00715@scoter.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted
Subject: VHDL Formalisation

This note is to announce the publication of University of Cambridge
Technical Report 249.  Interested parties should contact me at the
address in the .sig for copies.   The title and abstract are as follows:


           A Formalisation of the VHDL Simulation Cycle

                      John P. Van Tassel


   ABSTRACT:  The VHSIC Hardware Description Language (VHDL) has been
   gaining wide acceptance as a unifying HDL.  It is, however, still a
   language in which the only way of validating a design is by careful
   simulation.  With the aim of better understanding VHDL's particular
   simulation process and eventually reasoning about it, we have
   developed a formalisation of VHDL's simulation cycle for a subset of
   the language.  It has also been possible to embed our semantics in the
   Cambridge Higher-Order Logic (HOL) system and derive interesting
   properties about specific VHDL programs.

------------------------------------------------------------------------------
John Van Tassel                 |  Tel: +44-223-334729
Univ. of Cambridge              |  Fax: +44-223-334678
Computer Laboratory             |
Pembroke Street                 |  Email: jvt@cl.cam.ac.uk
Cambridge CB2 3QG               |
England                         |