To: info-hol@cs.uidaho.edu
Subject: Single Pulser
Date: Wed, 12 Oct 1994 08:44:38 +0100
From: schneide
Message-Id: <"i80fs2.ira.065:12.10.94.07.44.43"@ira.uka.de>
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.
Klaus Schneider
(**********************************)
(* *)
(* Klaus Schneider *)
(* *)
(* Institut f"ur Rechnerentwurf *)
(* und Fehlertoleranz *)
(* Universit"at Karlsruhe *)
(* Zirkel 2 *)
(* Geb"aude 20.20, Raum 255 *)
(* 76128 Karlsruhe 1 *)
(* new post number : 76128 *)
(* Germany *)
(* *)
(* Tel: 0721/608 3641 *)
(* Fax: 0721/37 04 55 *)
(* e-mail: schneide@ira.uka.de *)
(* *)
(**********************************)
--------------------
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
-------------------------------
Translation into SMV program
-------------------------------
MODULE Circuit(inp)
VAR
l1 : boolean;
DEFINE
l2 := !l1;
out := inp & l2;
ASSIGN
init(l1) := 0;
next(l1) := inp;
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))))
-------------------------------
SMV output
-------------------------------
smv -f -r single_pulse.smv
Key table size: 16381
Apply cache size: 16381
Variable ordering heuristics: OFF
Parsing...done.
inp:
BDD variable 17
p1:
BDD variable 18
p2:
BDD variable 19
p3:
BDD variable 20
p4:
BDD variable 21
q1:
BDD variable 22
q2:
BDD variable 23
q3:
BDD variable 24
q4:
BDD variable 25
q5:
BDD variable 26
q6:
BDD variable 27
C.l1:
BDD variable 28
process selector variable:
checking for multiple assignments...
checking for circular assignments...
evaluating INIT statements...
evaluating init() assignments...
size of global initial set = 2 states, 13 BDD nodes
evaluating TRANS statements...
evaluating next() assignments...
evaluating C.out:
evaluating C.l2:
size of C.l2 = 3 BDD nodes
size of C.out = 4 BDD nodes
size of transition relation = 279 BDD nodes
evaluating normal assignments...
size of invariant set = 4096 states, 1 BDD nodes
searching reachable state space..
iteration 0: BDD size = 13, states = 2
iteration 1: BDD size = 22, states = 6
iteration 2: BDD size = 37, states = 14
iteration 3: BDD size = 46, states = 26
iteration 4: BDD size = 53, states = 38
iteration 5: BDD size = 55, states = 44
evaluating fairness constraints...
evaluating specification AG (q6 -> (q1 | !p3 & p1 -> q2 | inp | p...
computing fixed point approximations for 1...
size of Y1 = 4096 states, 1 BDD nodes
size of Y2 = 44 states, 55 BDD nodes
computing fixed point approximations for AG (q6 -> (q1 | !p3 & p1 -> q2 | inp | p......
-- specification AG (q6 -> (q1 | !p3 & p1 -> q2 | inp | p... is true
resources used:
user time: 0.116667 s, system time: 0.1 s
BDD nodes allocated: 1836
Bytes allocated: 917504
BDD nodes representing transition relation: 279 + 1
reachable states: 44 (2^5.45943) out of 4096 (2^12)
smv: exit(0)
To: info-hol@cs.uidaho.edu
Subject: "Re: Single Pulser"
Date: Wed, 12 Oct 1994 10:20:31 +0100
From: schneide
Message-Id: <"i80fs2.ira.475:12.10.94.09.20.34"@ira.uka.de>
David Shepherd said:
|> 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).
I agree. There are certainly lots of states which are unnecessary.
Actually, there is no tool which generates this output, but I am currently
implementing such a tool. The transformation in a SMV-description
similar to the one I gave, can be done completely safe (i.e. without
mk_thm) in HOL. The output will then be exactly what I have
generated by hand.
Even if it is possible in this example to give a straightforward spec
directly in CLT, I do not believe that this is as simple for other
specifications as well. This is because the branching time has some
effects which seem to be unnatural to me, e.g. the NEXT operator
can be distributed over all other operators in linear logic, but not
in CTL, i.e. NOT(NEXT x) is not NEXT(NOT x) does hold in linear
logic.
So, are people able to think in CTL directly? I am not sure about that.
The tool does therefore also translate linear logic into branching
time logic.
Klaus.
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
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
To: info-hol@cs.uidaho.edu
Subject: Re: Single Pulser
Date: Wed, 12 Oct 1994 11:16:23 +0100
From: schneide
Message-Id: <"i80fs2.ira.881:12.10.94.10.16.29"@ira.uka.de>
I have to apologize to use info-hol for a LTL-CTL discussion, but
both LTL and CTL are interesting formalisms which could/should be
implemented in HOL/HOL2000. I have already a theory of temporal
linear time operators which I can make available. But I know, that
some more people do also have such theories.
Again, D. Shepherd has said:
|> What I was disputing was the claim that the property couldn't be
|> described in CTL and needed all extra stuff in the main module to
|> capture the spec.
Yes, of course you can express these things directly in CTL. However,
I am concerned about the understanding of nested branching time
operators. The spec you gave only uses A-Operators, but if you have
mixtures with E-Operators things can become quickly awkward.
|> BTW, I'm not sure exactly what your tool is ... is it a proof system
|> for such SMV like machines in HOL or is it a method of generating an
|> equivalent CTL formula from a more general one?
My (future) tool is translating a fragment (which I however can not formalize here)
of LTL into automata-like formulae in HOL. This translation is however
not done as in the mentioned CAV94 paper (which required exponential time
in the worst case). Instead, it uses some facts of the properties of the
fragment and therefore the translation can be done in linear time.
Of course, not everything can be expressed in this fragment, e.g.
fairness is lost. However, from the hardware specification point of
view I am surprised how many specifications fall into this fragment.
|> Certainly, from brief experimentation with a LTL->CTL translator
|> someone at CMU has done (see CAV94 for details), LTL is certainly
|> much more "natural" to think about - however, if you can express
|> something in CTL then it is about 2 or 3 times more efficient than
|> doing the same in translated LTL.
Yes, LTL model checking is no more polynomial and as complex as
LTL satisfiability checking. However, often the fact is mentioned
that CTL model checking can be done in linear time (in terms of
the length of the formulae and the size of the model), but I heard
somewhere that LTL is exponentially more succint than CTL, i.e.
there are facts which can be expressed with relatively small
LTL-formulae, but only with large CTL formulae. So, at the end,
the complexity is all the same, if you consider the same problem.
Klaus.
From: David Shepherd
Subject: Re: "Re: Single Pulser/Spec of D. Shepherd" (fwd)
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Wed, 12 Oct 1994 12:26:38 +0100 (BST)
David Shepherd has said:
Matthew Morley has said:
> I dunno if it's legal CTL (nesting Os, I like stronger logics!) but it
> seems to me that the invariant you & Klaus want is:
>
> (!inp & O inp) -> O ((inp & !out) U (inp & out & O (!out U !inp)))
>
> which, if my (also swift) thinking is correct leaves things nicely
> loose around the "what of out when inp is low" area? Note the
> reference point is that before t0.
Its not CTL -- but it is LTL (apart from use of O instead of X).
My mindset seems to be polluted by CTL and I hadn't thought of this formulation
till I saw it - at which point it is obvious!
Also, given LTL's use of U as a "strong" until (p U q means p holds until
q hold *and* q will definitely hold at some point), an extra antecedent
(G (inp -> F !inp))
is needed to filter out traces where inp remains high for ever.
Using this the formula is proved true.
Now while all these take a trivial time (< 1s) it is instructive to
compare the reachable state space and transition relation size:
1) CTL proof:
BDD nodes allocated: 14
BDD nodes representing transition relation: 5 + 1
reachable states: 4 (2^2) out of 4 (2^2)
2) HOL linear logic translated to CTL
BDD nodes allocated: 1488
BDD nodes representing transition relation: 279 + 1
reachable states: 44 (2^5.45943) out of 4096 (2^12)
3) LTL translated to CTL
BDD nodes allocated: 704
BDD nodes representing transition relation: 41 + 1
reachable states: 144 (2^7.16993) out of 256 (2^8)
Note that 2) introduces several more variables and has a bigger transition
relation - on larger examples this may be a more serious problem!
--------------------------------------------------------------------------
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."
--------------------------------------------------------------------------
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."
To: info-hol@cs.uidaho.edu
Subject: Re: Single Pulser/Spec of P.Windley
Date: Wed, 12 Oct 1994 16:30:56 +0100
From: schneide
Message-Id: <"i80fs2.ira.729:12.10.94.15.30.59"@ira.uka.de>
Of course, a specification in higher order logic is the nicest one.
However, the verification can then only be done manually, and
if you consider the runtimes in a previous email of D. Shepherd,
then you will realize, that HOL can never compete with the
model checkers in terms of efficiency and usability.
Model checkers are base on very limited languanges such that they
cannot be the solution for hardware verification.
A tactic like SMV_TAC would be nevertheless very helpful in HOL,
therefore I am going to implement something like that.
Klaus.
From: "Kathi Fisler"
Subject: Re: Single Pulser
To: info-hol@cs.uidaho.edu
Date: Wed, 12 Oct 1994 11:02:14 -0500 (EST)
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
From: "Phil Windley"
To: "Kathi Fisler"
Cc: info-hol@cs.uidaho.edu, schneide@ira.uka.de, des@inmos.co.uk
Subject: Re: Single Pulser
In-Reply-To: Your message of Wed, 12 Oct 1994 11:02:14 -0500.
<199410121602.JAA19126@dworshak.cs.uidaho.edu>
Date: Wed, 12 Oct 1994 11:12:23 -0600
On Wed, 12 Oct 1994 11:02:14 -0500 (EST) "Kathi Fisler" writes
+--------------------
| There should only be one output pulse between each pair of
| rising edges on the input pulse.
One of the nice things about unique existence...
--phil--
From: "Victor A. Carreno"
To: kfisler@cs.indiana.edu
Subject: Re: Single Pulser
Cc: info-hol@cs.uidaho.edu, vac@air16.larc.nasa.gov
>As has already been pointed out, this specification missed the point
>that the output should not be high when the input is low.
>This is not a component that can be realized in physical hardware,
>since we can't predict the drop on the input.
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*
The specification by Albert Camilleri does not make the output low when the
input is low. 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.
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.
Victor.
To: info-hol@cs.uidaho.edu (info-hol)
Date: Wed, 12 Oct 94 14:29:10 PDT
Cc: bobo@hprpcd.rose.hp.com (Bob Odineal)
For what it's worth, one little trick I have found when using SMV, which helps
*enormously* with reducing the complexity of the CTL specs, is to define
additional macros into the FSM model, and then to use these directly in the CTL
formulae. This can potentially make things much clearer (especially with
problems much more complex than the single pulser ;-).
To illustrate, in my proposed SMV solution to the single pulser (which Kathi
Fisler posted earlier) the use of a variable to denote the "rising edge" of
the input is helpful because it doesn't have to be expressed in terms of
temporal "next" operators inside the CTL spec each time it is needed.
(Obviously, such use of macros helps sort out the wood from the trees in most
specification languages.)
So, if
risingEdge(t+1) = i(t+1) & ~i(t) (to be expressed as a FSM)
the first part of the spec says that once you get a rising edge on the
input, then the output will always eventually go high.
AG (risingEdge -> (AF o))
The second part says that once an output happens then it will immediately go
low on the next cycle (a single pulse), and it will stay low at least until
the next rising edge on the input. (max one output per rising edge).
AG (o -> (AX (A [!o U risingEdge])))
And finally, the third part of the spec says that if the output does not
happen at the same time as the rising edge on the input, then there will be no
other rising edge until the output happens. (max one rising edge per output).
AG (risingEdge -> (!o -> (AX (A [!risingEdge U o]))))
So the first part of the spec denotes liveness, and the second and third
together denote a 1:1 correspondence between input and rising edge.
***Now caution is required here.***
The above spec attempts to capture the notion of "neighbourhood" within which
the output must go high. The neighbourhood (as presented in Steve Johnson's
lecture at TPCD) is defined as the interval between successive rising edges on
the input. This presumes a special kind of input: one which goes low again
after it goes high!
Thus, the implementation suggested in the paper of making the output go high
on the falling edge of the input:
o(t+1) = ~i(t+1) /\ i(t)
does not satisfy the above specification for all inputs, eg. in the case that
the input stays high forever! In such (an undesired) behaviour, the notion of
neighbourhood we adopted becomes infinite, so we need to put a constraint on
the input to be well-behaved if the spec is to make any sense. This can be
regarded as an implementation issue, of course, as opposed to one of
specification (depending on how loose a spec one desires).
In SMV, one abstract way of constraining the behaviour of the input would be by
using FAIRNESS constraints, eg
FAIRNESS risingEdge
which would prune the state space to only those FSMs in which rising edges
happened frequently often (i.e. to disregard cases where the input stayed high
forever, or low forever).
An overall SMV verification, therefore, of the implementation of the single
pulser presented in Steve's paper could be:
---------------------------------------------------------------
MODULE main
VAR i : boolean; -- non-deterministically 0 or 1.
VAR pi : boolean; -- previous value of i, ie. pi(t+1) = i
ASSIGN next (pi) := i;
DEFINE o := pi & !i; -- implementation of single pulser.
-- (equivalent to input falling edge!)
DEFINE risingEdge := i & !pi; -- 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]))))
----------------------------------------------------------------
The result is rather simple, but I must confess to have only thought about the
matter for no more than several minutes, so there could well be mistakes from
what was originally intended, and of course, there could well be other simpler
and more elegant solutions.
--Albert
PS Without using the additional benefit of expressing parts of the specs as
FSMs, I have often found that expressivity in CTL alone can be a problem.
With a combination of FSM and CTL, however, things can get a lot easier.
One common example is referring to things which must have happened in the
past: e.g. if X is true, then Y must have been true some time ago.
This sort of thing becomes very easy if you can use FSMs to maintain
"memory" (or state), and then to use that directly in the CTL specs.
--
-----------------------------------------------------------------
| 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 | |
-----------------------------------------------------------------
From: Albert Camilleri
Subject: Re: Single Pulser (reply to Victor)
To: info-hol@cs.uidaho.edu (info-hol)
Date: Wed, 12 Oct 94 16:04:11 PDT
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 | |
-----------------------------------------------------------------
From: "steve johnson"
Subject: Could one of you post this to the HOL newsgroup.
To: zhu@cs.indiana.edu (zheng zhu), psm@cs.indiana.edu
Date: Wed, 12 Oct 1994 16:09:11 -0500 (EST)
Paul or Zheng.
Thanks for the transcripts; Kathi has also told me about them. I'm just
back from ICCD and catching up on my mail so I haven't had much time
to study the correspondence among members of the HOL group. However,
from my first impression, the discussion of CTL may not be a reflection
of what actually occurred at the meeting. Would you please post this
note with my promise to follow up with a more detailed discussion.
It is true that we had substantial difficulty representing in CTL
the facts which we wanted to prove about the single pulser. Indeed, the
attempt that appears in the participants' proceedings is not only
cumbersome, but may also be incorrect, and further, is an overly strong
proposition.
We (the listed coauthors) are very indebted to Albert Camerelli who
looked at the section at the TPCD workshop and made some suggestions.
On our return from Bad Herrenalb, Kathi Fisler and I worked with the
formulas suggested by Albert. They are certainly more elegant, almost
certainly correct, and they have been accepted as true by SMV.
I want to look very carefully at the solution before publishing it
and that will take a couple of days. In the mean time, I would like
to clarify: Most important, we were able to specify the properties of interest
about the single pulser in CTL. Our first attempt was not very elegant---and
I am told that we made the kinds of stylistic mistakes that are common when
people first use the logic. But nevertheless, the properties of interest
were expressible in CTL.
Second, I want to acknowledge that one of our goals in this series of studies
is to approach each system with a kind of freshness, or innocence of mind, that
might allow us to explain to someone not versed in verification methodogy
what some of the basic intellectual "startup" problems are in each tool and
logic. We may have been succeeded beyond our dreams with CTL,
but our general impression has been that e a c h formalism exacts its own
kind of intellectual toll and that, over all, these appear to be
quite comparable.
I am very happy to see people taking an interest in this set of studies and
I hope that more can be initiated. We will continue to maintain the
single pulser examples in cooperation with IFIP WG 10.5 (formerly 10.2).
More later...
Steve Johnson______________________________________________
Computer Science Department net: sjohnson@cs.indiana.edu
Indiana University tel: 812-855-2567
Bloomington, IN 47405-4101 fax: 812-855-4829
To: info-hol@cs.uidaho.edu
Subject: Single Pulser Proof in HOL
Date: Thu, 13 Oct 1994 14:13:35 +0100
From: schneide
Again I considered the single pulser. The original spec I gave in linear temporal
logic in HOL was:
((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
The translation (which can be done in HOL) into my automata like formula
resulted in a formula with 10 state variables such that there might be 1024
possible states. The verification of a given circuit required a traversal
through 44 states.
D. Shepherd gave another spec which I would translate to linear temporal
logic as follows:
(~inp t0 ==> NEXT (\d. inp d ==> ((\t.inp t) UNTIL (\t.inp t /\ out t)) d) t0 ) /\
(out t0 ==> NEXT ((\t.~out t) UNTIL (\t.~inp t)) t0 ) /\
(~inp t0 ==> ~out t0)
In a certain way this spec is "more efficient" since there are not so deep
nestings of temporal operators as in my spec. Therefore it is much easier
to prove. I have done the proof of this spec completely in HOL (without
SMV; see the proof script below).
The proof in HOL90.6 required 3.61 seconds (SPARC10) and (1041,3388)
intermediate theorems were generated. I used some special tactics for
temporal operators for the proof, so do not try to rerun it without these
tactics.
However, I didn't translate this spec into my automata formulae in order to
check it with SMV. But it seems to be clear that much less states are produced
by this spec (I am estimating that 6 state variables would be sufficient).
Klaus
(* **************************************************************************** *)
(* PROOF of SINGLE Pulser in HOL *)
(* **************************************************************************** *)
new_theory "single_pulser";
new_parent "es2";
add_theory_to_sml "es2";
open Hardware_Tacs;
new_definition("SINGLE_PULSER_IMP",
--`SINGLE_PULSER_IMP inp out =
?l1 l2.
INV(l1,l2) /\
DELAY(inp,l1) /\
AND(inp,l2,out)`--);
new_definition("SINGLE_PULSER_SPEC1",
--`SINGLE_PULSER_SPEC1 inp out =
!t0. ((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`--);
new_definition("SINGLE_PULSER_SPEC2",
--`SINGLE_PULSER_SPEC2 inp out =
!t0. (~inp t0 ==> NEXT (\d. inp d ==> ((\t.inp t) UNTIL (\t.inp t /\ out t)) d) t0 ) /\
(out t0 ==> NEXT ((\t.~out t) UNTIL (\t.~inp t)) t0 ) /\
(~inp t0 ==> ~out t0)`--);
val SINGLE_PULSER_CORRECT2 = TAC_PROOF(
(* **************************************************************************** *)
(* Evalutation Time : 3.610000 sec *)
(* Intermediate Theorems : (1041,3388) *)
(* **************************************************************************** *)
([],--`SINGLE_PULSER_IMP inp out ==> SINGLE_PULSER_SPEC2 inp out`--),
PURE_REWRITE_TAC(map snd (definitions "-"))
THEN PURE_REWRITE_TAC[AND_DEF,INV_DEF,DELAY_DEF]
THEN FLAT_HW_TAC THEN COMB_ELIM_TAC
THEN CONV_TAC(DEPTH_CONV FORALL_AND_CONV)
THEN CONV_TAC(DEPTH_CONV FORALL_AND_CONV)
THEN STRIP_TAC THEN REPEAT CONJ_TAC
THENL[
REPEAT STRIP_TAC THEN REWRITE_TAC[NEXT] THEN BETA_TAC
THEN DISCH_TAC THEN PURE_REWRITE_TAC[UNTIL_REC] THEN BETA_TAC
THEN ASM_REWRITE_TAC[],
REPEAT STRIP_TAC THEN REWRITE_TAC[NEXT] THEN BETA_TAC
THEN MY_MP_TAC (--`!t:num. out t ==> inp t`--)
THENL[
INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC,
DISCH_TAC]
THEN PURE_REWRITE_TAC[UNTIL_INVARIANT_THM]
THEN EXISTS_TAC (--`\t:num. inp t ==> ~out t`--) THEN BETA_TAC
THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
THEN RES_TAC THEN RES_TAC,
INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN PROP_TAC]);
------- End of Forwarded Message
To: info-hol@cs.uidaho.edu (info-hol)
Date: Thu, 13 Oct 94 14:21:41 PDT
Cc: sjohnson@cs.indiana.edu
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 | |
-----------------------------------------------------------------