Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <22923-0@swan.cl.cam.ac.uk>; Mon, 6 Apr 1992 23:08:57 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07517;
          Mon, 6 Apr 92 14:51:58 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from ULTRASTAR.EE.CORNELL.EDU by ted.cs.uidaho.edu (16.6/1.34) 
          id AA07513; Mon, 6 Apr 92 14:51:46 -0700
Date: Mon, 6 Apr 92 17:51:34 -0400
From: markaa@EDU.CORNELL.EE.ultrastar (Mark D. Aagaard)
Received: by ultrastar.EE.CORNELL.EDU (5.65+IDA-1.3.5+christos-1/1.6.10+n-y-Cornell-Electrical-Engineering) 
          id AA10355; Mon, 6 Apr 92 17:51:34 -0400
Message-Id: <9204062151.AA10355@ultrastar.EE.CORNELL.EDU>
To: info-hol@edu.uidaho.cs.ted
Subject: interfacing thm provers and other circuit "verifiers"


In ICCAD '90 there is a paper describing some work done at Fujitsu
with interfacing HOL and a BDD tool. The general idea was to use HOL 
to do high level reasoning in a temporal logic, and then use the 
BDD tool to quickly perform Boolean functions. Does anyone know more 
details about this work, or have any information about other work
which has combined "informal" verification and theorem proving
verification?


author	= {M. Fujita, Y. Matsunaga, T. Kakuda},
title	= {Automatic and semi-automatic verification of
		switch-level circuits with {T}emporal 
		{L}ogic and {B}inary {D}ecision {D}iagram},
booktitle = {International Conference on Computer Aided Design},
year	= {1990},
organization = {ACM/IEEE},
pages	= {38--41}


 thanks,
   mark aagaard
   markaa@ee.cornell.edu