1% PROOF : Transistor Implementation of a Counter % 2% FILE : regn.ml % 3% % 4% DESCRIPTION : Defines a dynamic register and uses it to construct % 5% a n-bit dynamic register. Note that only N-type % 6% pass transistors are used instead of complementary % 7% logic. % 8% % 9% The register model is taken from Inder Dhingra's % 10% paper, "Formal Validation of an Integrated Circuit % 11% Design Style", Hardware Verification Workshop, % 12% University of Calgary, January 1987. % 13% % 14% AUTHOR : J.Joyce % 15% DATE : 31 March 1987 % 16 17new_theory `regn`;; 18 19loadt `misc`;; 20loadt `types`;; 21 22new_parent `clock`;; 23new_parent `dataabs`;; 24 25% ===================================================================== % 26% Propagation of a signal through the register: % 27% % 28% phiA phiB % 29% _|_ _|_ % 30% i ___| |___w1_____w2_____w3___| |___w4_____w5_____ o % 31% | | | | % 32% Cap1 Cap2 Cap3 Cap4 % 33% % 34% t i(t) i(t) % 35% t+1 Zz i(t) % 36% t+2 Zz Zz i(t) i(t) % 37% t+3 Zz i(t) % 38% t+4 Zz Zz i(t) % 39% ===================================================================== % 40 41let REG_IMP = new_definition ( 42 `REG_IMP`, 43 "REG_IMP (phi1:^wire,phi2:^wire,i:^wire,o:^wire) = 44 ?w1 w2 w3 w4 w5. 45 Ntran (phi1,i,w1) /\ 46 Cap (w1,w2) /\ 47 Cap (w2,w3) /\ 48 Ntran (phi2,w3,w4) /\ 49 Cap (w4,w5) /\ 50 Cap (w5,o)");; 51 52let REGn_IMP = new_definition ( 53 `REGn_IMP`, 54 "REGn_IMP n (phi1:^wire,phi2:^wire,i:^bus,o:^bus) = 55 !m. m <= n ==> REG_IMP (phi1,phi2,DEST_BUS i m,DEST_BUS o m)");; 56 57let when = definition `tempabs` `when`;; 58let Cap = definition `mos` `Cap`;; 59let Ntran = definition `mos` `Ntran`;; 60let Clock = definition `clock` `Clock`;; 61let DEST_BUS = definition `dataabs` `DEST_BUS`;; 62 63let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 64 65let ClockSignals = theorem `clock` `ClockSignals`;; 66let TimeOf_isHi_TRUE = theorem `clock` `TimeOf_isHi_TRUE`;; 67let TimeOf_isHi_plus4 = theorem `clock` `TimeOf_isHi_plus4`;; 68 69let isBus_THM = theorem `dataabs` `isBus_THM`;; 70let Clock_Cycle = theorem `clock` `Clock_Cycle`;; 71 72let t0 = "t:num";; 73let t1 = "SUC t";; 74let t2 = "SUC(SUC t)";; 75let t3 = "SUC(SUC(SUC t))";; 76let t4 = "SUC(SUC(SUC(SUC t)))";; 77 78let w1thm = PURE_REWRITE_RULE [Ntran] (ASSUME "Ntran(phiA,i,w1)");; 79let w2thm = PURE_REWRITE_RULE [Cap] (ASSUME "Cap(w1,w2)");; 80let w3thm = PURE_REWRITE_RULE [Cap] (ASSUME "Cap(w2,w3)");; 81let w4thm = PURE_REWRITE_RULE [Ntran] (ASSUME "Ntran(phiB,w3,w4)");; 82let w5thm = PURE_REWRITE_RULE [Cap] (ASSUME "Cap(w4,w5)");; 83let othm = PURE_REWRITE_RULE [Cap] (ASSUME "Cap(w5,o)");; 84 85% The following 12 theorems establish that the output signal at time % 86% "t+4" is the value of the input signal at time "t" following the % 87% causal relationships shown in the above diagram. Assumptions about % 88% phiA and phiB are introduced as required. % 89 90let w1t0 = REWRITE_RULE [ASSUME "phiA ^t0 = Hi"] (SPEC t0 w1thm);; 91let w1t1 = 92 REWRITE_RULE 93 [ASSUME "phiA ^t1 = Lo";val_not_eq_ax] (SPEC t1 w1thm);; 94let w1t2 = 95 REWRITE_RULE 96 [ASSUME "phiA ^t2 = Lo";val_not_eq_ax] (SPEC t2 w1thm);; 97let w2t1 = REWRITE_RULE [SUC_SUB1;w1t1;w1t0] (SPEC t1 w2thm);; 98let w2t2 = REWRITE_RULE [SUC_SUB1;w1t2;w1t1] (SPEC t2 w2thm);; 99let w3t2 = REWRITE_RULE [SUC_SUB1;w2t2;w2t1] (SPEC t2 w3thm);; 100let w3t2 = REWRITE_RULE [SUC_SUB1;w2t2;w2t1] (SPEC t2 w3thm);; 101let w4t2 = REWRITE_RULE [ASSUME "phiB ^t2 = Hi";w3t2] (SPEC t2 w4thm);; 102let w4t3 = 103 REWRITE_RULE 104 [ASSUME "phiB ^t3 = Lo";val_not_eq_ax] (SPEC t3 w4thm);; 105let w4t4 = 106 REWRITE_RULE 107 [ASSUME "phiB ^t4 = Lo";val_not_eq_ax] (SPEC t4 w4thm);; 108let w5t3 = REWRITE_RULE [SUC_SUB1;w4t3;w4t2] (SPEC t3 w5thm);; 109let w5t4 = REWRITE_RULE [SUC_SUB1;w4t4;w4t3] (SPEC t4 w5thm);; 110let ot4 = REWRITE_RULE [SUC_SUB1;w5t4;w5t3] (SPEC t4 othm);; 111 112% ot4 = ............ |- o(SUC(SUC(SUC(SUC t)))) = i t % 113 114let REG_CORRECT = prove_thm ( 115 `REG_CORRECT`, 116 "!phi1 phi1bar phi2 phi2bar i o. 117 Clock (phi1,phi1bar,phi2,phi2bar) /\ 118 REG_IMP (phi1,phi2,i,o) 119 ==> 120 !t. ((o when (isHi phi1)) (t+1) = (i when (isHi phi1)) t)", 121 PURE_REWRITE_TAC [REG_IMP;when] THEN 122 BETA_TAC THEN 123 REPEAT STRIP_TAC THEN 124 IMP_RES_TAC Clock_Cycle THEN 125 IMP_RES_TAC TimeOf_isHi_plus4 THEN 126 ASM_REWRITE_TAC [] THEN 127 HOL_IMP_RES_THEN (ASSUME_TAC o (SPEC "t")) TimeOf_isHi_TRUE THEN 128 SUC_FORM_TAC THEN 129 IMP_RES_TAC (SUC_FORM_RULE ClockSignals) THEN 130 IMP_RES_TAC (GEN "t" (DISCH_ALL ot4)));; 131 132let REGn_CORRECT = prove_thm ( 133 `REGn_CORRECT`, 134 "!n phi1 phi1bar phi2 phi2bar i o. 135 Clock (phi1,phi1bar,phi2,phi2bar) /\ 136 REGn_IMP n (phi1,phi2,i,o) /\ 137 isBus n i /\ 138 isBus n o 139 ==> 140 !t. ((o when (isHi phi1)) (t+1) = (i when (isHi phi1)) t)", 141 PURE_REWRITE_TAC [REGn_IMP;when] THEN 142 BETA_TAC THEN 143 REPEAT STRIP_TAC THEN 144 IMP_RES_TAC isBus_THM THEN 145 ASM_REWRITE_TAC [] THEN 146 REPEAT STRIP_TAC THEN 147 RES_TAC THEN 148 HOL_IMP_RES_THEN 149 (ASSUME_TAC o BETA_RULE o (PURE_REWRITE_RULE [DEST_BUS;when])) 150 REG_CORRECT THEN 151 ASM_REWRITE_TAC []);; 152 153close_theory ();; 154