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; Thu, 13 Oct 1994 18:13:59 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA21903; Thu, 13 Oct 1994 11:03:55 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA21893; Thu, 13 Oct 1994 11:03:54 -0600 Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA14696; Thu, 13 Oct 1994 10:58:34 -0600 Message-Id: <9410131658.AA14696@jaguar.cs.byu.edu> To: info-hol@leopard.cs.byu.edu Subject: Forward of message from schneide (Single Pulser Proof in HOL) Date: Thu, 13 Oct 1994 10:58:34 -0600 From: Phil Windley ------- Forwarded Message To: info-hol@cs.uidaho.edu Subject: Single Pulser Proof in HOL Date: Thu, 13 Oct 1994 14:13:35 +0100 From: schneide Sender: schneide@ira.uka.de Message-Id: <"i80fs2.ira.813:13.10.94.13.13.42"@ira.uka.de> 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