Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <8017.9410120815@frogland.inmos.co.uk>
Subject: Re: Single Pulser
To: schneide@ira.uka.de (schneide)
Date: Wed, 12 Oct 1994 09:15:54 +0100 (BST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <"i80fs2.ira.065:12.10.94.07.44.43"@ira.uka.de> from "schneide" at Oct 12, 94 08:44:38 am
Content-Type: text
Content-Length: 4418

schneide has said:
> 
> Hello,
>    at the TPCD conference in Bad Herrenalb, Steve Johnson presented in his talk
> a small circuit which is however not very easily to specify and to verify. He 
> used several proof systems for the verification and for the SMV system, he 
> was not able to create a suitable specification in CTL. This is --in my opinion--
> because CTL (a branching time logic) is a unnatural thing.
> 
>   In my approach, I use HOL and I have embedded some linear time operators
> such as ALWAYS, EVENTUAL, NEXT, WHEN, UNTIL, BEFORE and WHILE. The proof
> method I currently use is as follows: I translate the temporal logic formulae
> in some sort of finite automaton (I call these automata `hardware formulae')
> and use SMV as a decision procedure without validating in HOL afterwards
> (this could however be done, see my paper on HUG93).
> 
> I have verified the single pulser, a short description of the verification is given
> below. I have done the translation into a SMV program by hand, though it is
> absolutely clear to me how it can be done automatically in HOL. 
> The implementation of this translation procedure is one of my future aims.
> 
> 
> 
> --------------------
>  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.
> 
> --------------------
>  Formal specification:
> --------------------
>  ((NEXT(out BEFORE (\t.~NEXT inp t))) WHEN (\t. ~inp t /\ NEXT inp t)) t0 /\
>  ((NEXT((\t.~out t) UNTIL (\t. ~inp t /\ NEXT inp t))) WHEN out) t0 /\
>  ((NEXT((\t.~out t) WHEN (\t. ~inp t /\ NEXT inp t))) WHEN out) t0


proposed SMV spec 


> MODULE main
> VAR
>   inp : boolean;
>    p1 : boolean;
>    p2 : boolean;
>    p3 : boolean;
>    p4 : boolean;
>    q1 : boolean;
>    q2 : boolean;
>    q3 : boolean;
>    q4 : boolean;
>    q5 : boolean;
>    q6 : boolean;
>     C : Circuit(inp);
> #  Cout : boolean;
> ASSIGN
>    init(p1) := 0;
>    next(p1) := inp;
>    init(p2) := 0;
>    next(p2) := C.out;
>    init(p3) := 0;
>    next(p3) := p1;
>    init(p4) := 0;
>    next(p4) := p2;
>    init(q5) := 0;
>    next(q5) := 1;
>    init(q6) := 0;
>    next(q6) := q5;
>    init(q1) := 0;
>    next(q1) := q6 & (q1 | !p3) & (q1 | p1);
>    init(q2) := 0;
>    next(q2) := q6 & (q1 | !p3) & (q1 | p1) & (q2 | p2);
>    init(q3) := 0;
>    next(q3) := q6 & (q3 | p4);
>    init(q4) := 0;
>    next(q4) := q6 & (q3 | p4) & (q4 | (!p1 & inp));
> SPEC
>    AG (q6 -> (((q1 | (!p3 & p1)) -> (q2 | inp | p2)) & 
> 	      ((q3 | p4) -> (!p2 | q4))))


I claim that this spec is way over the top in complexity - ? was it
autogenerated from some tool that builds recogniser automata from
another logic (e.g. there's a program that produces SMV modules to
recognise LTL specs).

A much simpler (in my mind) spec is by observing that the spec can be
divided into 2 parts (in much the same way as the treatment of ?! in HOL).
Basically it can be considered to be

1) If inp goes high then out must go high before inp goes low 
   - i.e. inp must remain high until inp is high
2) Out can be high at most once in each phase where inp is high
   - i.e. if out goes high then it cannot be high again before inp is
     low.

Then the spec is

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

N.b. WU is the "weak until" operator which, for some unknown reason,
isn't in SMV ... its like until except it doesn't force the second term
to become true eventually - i.e. it gives safety properties rather than
liveness properties. Adding WU to SMV is left as an exercise to the
reader (its really pretty trivial).

-- specification AG (!inp -> AX (inp -> A(inp U out))) &
AG (out -> AX A((!out) WU (!inp))) (in module C) is true

resources used:
user time: 0.0333333 s, system time: 0.0666667 s
BDD nodes allocated: 14
Bytes allocated: 995328
BDD nodes representing transition relation: 5 + 1


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."