Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Albert Camilleri <ac@gslxsrv.rose.hp.com>
Message-Id: <9410122304.AA02779@gslxsrv.rose.hp.com>
Subject: Re: Single Pulser (reply to Victor)
To: info-hol@cs.uidaho.edu (info-hol)
Date: Wed, 12 Oct 94 16:04:11 PDT
In-Reply-To: <199410122106.RAA01450@air52.larc.nasa.gov>; from "Victor A. Carreno" at Oct 12, 94 5:06 pm
Mailer: Elm [revision: 70.85]

Reply to Victor Carreno's memo:


> >As has already been pointed out, this specification missed the point
> >that the output should not be high when the input is low.

As I understood the spec defined in the lecture, the requirement was that the
output pulsed in response to a rising edge, before the next rising edge
happened. This was defined as a "neighbourhood".

		_________	_____
i	________|	|_______|

neighbourhood	^---------------^

So I can't understand why the output cannot be high when the input is low.
Unless I misunderstood the spec, or the above statement.

> >This is not a component that can be realized in physical hardware,
> >since we can't predict the drop on the input.

Maybe, but it can still happen in practice.

> That is because the specification can not guarantee both:
> - that the circuit will produce a pulse for every rising edge
> 
> &
> 
> - that the output is low when the input is low
> 
> *unless you demand instantaneous response*

Care is required here. Specifications are not intended to guarantee anything.
Specifications are intended to capture intended behaviour and could be anything
we wish them to be. Whether they are implementable, i.e. whether a description
of an implementation meets that specification, is a different issue!

> The specification by Albert Camilleri does not make the output low when the
> input is low.

It shouldn't.

> Consider the following sequence. (0 = false, 1 = true)
> 
> state step   0 1 2 3 4 
> inp          0 1 0 1 0 
> o            0 0 1 0 1 
> rising_edge  0 1 0 1 0 
> 
> by: AG (rising_edge -> (!o -> (AX A[!rising_edge U o])))
> 
> output 'o' has to be 1 at state step 2 since at step 3 rising_edge is 1.

No. As far as I am aware, AG (risingEdge -> (AF o)) allows risingEdge and o to
be true at the same time. (AF o) means o must be true at least once on every
path of the tree following from the current node. This does not preclude o
from being true at the current node!

This is why I wrote
	AG (rising_edge -> (!o -> (AX A[!rising_edge U o])))
instead of
	AG (rising_edge -> (AX A[!rising_edge U o]))

The latter does not cover the case when o goes high on risingEdge (remember
the definition of "neighbourhood"). In this case a rising edge will keep
waiting for an output which has already happened!

To implement a pulser where the output went high on the rising edge (instead
of on the falling edge as in the paper) of the input, all that needs to be
done is to put the inverter on the state rather than on the direct input.
Of course, there might be electrical reasons why this would not be
advisable, but I don't know about these ;-).

> in fact, Albert's specification can be reduced to: 
> 
> SPEC
> 	  AG (rising_edge -> (AF (o))) &
> 	  AG (o -> AX (A[!o U rising_edge])) &
>   	  AG (rising_edge -> (AX A[!rising_edge U o]))
> 
> since output 'o' is always 0 when rising_edge is 1.

I don't think so (unless I'm missing something), see above.

--Albert

-----------------------------------------------------------------
|  Albert J Camilleri		|				|
|  Hewlett-Packard Company	|				|
|  Systems Technology Division	|  Tel  : +1 916 785 8488	|
|  Mailstop R5/EF		|  Fax  : +1 916 785 3096	|
|  8000 Foothills Boulevard	|  Email: ac@hprpcd.rose.hp.com	|
|  Roseville, CA 95747		|				|
|  USA				|				|
-----------------------------------------------------------------