Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 12 Oct 1994 09:00:43 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA29237; Wed, 12 Oct 1994 01:48:54 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA29232; Wed, 12 Oct 1994 01:48:48 -0600 Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id AAA18150 for ; Wed, 12 Oct 1994 00:41:53 -0700 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Wed, 12 Oct 1994 08:41:20 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <01063-0@i80fs2.ira.uka.de>; Wed, 12 Oct 1994 08:44:39 +0100 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)