1 2%<---------------------------------------------------------------------------- 3 4 The difference model of transistors and its use to distinguish the good and 5 bad XOR circuits described in "Hardware Verification using Higher-Order 6 Logic" (Camilleri, Gordon and Melham, Technical Report 91). 7 8 The bad circuit is: 9 10 11 |-----| 12 | Pwr | 13 |-----| 14 | p1 15 -- 16 || 17 |--0|| 18 | || 19 | -- 20 | | 21 | | 22 i1---+---- | ---------------------------| 23 | | | 24 | | -- 25 | | || 26 | | |--0|| 27 | | | || 28 | | | -- 29 | | | | 30 i2-- | --- | ---------------------| |---o 31 | | | | 32 | | | -- 33 | | | || 34 | | |---|| 35 | | || 36 | | -- 37 | | p2 | 38 | |----------------------------| 39 | | 40 | -- 41 | || 42 |---|| 43 || 44 -- 45 | p3 46 |-----| 47 | Gnd | 48 |-----| 49 50 The good circuit has two extra transistors forming a transmission gate: 51 52 53 |-----| 54 | Pwr | 55 |-----| 56 | p1 57 -- 58 || 59 |--0|| 60 | || 61 | -- 62 | | 63 | | 64 i1------+---- | ------+--------------------| 65 | | | +-------- | --+ 66 | | ___O___ | -- | 67 | | |-----| | || | 68 +- | --- | ---| |-------+ |--0|| |--o 69 | | | |-----| | || | 70 i2---| | | ------- | -- | 71 | | | | | | | 72 +- | --- | ---------------------| |---+ 73 | | | | | 74 | | | | -- 75 | | | | || 76 | | | |---|| 77 | | | || 78 | | | -- 79 | | p3 | | 80 | |-------+--------------------| 81 | | 82 | -- 83 | || 84 |---|| 85 || 86 -- 87 | p2 88 |-----| 89 | Gnd | 90 |-----| 91 92 93---------------------------------------------------------------------------->% 94 95 96%----------------------------------------------------------------------------% 97% For HOL88 compatibility: % 98% % 99 100hide_constant`o`;; 101load_library`unwind`;; 102load_library`eval`;; 103 104% % 105%----------------------------------------------------------------------------% 106 107system `rm XOR.th`;; % removes XOR.th if it exists % 108 109new_theory `XOR`;; 110 111% The type of the two values HI and LO. % 112 113new_type 0 `val`;; 114 115new_constant(`HI`, ":val");; 116new_constant(`LO`, ":val");; 117 118%----------------------------------------------------------------------------% 119% Power. % 120%----------------------------------------------------------------------------% 121 122let PWR = 123 new_definition 124 (`PWR`, "PWR o = (o=HI)");; 125 126%----------------------------------------------------------------------------% 127% Ground. % 128%----------------------------------------------------------------------------% 129 130let GND = 131 new_definition 132 (`GND`, "GND o = (o=LO)");; 133 134%----------------------------------------------------------------------------% 135% n-transistor. % 136%----------------------------------------------------------------------------% 137 138let NTRAN = 139 new_definition 140 (`NTRAN`, "NTRAN(g,a,b) = (g=HI) ==> ((a=LO) = (b=LO))");; 141 142%----------------------------------------------------------------------------% 143% p-transistor. % 144%----------------------------------------------------------------------------% 145 146let PTRAN = 147 new_definition 148 (`PTRAN`, "PTRAN(g,a,b) = (g=LO) ==> ((a=HI) = (b=HI))");; 149 150%----------------------------------------------------------------------------% 151% The bad XOR gate. % 152%----------------------------------------------------------------------------% 153 154let BAD_XOR = 155 new_definition 156 (`BAD_XOR`, 157 "BAD_XOR(i1,i2,o) = 158 ?p1 p2 p3. 159 PWR p1 /\ GND p2 /\ 160 PTRAN(i1,p1,p3) /\ NTRAN(i1,p3,p2) /\ 161 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3)");; 162 163%----------------------------------------------------------------------------% 164% The good XOR gate. % 165%----------------------------------------------------------------------------% 166 167let GOOD_XOR = 168 new_definition 169 (`GOOD_XOR`, 170 "GOOD_XOR(i1,i2,o) = 171 ?p1 p2 p3. 172 PWR p1 /\ GND p2 /\ 173 PTRAN(i1,p1,p3) /\ NTRAN(i1,p3,p2) /\ 174 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3) /\ 175 PTRAN(i1,i2,o) /\ NTRAN(p3,i2,o)");; 176 177close_theory();; 178 179 180%----------------------------------------------------------------------------% 181% Some INCREDIBLY INEFFICIENT ML functions for `running' CMOS circuits. % 182% Massive speed ups should be possible by using less brute-force methods. % 183%----------------------------------------------------------------------------% 184 185 186%----------------------------------------------------------------------------% 187% |- (x=y) = (y=x) if y is a variable and % 188% either x is not a variable or x is in l % 189%----------------------------------------------------------------------------% 190 191let EQ_FLIP_CONV l t = 192 (let x,y = dest_eq t 193 in 194 if is_var y & (not(is_var x) or mem x l) 195 then SPECL[x;y](INST_TYPE[type_of x, ":*"]EQ_SYM_EQ) 196 else fail 197 ) ? failwith `EQ_FLIP_CONV`;; 198 199%----------------------------------------------------------------------------% 200% extract_vars "t = ?p1 ... pm. (l1=t1)/\ ... /\(ln=tn)" % 201% ---> % 202% the list of those li such that ti is not a variable. % 203%----------------------------------------------------------------------------% 204 205let extract_vars th = 206 let (), right = dest_eq(concl th) 207 in 208 let (),conjs = (I # conjuncts)(strip_exists right) 209 in 210 mapfilter(\t. not(is_var(rhs t)) => lhs t | fail)conjs;; 211 212%----------------------------------------------------------------------------% 213% remove repeated members from an existentially quantified conjunction % 214% on the right of an equation. % 215%----------------------------------------------------------------------------% 216 217let CONJ_SIMP_RULE th = 218 let left,right = dest_eq(concl th) 219 in 220 let vars,body = strip_exists right 221 in 222 let l = conjuncts body 223 in 224 let l' = setify l 225 in 226 if l=l' 227 then th 228 else th TRANS LIST_MK_EXISTS vars (CONJ_SET_CONV l l');; 229 230%----------------------------------------------------------------------------% 231% I added the stuff below to convert "T=x" into "x" and "F=x" into "~x" etc % 232% when making the file run in HOL88. I don't know why it was not % 233% needed before. % 234%----------------------------------------------------------------------------% 235 236load_library`taut`;; 237 238let EQTL_OUT = TAUT_RULE "(T = x) = x" 239and EQFL_OUT = TAUT_RULE "(F = x) = ~x" 240and EQTR_OUT = TAUT_RULE "(x = T) = x" 241and EQFR_OUT = TAUT_RULE "(x = F) = ~x";; 242 243let CMOS_UNWIND th = 244 CONJ_SIMP_RULE 245 (OLD_UNWIND_RULE 246 (CONV_RULE 247 (bool_CONV THENC 248 EQ_CONV THENC 249 COND_CONV THENC 250 DEPTH_CONV(REWRITE_CONV EQTL_OUT) THENC % Added for HOL88 % 251 DEPTH_CONV(REWRITE_CONV EQFL_OUT) THENC % Added for HOL88 % 252 DEPTH_CONV(REWRITE_CONV EQTR_OUT) THENC % Added for HOL88 % 253 DEPTH_CONV(REWRITE_CONV EQFR_OUT) THENC % Added for HOL88 % 254 DEPTH_CONV(EQ_FLIP_CONV(extract_vars th))) 255 th));; 256 257letrec iterate f x = 258 let x' = f x 259 in 260 if x=x' then x else iterate f x';; 261 262let CMOS_EXPAND th = 263 let th1 = UNFOLD_RULE [NTRAN;PTRAN;PWR;GND] th 264 in 265 let th2 = iterate CMOS_UNWIND th1 266 in 267 let th3 = CONV_RULE (DEPTH_CONV(REWRITE_CONV EXISTS_SIMP)) th2 268 in 269 let th4 = REWRITE_RULE[]th3 270 in 271 (PRUNE_RULE th4 ? th4);; 272 273let prove_case xor_spec (i1,i2) = 274 CMOS_EXPAND(INST[i1,"i1:val";i2,"i2:val"](SPEC_ALL xor_spec));; 275 276let BAD_HH_THM = prove_case BAD_XOR ("HI","HI");; 277 278let BAD_HL_THM = prove_case BAD_XOR ("HI","LO");; 279 280let BAD_LH_THM = prove_case BAD_XOR ("LO","HI");; 281 282let BAD_LL_THM = prove_case BAD_XOR ("LO","LO");; 283 284 285let GOOD_HH_THM = prove_case GOOD_XOR ("HI","HI");; 286 287let GOOD_HL_THM = prove_case GOOD_XOR ("HI","LO");; 288 289let GOOD_LH_THM = prove_case GOOD_XOR ("LO","HI");; 290 291let GOOD_LL_THM = prove_case GOOD_XOR ("LO","LO");; 292