1 2% Inder's adder slice (ADD_SLICE) 3 4 5 |-----| 6 | PWR | 7 |-----| 8 | 9 |p0 10 | 11 |---------+------------+----------+------------+-------------| 12 | | | | | | 13 -- -- | ---+--- -- | 14 || || | || || || | 15p1-0|| b ||0--cin | a--0|| ||0--b ||0--a | 16 || | || | || || || | 17 -- 0 -- | ---+--- -- | 18 | ----- | | | | | 19 | ----- | | | | | 20 p2|--| |--|p3 | |p7 |p8 | 21 | | | | | | 22 | | | | | | 23 -- -- | -- -- | 24 || || -- || || -- 25a--0|| ||0--p1 || ||0--cin ||0--b || 26 || || |-0|| || || |-0|| 27 -- -- | || -- -- | || 28 | | | -- | | | -- 29 p4|---------+-------| |--sum p1|------------+--------| |--cout 30 | | | -- | | | -- 31 -- -- | || -- -- | || 32 || || |--|| || || |--|| 33a---|| b ||---p1 || cin---|| b---|| || 34 || | || -- || || -- 35 -- | -- | -- -- | 36 | ----- | | | | | 37 | ----- | | | | | 38 p5|--| |--|p6 | |p9 |p10 | 39 | | | | | | 40 | | | | | | 41 -- -- | ---+--- -- | 42 || || | || || || | 43p1--|| ||---cin | a---|| ||---b ||---a | 44 || || | || || || | 45 -- -- | ---+--- -- | 46 | | | | | | 47 |---------+------------+----------+------------+-------------| 48 | 49 |p11 50 | 51 |-----| 52 | GND | 53 |-----| 54 55% 56 57timer true;; 58 59new_theory`adders`;; 60 61 62new_definition 63 (`PWR`, 64 "PWR(o:bool) = (o=T)");; 65 66new_definition 67 (`GND`, 68 "GND(o:bool) = (o=F)");; 69 70new_definition 71 (`PTRAN`, 72 "PTRAN(g,s:bool,d:bool) = ((g=F) ==> (s=d))");; 73 74new_definition 75 (`NTRAN`, 76 "NTRAN(g,s:bool,d:bool) = ((g=T) ==> (s=d))");; 77 78new_definition 79 (`ADD1_IMP`, 80 "ADD1_IMP(a,b,cin,sum,cout) = 81 ?p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11. 82 PTRAN(p1,p0,p2) /\ PTRAN(cin,p0,p3) /\ 83 PTRAN(b,p2,p3) /\ PTRAN(a,p2,p4) /\ PTRAN(p1,p3,p4) /\ 84 NTRAN(a,p4,p5) /\ NTRAN(p1,p4,p6) /\ 85 NTRAN(b,p5,p6) /\ NTRAN(p1,p5,p11) /\ NTRAN(cin,p6,p11) /\ 86 PTRAN(a,p0,p7) /\ PTRAN(b,p0,p7) /\ 87 PTRAN(a,p0,p8) /\ PTRAN(cin,p7,p1) /\ PTRAN(b,p8,p1) /\ 88 NTRAN(cin,p1,p9) /\ NTRAN(b,p1,p10) /\ 89 NTRAN(a,p9,p11) /\ NTRAN(b,p9,p11) /\ NTRAN(a,p10,p11) /\ 90 PWR(p0) /\ PTRAN(p4,p0,sum) /\ NTRAN(p4,sum,p11) /\ 91 GND(p11) /\ PTRAN(p1,p0,cout) /\ NTRAN(p1,cout,p11)");; 92 93 94let PTRAN = definition `adders` `PTRAN` 95and NTRAN = definition `adders` `NTRAN` 96and PWR = definition `adders` `PWR` 97and GND = definition `adders` `GND` 98and ADD1_IMP = definition `adders` `ADD1_IMP`;; 99 100% |- (x=y) = (y=x) if y is a variable and 101 either x is not a variable or x is in l % 102 103let EQ_FLIP_CONV l t = 104 (let x,y = dest_eq t 105 in 106 if is_var y & (not(is_var x) or mem x l) 107 then SPECL[x;y](INST_TYPE[type_of x, ":*"]EQ_SYM_EQ) 108 else fail 109 ) ? failwith `EQ_FLIP_CONV`;; 110 111% extract_vars "t = ?p1 ... pm. (l1=t1)/\ ... /\(ln=tn)" 112 ---> 113 the list of those li such that ti is not a variable % 114 115let extract_vars th = 116 let (), right = dest_eq(concl th) 117 in 118 let (),conjs = (I # conjuncts)(strip_exists right) 119 in 120 mapfilter(\t. not(is_var(rhs t)) => lhs t | fail)conjs;; 121 122% remove repeated members from an existentially quantified conjunction 123 on the right of an equation % 124 125let CONJ_SIMP_RULE th = 126 let left,right = dest_eq(concl th) 127 in 128 let vars,body = strip_exists right 129 in 130 let l = conjuncts body 131 in 132 let l' = setify l 133 in 134 if l=l' 135 then th 136 else th TRANS LIST_MK_EXISTS vars (CONJ_SET_CONV l l');; 137 138let CMOS_UNWIND th = 139 CONJ_SIMP_RULE 140 (UNWIND_RULE 141 (CONV_RULE 142 (bool_CONV THENC 143 EQ_CONV THENC 144 COND_CONV THENC 145 (DEPTH_CONV (EQ_FLIP_CONV(extract_vars th)))) 146 th));; 147 148letrec iterate f x = 149 let x' = f x 150 in 151 if x=x' then x else iterate f x';; 152 153let CMOS_EXPAND th = 154 let th1 = UNFOLD_RULE [NTRAN;PTRAN;PWR;GND] th 155 in 156 let th2 = iterate CMOS_UNWIND th1 157 in 158 let th3 = CONV_RULE (DEPTH_CONV(REWRITE_CONV EXISTS_SIMP)) th2 159 in 160 (PRUNE_RULE th3 ? th3);; 161 162let prove_case1(a,b,cin) = 163 CMOS_EXPAND(INST[a,"a:bool";b,"b:bool";cin,"cin:bool"]ADD1_IMP);; 164 165let TTT_Thm1 = save_thm(`TTT_Thm1`, prove_case1("T","T","T"));; 166 167let TTF_Thm1 = save_thm(`TTF_Thm1`, prove_case1("T","T","F"));; 168 169let TFT_Thm1 = save_thm(`TFT_Thm1`, prove_case1("T","F","T"));; 170 171let TFF_Thm1 = save_thm(`TFF_Thm1`, prove_case1("T","F","F"));; 172 173let FTT_Thm1 = save_thm(`FTT_Thm1`, prove_case1("F","T","T"));; 174 175let FTF_Thm1 = save_thm(`FTF_Thm1`, prove_case1("F","T","F"));; 176 177let FFT_Thm1 = save_thm(`FFT_Thm1`, prove_case1("F","F","T"));; 178 179let FFF_Thm1 = save_thm(`FFF_Thm1`, prove_case1("F","F","F"));; 180 181 182% Full adder from page 92 "Introduction to MOS LSI Design" by 183 Mavor, Jack and Denyer. This circuit (with some bits missing) also 184 occurrs in "Let's Design CMOS Circuits! (Part 1)" by M. Annaratone, 185 CMU-CS-84-101 % 186 187new_definition 188 (`ADD2_IMP`, 189 "ADD2_IMP(a,b,cin,sum,cout) = 190 ?p0 p1 p2 p3 p4 p5. 191 PWR(p0) /\ GND(p5) /\ 192 PTRAN(cin,p0,p1) /\ NTRAN(cin,p1,p5) /\ PTRAN(p3,p1,sum) /\ 193 NTRAN(p2,p1,sum) /\ PTRAN(p2,cin,sum) /\ NTRAN(p3,cin,sum) /\ 194 PTRAN(p3,cin,cout) /\ NTRAN(p2,cin,cout) /\ PTRAN(p2,a,cout) /\ 195 NTRAN(p3,a,cout) /\ PTRAN(a,p2,b) /\ NTRAN(p4,p2,b) /\ 196 PTRAN(p4,p3,b) /\ NTRAN(a,p3,b) /\ PTRAN(b,a,p2) /\ NTRAN(b,p2,p4) /\ 197 PTRAN(b,p4,p3) /\ NTRAN(b,p3,a) /\ PTRAN(a,p0,p4) /\ NTRAN(a,p4,p5)");; 198 199 200let ADD2_IMP = definition `adders` `ADD2_IMP`;; 201 202let prove_case2(a,b,cin) = 203 CMOS_EXPAND(INST[a,"a:bool";b,"b:bool";cin,"cin:bool"]ADD2_IMP);; 204 205let TTT_Thm2 = save_thm(`TTT_Thm2`, prove_case2("T","T","T"));; 206 207let TTF_Thm2 = save_thm(`TTF_Thm2`, prove_case2("T","T","F"));; 208 209let TFT_Thm2 = save_thm(`TFT_Thm2`, prove_case2("T","F","T"));; 210 211let TFF_Thm2 = save_thm(`TFF_Thm2`, prove_case2("T","F","F"));; 212 213let FTT_Thm2 = save_thm(`FTT_Thm2`, prove_case2("F","T","T"));; 214 215let FTF_Thm2 = save_thm(`FTF_Thm2`, prove_case2("F","T","F"));; 216 217let FFT_Thm2 = save_thm(`FFT_Thm2`, prove_case2("F","F","T"));; 218 219let FFF_Thm2 = save_thm(`FFF_Thm2`, prove_case2("F","F","F"));; 220 221close_theory();; 222 223 224