Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 14:19:49 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA031769870;
          Tue, 26 Sep 1995 06:51:10 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from cat.syr.edu (chin.cat.syr.EDU) by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA031629857;
          Tue, 26 Sep 1995 06:50:57 -0600
Date: Tue, 26 Sep 95 08:50:53 EDT
From: chin@cat.syr.EDU (Shiu-Kai Chin)
Received: by cat.syr.edu (4.1/1.0-6/5/90) id AA01962;
          Tue, 26 Sep 95 08:50:53 EDT
Message-Id: <9509261250.AA01962@cat.syr.edu>
To: info-hol@leopard.cs.byu.edu
Subject: VHDL


Odyssey Research Associates has a Larch/VHDL system (and a Larch/ADA system)
which uses their Penelope prover.  Penelope has a nice user interface,
(alas, no tactic language), and is usable by engineers.  We have used
it at SU to teach verification.

You can contact Damir Jamsek at ORA to find out more.

 damir@oracorp.com

--Shiu-Kai Chin