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: <9410132121.AA06135@gslxsrv.rose.hp.com>
Subject: Re: Single Pulser (reply to Victor)
To: info-hol@cs.uidaho.edu (info-hol)
Date: Thu, 13 Oct 94 14:21:41 PDT
Cc: sjohnson@cs.indiana.edu
In-Reply-To: <199410131455.KAA01725@air52.larc.nasa.gov>; from "Victor A. Carreno" at Oct 13, 94 10:55 am
Mailer: Elm [revision: 70.85]

> >As has already been pointed out, this specification missed the point
> >that the output should not be high when the input is low.
> 
> was indeed misinterpreted by me. However, the point is stil valid. What
> Kathi meant is that the specification should not describe a behaviour where
> an output pulse is generated when there is not a rising edge. That is, if
> there is never a rising edge, there should never be an output pulse. The
> specification:

Yes, the given spec would permit a single pulse to be generated before
any rising edge happened. If this is undesired, then the spec would need to be
strengthened.

But now this leads to another interesting twist!

What is the interpretation of the situation when the input starts off as high?
Is this classed as a rising edge? Strictly speaking, not. And certainly not
according to our definition of rising edge,
	i.e. risingEdge(t+1) := ~i(t) & i(t+1)

But the proposed implementation would drive an output pulse on the falling
edge of i, and so an o would be observable before any "rising edges"!
	_____
i	    |_____
	     _
o	____| |

Conversely, an implementation which pulsed exactly on the rising edge would
"miss" a pulse for the first time i was high:
	____	   ___
i           |_____|
	           _
o       __________| |

To address this, we could say that o should only go high in response to an
input (as opposed to rising edge). But then we run into implementation
problems, and the definition of neighbourhood (time between successive rising
edges) becomes a little woolly.

Simpler would be to again constrain the behaviour on the input (i.e. force it
to start at 0) and to provide the spec for well-behaved input only (remember we
already made a constraint on the input that it would not stay in the same
state forever).

Then we could add one more line to strengthen the SPEC which would say that
if the output is high, then a rising edge must have happened, now or sometime
in the past:

	SPEC	AG (o -> (risingEdge | pastRisingEdge))

where we can define pastRisingEdge as a FSM as follows:

VAR     pastRisingEdge : boolean;

ASSIGN  init (pastRisingEdge) := 0;
	next (pastRisingEdge) :=
	     case risingEdge	 : 1;
		  o	     	 : 0;	-- can omit this line if only worried
		  			-- about initialisation.
		  1 : pastRisingEdge;
	     esac;

Of course, some redundancy might now have been introduced wrt the previous
specs. I can't afford the time to think about optimising it. But a potential
overall SMV solution might look as follows (note the change on the definition
of i, forcing it to start at 0).

-----------------------------------------------------------

MODULE	main

VAR	i : boolean;

ASSIGN	init (i) := 0;			-- initialise input to 0, then
	next (i) := {0,1};		-- non-deterministically 0 or 1.

VAR	i1 : boolean;			-- previous value of i, ie. pi(t+1) = i

ASSIGN	init (i1) := 0;
	next (i1) := i;

VAR	pastRisingEdge : boolean;

ASSIGN	init (pastRisingEdge) := 0;
	next (pastRisingEdge) :=
	     case risingEdge : 1;	-- rising edge has happened.
		  o          : 0;	-- output clears last rising edge.
		  1 : pastRisingEdge;	-- retain state.
	     esac;

DEFINE	o := i1 & !i;			-- implementation of single pulser.
					-- (equivalent to input falling edge!)
--DEFINE o := risingEdge;		-- alternative implementation.
					-- (equivalent to input rising edge)

DEFINE	risingEdge := i & !i1;		-- input rising edge.

FAIRNESS risingEdge			-- constrain input to "rise and fall"

SPEC	AG (risingEdge -> (AF o))
SPEC	AG (o -> (AX (A [!o U risingEdge])))
SPEC	AG (risingEdge -> (!o -> (AX (A [!risingEdge U o]))))
SPEC	AG (o -> (risingEdge | pastRisingEdge))

---------------------------------------------------------------------

Cheers
--Albert

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