1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: clock.ml						%
3%									%
4% DESCRIPTION	: Defines predicates for a very simple version of	%
5%		  two phase non-overlapping clocking and derives	%
6%		  theorems about the clock behaviour.  The theory	%
7%		  also uses the temporal abstraction theory to derive	%
8%		  two major theorems for temporal abstraction on any	%
9%		  of the four phases of the clock.			%
10%									%
11%		  These definitions of a two phase non-overlapping 	%
12%		  clock are taken from I. Dhingra's paper, "Formal	%
13%		  Validation of an Integrated Circuit Design Style",	%
14%		  Hardware Verification Workshop, University of		%
15%		  Calgary, January 1987.				%
16%									%
17% AUTHOR	: J.Joyce						%
18% DATE		: 31 March 1987						%
19
20new_theory `clock`;;
21
22loadt `misc`;;
23loadt `types`;;
24
25new_parent `da`;;
26new_parent `mos`;;
27new_parent `tempabs`;;
28
29let Shift = new_definition (
30	`Shift`,
31	"Shift (phi1:^wire) (phi2:^wire) = !t. phi2 (t+2) = phi1 t");;
32
33let Invert = new_definition (
34	`Invert`,
35	"Invert (phi:^wire) (phibar:^wire) = !t. phibar t = Not (phi t)");;
36
37let Cycle1 = new_definition (
38	`Cycle1`,
39	"Cycle1 (phi:^wire) (t:^time) =
40	  (phi t = Hi) /\ (phi (t+1) = Lo) /\
41	    (phi (t+2) = Lo) /\ (phi (t+3) = Lo)");;
42
43let Cycle = new_definition (
44	`Cycle`,
45	"Cycle (phi:^wire) =
46	  ((!t. phi (t+4) = phi t) /\
47	    (Cycle1 phi 0 \/
48	      Cycle1 phi 1 \/ Cycle1 phi 2 \/ Cycle1 phi 3))");;
49
50let Clock = new_definition (
51	`Clock`,
52	"Clock (phi1:^wire,phi1bar:^wire,phi2:^wire,phi2bar:^wire) =
53	  Cycle phi1 /\ Shift phi1 phi2 /\
54	    Invert phi1 phi1bar /\ Invert phi2 phi2bar");;
55
56let isHi = new_definition (`isHi`,"isHi phi t = (phi t = Hi)");;
57
58let Not = definition `mos` `Not`;;
59let Inf = definition `tempabs` `Inf`;;
60let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;;
61
62let DA = theorem `da` `DA`;;
63let Next_ADD1 = theorem `tempabs` `Next_ADD1`;;
64let Next_INCREASE = theorem `tempabs` `Next_INCREASE`;;
65let Next_IDENTITY = theorem `tempabs` `Next_IDENTITY`;;
66let TimeOf_TRUE = theorem `tempabs` `TimeOf_TRUE`;;
67let TimeOf_Next = theorem `tempabs` `TimeOf_Next`;;
68
69let DISJ_ASSOC = TAC_PROOF (
70	([],"!t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3"),
71	REPEAT GEN_TAC THEN
72	BOOL_CASES_TAC "t1" THEN REWRITE_TAC [] ORELSE
73	BOOL_CASES_TAC "t2" THEN REWRITE_TAC [] ORELSE
74	BOOL_CASES_TAC "t3" THEN REWRITE_TAC []);;
75
76% lemma1 = [Cycle phi] |- !t. phi(SUC(SUC(SUC(SUC t)))) = phi t %
77let lemma1 = SUC_FORM_RULE (CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Cycle))));;
78
79let lemma2 =
80	PURE_REWRITE_RULE [lemma1]
81	  (SUC_FORM_RULE
82	    (PURE_REWRITE_RULE [Cycle1]
83	      (CONJUNCT2 (UNDISCH (fst (EQ_IMP_RULE Cycle))))));;
84
85let lemma3 = TAC_PROOF (
86	([],"!phi. Cycle phi ==> !t. (Cycle1 phi (t+4) = Cycle1 phi t)"),
87	REPEAT STRIP_TAC THEN
88	PURE_REWRITE_TAC [Cycle1] THEN
89	PURE_REWRITE_TAC [SYM (SPECL ["t";"4";"m"] ADD_ASSOC)] THEN
90	PURE_REWRITE_TAC [SPECL ["4";"m"] ADD_SYM] THEN
91	PURE_REWRITE_TAC [ADD_ASSOC] THEN
92	REWRITE_TAC [CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Cycle)))]);;
93
94let th1 = TAC_PROOF (
95	([],"0 < 4"),
96	SUC_FORM_TAC THEN
97	ASSUME_TAC (SPEC "0" LESS_0) THEN
98	REPEAT (FIRST [FIRST_ASSUM ACCEPT_TAC;IMP_RES_TAC LESS_SUC]));;
99
100let th2 = TAC_PROOF (
101	([],"!m. m < 4 ==> ((m = 0) \/ (m = 1) \/ (m = 2) \/ (m = 3))"),
102	let thm =
103	  GEN_ALL (SYM
104	    (SUBS [SPECL ["m = n";"m < n"] DISJ_SYM] (SPEC_ALL LESS_THM)))
105	in
106	REPEAT STRIP_TAC THEN
107	PURE_REWRITE_TAC [DISJ_ASSOC] THEN
108	PURE_REWRITE_TAC
109	  [GEN_ALL (REWRITE_RULE [NOT_LESS_0] (SPECL ["m";"0"] thm))] THEN
110	PURE_REWRITE_TAC [thm;SYM (num_CONV "1")] THEN
111	PURE_REWRITE_TAC [thm;SYM (num_CONV "2")] THEN
112	PURE_REWRITE_TAC [thm;SYM (num_CONV "3")] THEN
113	ASM_REWRITE_TAC [SYM (num_CONV "4")]);;
114
115% th3 = |- !m n p. (m + n) + p = (m + p) + n %
116let th3 =
117	GEN_ALL
118	  ((SUBS [SPECL ["n";"p"] ADD_SYM] (SYM (SPEC_ALL ADD_ASSOC)))
119	    TRANS (SPECL ["m";"p";"n"] ADD_ASSOC));;
120
121let Cycle1_ALWAYS = prove_thm (
122	`Cycle1_ALWAYS`,
123	"!phi.
124	  Cycle phi
125	  ==>
126	  !t.
127	    Cycle1 phi t \/
128	    Cycle1 phi (t+1) \/
129	    Cycle1 phi (t+2) \/
130	    Cycle1 phi (t+3)",
131	GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
132	STRIP_ASSUME_TAC
133	  (MP (SPECL ["t";"4"] DA)
134	    (NOT_EQ_SYM (MATCH_MP LESS_NOT_EQ th1))) THEN
135	SUBST1_TAC (ASSUME "t = (q * 4) + r") THEN
136	SPEC_TAC ("q:num","q':num") THEN
137	INDUCT_TAC THENL
138	[PURE_REWRITE_TAC [MULT_CLAUSES;ADD_CLAUSES] THEN
139	 PURE_REWRITE_TAC [Cycle1] THEN
140	 SUC_FORM_TAC THEN
141	 IMP_RES_TAC th2 THENL
142	 (map (\tm. SUBST1_TAC (ASSUME "r = ^tm")) ["0";"1";"2";"3"]) THEN
143	 SUC_FORM_TAC THEN
144	 PURE_REWRITE_TAC [lemma1] THEN
145	 IMP_RES_TAC (DISCH_ALL lemma2) THEN
146	 ASM_REWRITE_TAC [];				% 16 cases %
147	 PURE_REWRITE_TAC [MULT_CLAUSES] THEN
148	 PURE_REWRITE_TAC [SPECL ["m";"4";"n"] th3] THEN
149	 IMP_RES_THEN (\thm. ASM_REWRITE_TAC [thm]) lemma3]);;
150
151let th1 =
152	REWRITE_RULE
153	  [lemma1;ASSUME "phi t = Hi";val_not_eq_ax]
154	  (SUC_FORM_RULE
155	    (PURE_REWRITE_RULE [Cycle1]
156	      (SPEC_ALL (UNDISCH_ALL (SPEC_ALL Cycle1_ALWAYS)))));;
157
158let isHi_Cycle1_ALWAYS = prove_thm (
159	`isHi_Cycle1_ALWAYS`,
160	"!phi t. (Cycle phi /\ isHi phi t) ==> Cycle1 phi t",
161	PURE_REWRITE_TAC [isHi;Cycle1] THEN
162	REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
163	SUC_FORM_TAC THEN
164	ASM_REWRITE_TAC [th1]);;
165
166let num_CONVs = map num_CONV ["1";"2";"3";"4"];;
167let th1 = SUC_FORM_RULE (PURE_REWRITE_RULE [Cycle1] Cycle1_ALWAYS);;
168
169let Cycle_Inf = prove_thm (
170	`Cycle_Inf`,
171	"!phi. Cycle phi ==> Inf (isHi phi)",
172	PURE_REWRITE_TAC [Inf;isHi;GREATER] THEN
173	REPEAT STRIP_TAC THEN
174	ASSUME_TAC (SPEC "t" LESS_SUC_REFL) THEN
175	IMP_RES_TAC LESS_SUC THEN
176	IMP_RES_TAC LESS_SUC THEN
177	IMP_RES_TAC LESS_SUC THEN
178	IMP_RES_TAC (hd (IMP_CANON th1)) THENL
179	(map EXISTS_TAC ["t+4";"t+1";"t+2";"t+3"]) THEN
180	ASM_REWRITE_TAC (num_CONVs @ [ADD_CLAUSES;lemma1]));;
181
182let TimeOf_isHi_TRUE = prove_thm (
183	`TimeOf_isHi_TRUE`,
184	"!phi. Cycle phi ==> !n. (isHi phi) (TimeOf (isHi phi) n)",
185	GEN_TAC THEN DISCH_TAC THEN
186	IMP_RES_TAC Cycle_Inf THEN IMP_RES_TAC TimeOf_TRUE);;
187
188let TimeOf_isHi_Next = prove_thm (
189	`TimeOf_isHi_Next`,
190	"!phi.
191	  Cycle phi ==>
192	  !n. Next (TimeOf (isHi phi) n,TimeOf (isHi phi) (n+1)) (isHi phi)",
193	REPEAT STRIP_TAC THEN
194	IMP_RES_TAC Cycle_Inf THEN IMP_RES_TAC TimeOf_Next);;
195
196% th1 = .. |- phi(SUC(SUC(SUC(SUC t)))) = Hi %
197let th1 = SUBS [SYM (SPEC "t" lemma1)] (ASSUME "phi t = Hi");;
198let th2 = TAC_PROOF (
199	([],"!phi t. (phi t = Lo) ==> ~(phi t = Hi)"),
200	REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC [val_not_eq_ax]);;
201let th3 =
202	SUC_FORM_RULE
203	  (PURE_REWRITE_RULE [isHi] (SPEC "isHi phi" Next_ADD1));;
204let th4 =
205	SUC_FORM_RULE
206	  (PURE_REWRITE_RULE [isHi] (SPEC "isHi phi" Next_INCREASE));;
207
208let isHi_Next_plus4 = prove_thm (
209	`isHi_Next_plus4`,
210	"!phi t. (Cycle phi /\ isHi phi t) ==> Next (t,t+4) (isHi phi)",
211	REPEAT STRIP_TAC THEN
212	SUC_FORM_TAC THEN
213	IMP_RES_TAC
214	  (SUC_FORM_RULE (PURE_REWRITE_RULE [Cycle1] isHi_Cycle1_ALWAYS)) THEN
215	ASSUME_TAC th1 THEN
216	IMP_RES_TAC th2 THEN
217	IMP_RES_TAC th3 THEN
218	IMP_RES_TAC th4 THEN
219	IMP_RES_TAC th4 THEN
220	IMP_RES_TAC th4);;
221
222let TimeOf_isHi_Next_plus4 = prove_thm (
223	`TimeOf_isHi_Next_plus4`,
224	"!phi.
225	  Cycle phi ==>
226	  !n. Next (TimeOf (isHi phi) n,(TimeOf (isHi phi) n)+4) (isHi phi)",
227	REPEAT STRIP_TAC THEN
228	ASSUME_TAC
229	  (SPEC "n" (MATCH_MP TimeOf_isHi_TRUE (ASSUME "Cycle phi"))) THEN
230	IMP_RES_TAC isHi_Next_plus4);;
231
232let TimeOf_isHi_plus4 = prove_thm (
233	`TimeOf_isHi_plus4`,
234	"!phi.
235	  Cycle phi ==>
236	    !n. (TimeOf (isHi phi) (n+1) = (TimeOf (isHi phi) n)+4)",
237	REPEAT STRIP_TAC THEN
238	ASSUME_TAC
239	  (SPEC "n" (MATCH_MP TimeOf_isHi_Next (ASSUME "Cycle phi"))) THEN
240	ASSUME_TAC
241	  (SPEC "n"
242	    (MATCH_MP TimeOf_isHi_Next_plus4 (ASSUME "Cycle phi"))) THEN
243	IMP_RES_TAC Next_IDENTITY);;
244
245let th1 =
246	SUC_FORM_RULE
247	  (PURE_REWRITE_RULE [Cycle1] (ASSUME "Cycle1 phi1 t"));;
248let th2 =
249	SUC_FORM_RULE
250	  (SUBS (CONJUNCTS th1)
251	    (SPEC "t"
252	      (CONJUNCT1
253	        (PURE_REWRITE_RULE [Cycle] (ASSUME "Cycle phi1")))));;
254let th3 = PURE_REWRITE_RULE [Invert] (ASSUME "Invert phi1 phi1bar");;
255let th4 = PURE_REWRITE_RULE [Invert] (ASSUME "Invert phi2 phi2bar");;
256let th5 =
257	SUC_FORM_RULE
258	  (PURE_REWRITE_RULE [Shift] (ASSUME "Shift phi1 phi2"));;
259
260let ClockSignals = prove_thm (
261	`ClockSignals`,
262	"!phi1 phi1bar phi2 phi2bar t.
263	  (Clock (phi1,phi1bar,phi2,phi2bar) /\ (isHi phi1 t))
264	  ==>
265	  (phi1    t     = Hi) /\ (phi1    (t+1) = Lo) /\
266	  (phi1    (t+2) = Lo) /\ (phi1    (t+3) = Lo) /\
267	  (phi1    (t+4) = Hi) /\
268	  (phi1bar (t+1) = Hi) /\ (phi1bar (t+2) = Hi) /\
269	  (phi1bar (t+3) = Hi) /\ (phi1bar (t+4) = Lo) /\
270	  (phi2    (t+2) = Hi) /\ (phi2    (t+3) = Lo) /\
271	  (phi2    (t+4) = Lo) /\
272	  (phi2bar (t+3) = Hi) /\ (phi2bar (t+4) = Hi)",
273	PURE_REWRITE_TAC [Clock] THEN
274	REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
275	IMP_RES_TAC isHi_Cycle1_ALWAYS THEN
276	SUC_FORM_TAC THEN
277	REWRITE_TAC [th1;th2;th3;th4;th5;Not;val_not_eq_ax]);;
278%
279|- !phi1 phi1bar phi2 phi2bar.
280    Clock(phi1,phi1bar,phi2,phi2bar) ==> Cycle phi1
281%
282let Clock_Cycle = save_thm (
283	`Clock_Cycle`,
284	GEN_ALL (DISCH_ALL (CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Clock))))));;
285
286close_theory ();;
287