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; Wed, 12 Oct 1994 16:41:41 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA04050;
          Wed, 12 Oct 1994 09:35:37 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA04046;
          Wed, 12 Oct 1994 09:35:34 -0600
Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id IAA18903 
          for <info-hol@ted.cs.uidaho.edu>; Wed, 12 Oct 1994 08:28:53 -0700
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Wed, 12 Oct 1994 16:27:28 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <02727-0@i80fs2.ira.uka.de>;
          Wed, 12 Oct 1994 16:30:58 +0100
To: info-hol@cs.uidaho.edu
Subject: Re: Single Pulser/Spec of P.Windley
In-Reply-To: Mail from 'Phil Windley <windley@lal.cs.byu.edu>' dated: Wed, 12 Oct 1994 08:35:45 -0600
Date: Wed, 12 Oct 1994 16:30:56 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.729:12.10.94.15.30.59"@ira.uka.de>

Of course, a specification in higher order logic is the nicest one.
However, the verification can then only be done manually, and
if you consider the runtimes in a previous email of D. Shepherd,
then you will realize, that HOL can never compete with the
model checkers in terms of efficiency and usability.

Model checkers are base on very limited languanges such that they 
cannot be the solution for hardware verification.
A tactic like SMV_TAC would be nevertheless very helpful in HOL,
therefore I am going to implement something like that.

Klaus.