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 10:56:01 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA01029;
          Wed, 12 Oct 1994 03:53:49 -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 AA01024;
          Wed, 12 Oct 1994 03:53:37 -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 CAA18267 
          for <info-hol@ted.cs.uidaho.edu>; Wed, 12 Oct 1994 02:46:31 -0700
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Wed, 12 Oct 1994 10:45:53 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <01782-0@i80fs2.ira.uka.de>;
          Wed, 12 Oct 1994 10:49:17 +0100
To: info-hol@cs.uidaho.edu
Subject: "Re: Single Pulser/Spec of D. Shepherd"
Date: Wed, 12 Oct 1994 10:49:15 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.784:12.10.94.09.49.22"@ira.uka.de>

D. Shepherd said:

|> Then the spec is
|> 
|> SPEC
|>    (AG ((!inp) -> AX(inp -> A [inp U out]))) &
|>    (AG (out -> AX (A [ !out WU !inp ] )))

Not exactly. 
The first part (AG ((!inp) -> AX(inp -> A [inp U out]))) does not
cover the fact, that  inp is also high when out becomes high.
This is important, otherwise the impuls of out could follow
a high-phase of inp.

The second part (AG (out -> AX (A [ !out WU !inp ] ))) does not
cover the following:
After out has gone high, it has to go low at the next point of
time and then it has to be low until the next rising edge of inp 
is detected. The above specification only states that out is low 
until inp goes low. 

Klaus