Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <199410121602.JAA19126@dworshak.cs.uidaho.edu>
From: Kathi Fisler <kfisler@cs.indiana.edu>
Subject: Re: Single Pulser
To: info-hol@cs.uidaho.edu
Date: Wed, 12 Oct 1994 11:02:14 -0500 (EST)
Cc: schneide@ira.uka.de, des@inmos.co.uk
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 2195

One comment and one question about the single-pulser discussion:

>--------------------
> Informal specification:
>--------------------
>The circuit has a boolean valued input and a boolean valued output. If the 
>input changes from 0 to 1 at time t0 and is 1 until time t1, but changes at
>time t1+1 to 0, then there must be exactly one point of time between t0
>and t1 (including t0 and t1) such that out=1.

As has already been pointed out, this specification missed the point
that the output should not be high when the input is low.  However,
there is a more general statement of the specification, as Steve
raised in the talk, as follows:

	There should only be one output pulse between each pair of
	rising edges on the input pulse.

Although this is not the approach taken in the original conference
paper, Steve and I have since verified the single pulser in SMV using
the following, more general, specification (this spec was proposed by
Albert Camilleri):

	SPEC
	  AG (rising_edge -> (AF (o))) &
	  AG (o -> AX (A[!o U rising_edge])) &
  	  AG (rising_edge -> (!o -> (AX A[!rising_edge U o])))

where a rising_edge occurs if the input is low at time t and high at
time t+1.

---

Secondly, what struck me as interesting about the spec

	SPEC
   	  (AG ((!inp) -> AX(inp -> A [inp U (inp & out)]))) &
   	  (AG (out -> AX (A [ !out WU !inp ] )))
	  (AG (!inp -> !out))

is that, if I'm reading this right, this reflects a component with the
following behavior (someone please correct me if I'm wrong):

	       ----------------
   inp         |              |
 	   -----              ----------
	                 ------
   out                   |    |
 	   ---------------     ---------

This is not a component that can be realized in physical hardware,
since we can't predict the drop on the input.  Assuming that you coded
up this specification (either in HOL or in SMV), what would you prove
about it?  If anyone has examples, I'd like to see them seeing as I'm
relatively new to using these tools for hardware verification.

Kathi

-- 
Kathi Fisler                                    kfisler@cs.indiana.edu

Visual Inference and Hardware Methods Laboratories, Indiana University