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 | | -----------------------------------------------------------------