1(* --------------------------------------------------------------- 2Booth multiplier adapted from boothTheory by Anthony Fox 3 4This approach simply converts Anthony's definitions 5into the language accepted by hwDefine. 6 7All definitions have the suffix "d" (for "Device") 8to differentiate them from their original version 9(e.g, Anthony's definition of ALU becomes ALUd). 10 11The main function takes the input (a,rm,rs,rn) 12and computes (rm * rs + (if a then rn else 0w)). 13--------------------------------------------------------------- *) 14 15 16(* --------------------------------------------------------------- 17 Compilation 18--------------------------------------------------------------- *) 19(* 20quietdec := true; 21loadPath := ".." :: "../dff" :: !loadPath; 22map load 23 ["inlineCompile","fpgaCodeGenerator", 24 "word32Theory","boothTheory","compile","metisLib", 25 "arithmeticTheory","intLib","vsynth"]; 26open boothTheory vsynth compile metisLib inlineCompile; 27val _ = intLib.deprecate_int(); 28val _ = (if_print_flag := false); 29quietdec := false; 30*) 31 32 33(*----------------------------------------------------------------------------- 34 Boilerplate needed for compilation 35-----------------------------------------------------------------------------*) 36open HolKernel Parse boolLib bossLib metisLib; 37 38 39(* --------------------------------------------------------------- 40 Open theories 41--------------------------------------------------------------- *) 42open word32Theory boothTheory compile metisLib intLib 43 vsynth arithmeticTheory inlineCompile 44 fpgaCodeGenerator; 45 46 47(*----------------------------------------------------------------------------- 48 Set default parsing to natural numbers rather than integers 49-----------------------------------------------------------------------------*) 50val _ = intLib.deprecate_int(); 51 52(*---------------------------------------------------------------------------*) 53(* END BOILERPLATE *) 54(*---------------------------------------------------------------------------*) 55 56(*---------------------------------------------------------------------------*) 57(* Start new theory "boothDev" *) 58(*---------------------------------------------------------------------------*) 59val _ = new_theory "boothDev"; 60infixr 3 THENR; 61val _ = type_abbrev("word",``:word32``); 62 63(*---------------------------------------------------------------------------*) 64(* Converts the value of HB_def into a string *) 65(*---------------------------------------------------------------------------*) 66fun HB() = let fun tm2str tm = let val saved_val = !show_types 67 val _ = (show_types := false) 68 val s = Parse.term_to_string tm 69 val _ = (show_types := saved_val) 70 in s 71 end 72 in tm2str ((snd o dest_eq o snd o dest_thm) HB_def) 73 end; 74 75val _ = add_vsynth 76 [(``\(sw:bool,in1:num,in2:num). if sw then in1 else in2``, 77 (fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3))), 78 (``\(sw:bool,in1:word,in2:word). if sw then in1 else in2``, 79 (fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3))), 80 (``\(sw:bool,in1:bool,in2:bool). if sw then in1 else in2``, 81 (fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3))), 82 (``(UNCURRY ($= :num->num->bool))``,(fn[inp1,inp2] => inp1 ^ " == " ^ inp2)), 83 (``(UNCURRY ($+ :num->num->num))``,(fn[inp1,inp2] => inp1 ^ " + " ^ inp2)), 84 (``(UNCURRY ($+ :word->word->word))``,(fn[inp1,inp2] => inp1 ^ " + " ^ inp2)), 85 (``(UNCURRY ($MOD :num->num->num))``,(fn[inp1,inp2] => inp1 ^ " % " ^ inp2)), 86 (``(UNCURRY ($* :num->num->num))``,(fn[inp1,inp2] => inp1 ^ " * " ^ inp2)), 87 (``(UNCURRY ($<< :word->num->word))``,(fn[inp1,inp2] => inp1 ^ " << " ^ inp2)), 88 (``(UNCURRY ($- :word->word->word))``,(fn[inp1,inp2] => inp1 ^ " - " ^ inp2)), 89 (``(UNCURRY ($- :num->num->num))``,(fn[inp1,inp2] => inp1 ^ " - " ^ inp2)), 90 (``(UNCURRY BIT)``,(fn[inp1,inp2] => ("("^inp2^" << ("^HB()^"-" ^inp1^")) >> "^HB()))), 91 (``(UNCURRY ($DIV :num->num->num))``,(fn[inp1,inp2] => inp1 ^ " / " ^ inp2)), 92 (``(UNCURRY $/\)``,(fn[inp1,inp2] => inp1 ^ " && " ^ inp2)), 93 (``(UNCURRY $\/)``,(fn[inp1,inp2] => inp1 ^ " || " ^ inp2)), 94 (``w2n``,(fn[inp] => inp)), 95 (``($~ :bool->bool)``,(fn[inp] => ("!" ^ inp))), 96 (``(BITS 31 1)``, 97 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+1)"))), 98 (``(BITS 1 0)``, 99 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-1)) >> (("^HB()^"-1)+0)"))), 100 (``(BITS 31 3)``, 101 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+3)"))), 102 (``(BITS 31 5)``, 103 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+5)"))), 104 (``(BITS 31 7)``, 105 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+7)"))), 106 (``(BITS 31 9)``, 107 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+9)"))), 108 (``(BITS 31 11)``, 109 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+11)"))), 110 (``(BITS 31 13)``, 111 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+13)"))), 112 (``(BITS 31 15)``, 113 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+15)"))), 114 (``(BITS 31 17)``, 115 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+17)"))), 116 (``(BITS 31 19)``, 117 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+19)"))), 118 (``(BITS 31 21)``, 119 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+21)"))), 120 (``(BITS 31 23)``, 121 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+23)"))), 122 (``(BITS 31 25)``, 123 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+25)"))), 124 (``(BITS 31 27)``, 125 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+27)"))), 126 (``(BITS 31 29)``, 127 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+29)"))), 128 (``(BITS HB 02)``, 129 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-" ^ HB()^")) >> (("^HB()^"-"^HB()^")+2)"))), 130 (``(BITS 31 02)``, 131 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-31)) >> (("^HB()^"-31)+2)"))), 132 (``(BITS (HB-2) 0)``, 133 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-(" ^ HB()^"-2))) >> (("^HB()^"-("^HB()^"-2))+0)"))), 134 (``(BITS 29 0)``, 135 (fn[inp] => ("(" ^ inp ^ " << (" ^ HB() ^ "-29)) >> (("^HB()^"-29)+0)"))) 136 ]; 137 138 139(*****************************************************************************) 140(* Turn of COMB_SYNTH_COMB messages *) 141(*****************************************************************************) 142val _ = (if_print_flag := false); 143 144(* --------------------------------------------------------------- 145 MOD_CNTWd counts the number of shifts to be performed 146 by MSHIFTd (it computes the argument count1 --- see the 147 functions MSHIFTd and NEXTd). 148 The constant WL is the word length. 149--------------------------------------------------------------- *) 150 151val _ = add_combinational ["MOD","WL","DIV","*","uBITS","BITS","HB","w2n","n2w", 152 "word_lsl","word_mul","word_add","word_sub", 153 "HB","BITT","BITTT"]; 154 155val (MOD_CNTWd_def,_,MOD_CNTWd_dev,MOD_CNTWd_comb,_) = hwDefine2 156 157 `MOD_CNTWd n = n MOD (WL DIV 2)`; 158 159<<<<<<< boothDevScript.sml 160val MOD_CNTWd_cir = 161 MAKE_NETLIST (REFINE (DEPTHR ATM_REFINE) MOD_CNTWd_dev); 162 MY_NETLIST [] (REFINE (DEPTHR ATM_REFINE) MOD_CNTWd_dev); 163======= 164 165>>>>>>> 1.7 166 167(* --------------------------------------------------------------- 168 MSHIFTd 169--------------------------------------------------------------- *) 170val (MSHIFTd_def,_,MSHIFTd_dev,MSHIFTd_comb,_) = hwDefine2 171 172 `MSHIFTd(borrow,mul,count1) = count1 * 2 + 173 if borrow /\ (mul=1) \/ 174 ~borrow /\ (mul=2) then 1 else 0`; 175 176 177(* --------------------------------------------------------------- 178 ALUd 179--------------------------------------------------------------- *) 180 181val (ALUd_def,_,ALUd_dev,ALUd_comb,_) = hwDefine2 182 183 `ALUd(borrow2,mul,alua,alub) = 184 if ~borrow2 /\ (mul = 0) \/ 185 borrow2 /\ (mul = 3) then 186 alua 187 else if borrow2 /\ (mul = 0) \/ (mul = 1) then 188 alua + alub 189 else 190 alua - alub`; 191 192<<<<<<< boothDevScript.sml 193val ALUd_cir = 194 MAKE_NETLIST (REFINE (DEPTHR ATM_REFINE) ALUd_dev); 195 MY_NETLIST [] (REFINE (DEPTHR ATM_REFINE) ALUd_dev); 196======= 197>>>>>>> 1.7 198 199(* --------------------------------------------------------------- 200 INITd 201 The initialisation function takes the input 202 (a,rm,rs,rn) and returns the initial state 203 (mul:num, mul2:num, borrow2:bool, mshift:num, rm:word,rd:word). 204 The variable rd stores the result of the multiplication. 205--------------------------------------------------------------- *) 206 207val (INITd_def,_,INITd_dev,INITd_comb,_) = hwDefine2 208 209 `INITd(a,rm:word,rs,rn) = (BITS 1 0 (w2n rs), 210 BITS HB 2 (w2n rs), 211 F, 212 if (BITS 1 0 (w2n rs)) = 2 then 1 else 0, 213 rm, 214 if a then rn else 0w)`; 215 216<<<<<<< boothDevScript.sml 217val INITd_cir = 218 MAKE_NETLIST (REFINE (DEPTHR ATM_REFINE) INITd_dev); 219 MY_NETLIST [] (REFINE (DEPTHR ATM_REFINE) INITd_dev); 220======= 221>>>>>>> 1.7 222 223(* --------------------------------------------------------------- 224 NEXTd computes the next state from the current one 225--------------------------------------------------------------- *) 226val (NEXTd_def,_,NEXTd_dev,NEXTd_comb,_) = hwDefine2 227 `NEXTd(mul,mul2,borrow2,mshift,rm:word,rd) = 228 (BITS 1 0 (BITS (HB-2) 0 mul2), 229 BITS HB 2 (BITS (HB-2) 0 mul2), 230 BIT 1 mul, 231 MSHIFTd(BIT 1 mul, 232 BITS 1 0 (BITS (HB-2) 0 mul2), 233 MOD_CNTWd (mshift DIV 2 +1)), 234 rm, 235 ALUd(borrow2,mul,rd,rm << mshift))`; 236 237 238(* --------------------------------------------------------------- 239 APPLY_NEXTd applies the next state function t times 240--------------------------------------------------------------- *) 241val (APPLY_NEXTd_def,_,APPLY_NEXTd_dev, 242 APPLY_NEXTd_comb,APPLY_NEXTd_tot) = hwDefine2 243 244 `(APPLY_NEXTd(t,inp) = if t=0 then inp 245 else APPLY_NEXTd(t-1,NEXTd inp)) 246 measuring FST`; 247 248 249(* --------------------------------------------------------------- 250 STATEd computes the initial state and applies the next 251 state function t times 252--------------------------------------------------------------- *) 253val (STATEd_def,_,STATEd_dev,STATEd_comb,_) = hwDefine2 254 255 `STATEd(t,(a,rm,rs,rn)) = APPLY_NEXTd(t,INITd(a,rm,rs,rn))`; 256 257 258(* --------------------------------------------------------------- 259 DURd returns the duration or the number of transitions 260 taken for the state-machine to compute the multiplication. 261--------------------------------------------------------------- *) 262val (DURd_def,_,DURd_dev,DURd_comb,_) = hwDefine2 263 264 `DURd w = if BITS 31 1 (w2n w) = 0 then 1 265 else if BITS 31 3 (w2n w) = 0 then 2 266 else if BITS 31 5 (w2n w) = 0 then 3 267 else if BITS 31 7 (w2n w) = 0 then 4 268 else if BITS 31 9 (w2n w) = 0 then 5 269 else if BITS 31 11 (w2n w) = 0 then 6 270 else if BITS 31 13 (w2n w) = 0 then 7 271 else if BITS 31 15 (w2n w) = 0 then 8 272 else if BITS 31 17 (w2n w) = 0 then 9 273 else if BITS 31 19 (w2n w) = 0 then 10 274 else if BITS 31 21 (w2n w) = 0 then 11 275 else if BITS 31 23 (w2n w) = 0 then 12 276 else if BITS 31 25 (w2n w) = 0 then 13 277 else if BITS 31 27 (w2n w) = 0 then 14 278 else if BITS 31 29 (w2n w) = 0 then 15 279 else 16`; 280 281 282(* --------------------------------------------------------------- 283 PROJ_RDd projects the result of the multiplication from 284 the state 285--------------------------------------------------------------- *) 286<<<<<<< boothDevScript.sml 287val (PROJ_RDd_def,_,PROJ_RDd_dev) = hwDefine 288======= 289val (PROJ_RDd_def,_,PROJ_RDd_dev,PROJ_RDd_comb,_) = hwDefine2 290 291>>>>>>> 1.7 292 `PROJ_RDd(mul:num, mul2:num, borrow2:bool, 293 mshift:num, rm:word32, rd:word32) = rd`; 294 295 296(* --------------------------------------------------------------- 297 BOOTHMULTIPLYd 298 The correctness theorem for the original BOOTHMULTIPLY states 299 that |- BOOTHMULTPLY a rm rs rn 300 = (rm * rs + (if a then rn else 0w)) 301--------------------------------------------------------------- *) 302val (BOOTHMULTIPLYd_def,_,BOOTHMULTIPLYd_dev, 303 BOOTHMULTIPLYd_comb,_) = hwDefine2 304 305 `BOOTHMULTIPLYd(a,rm,rs,rn) = PROJ_RDd(STATEd(DURd rs,a,rm,rs,rn))`; 306 307 308 309(* --------------------------------------------------------------- 310 MULTd is the main function. 311--------------------------------------------------------------- *) 312val (MULTd_def,_,MULTd_dev,MULTd_comb,_) = hwDefine2 313 314 `MULTd(a,b) = BOOTHMULTIPLYd(F,a,b,0w)`; 315 316 317 318(* --------------------------------------------------------------- 319 Refinement 320 The atomic operators are: 321 w2n, BIT, BITS, =, -, DIV 2, +, MOD, * 2, /\, ~, \/, << 322--------------------------------------------------------------- *) 323val MULTd_dev = save_thm("MULTd_dev", 324 REFINE (DEPTHR (LIB_REFINE [BOOTHMULTIPLYd_dev]) 325 THENR DEPTHR (LIB_REFINE [DURd_dev,STATEd_dev,PROJ_RDd_dev]) 326 THENR DEPTHR (LIB_REFINE [INITd_dev,APPLY_NEXTd_dev]) 327 THENR DEPTHR (LIB_REFINE [NEXTd_dev]) 328 THENR DEPTHR (LIB_REFINE [ALUd_dev,MSHIFTd_dev,MOD_CNTWd_dev]) 329 THENR DEPTHR ATM_REFINE) MULTd_dev); 330 331 332(* --------------------------------------------------------------- 333 Proofs 334--------------------------------------------------------------- *) 335 336(* --------------------------------------------------------------- 337 MOD_CNTWd = MOD_CNTW 338--------------------------------------------------------------- *) 339val MOD_CNTW_EQ = store_thm("MOD_CNTW_EQ", 340 ``MOD_CNTWd = MOD_CNTW``, 341 METIS_TAC [MOD_CNTWd_def,MOD_CNTW_def]); 342 343 344(* --------------------------------------------------------------- 345 MSHIFTd(a,b,c) = MSHIFT a b c 346--------------------------------------------------------------- *) 347val MSHIFT_EQ = store_thm("MSHIFT_EQ", 348 ``!a b c. MSHIFTd(a,b,c) = (MSHIFT a b c)``, 349 RW_TAC arith_ss [MSHIFTd_def,MSHIFT_def]); 350 351 352(* --------------------------------------------------------------- 353 ALUd(a,b,c,d) = ALU a b c d 354--------------------------------------------------------------- *) 355val ALU_EQ = store_thm("ALU_EQ", 356 ``!a b c d. ALUd(a,b,c,d) = (ALU a b c d)``, 357 RW_TAC arith_ss [ALUd_def,ALU_def]); 358 359 360(* --------------------------------------------------------------- 361 T2B converts a tuple into a state (type state_BOOTH) 362--------------------------------------------------------------- *) 363val T2B_def = Define `T2B(a,b,c,d,e,f) = BOOTH a b c d e f`; 364 365 366(* --------------------------------------------------------------- 367 T2B(INITd(a,b,c,d)) = INIT a b c d 368--------------------------------------------------------------- *) 369val INIT_EQ = store_thm("INIT_EQ", 370 ``!a b c d. T2B(INITd(a,b,c,d)) = (INIT a b c d)``, 371 RW_TAC arith_ss [T2B_def,INITd_def,INIT_def] 372 THEN `(mul1 = w2n c) /\ (count1 = 0) /\ 373 (mul = BITS 1 count1 mul1) /\ 374 (mshift = (if mul = 2 then 1 else count1))` 375 by RW_TAC arith_ss [] 376 THEN RW_TAC arith_ss []); 377 378 379(* --------------------------------------------------------------- 380 T2B(NEXTd a) = NEXT(T2B a) 381--------------------------------------------------------------- *) 382val NEXT_EQ = store_thm("NEXT_EQ", 383 ``!a. T2B(NEXTd a) = (NEXT (T2B a))``, 384 Cases_on `a` 385 THEN Cases_on `r` 386 THEN Cases_on `r1` 387 THEN Cases_on `r` 388 THEN Cases_on `r1` 389 THEN RW_TAC arith_ss [NEXTd_def,NEXT_def,T2B_def] 390 THEN `(mshift' = MSHIFT borrow mul' count1) /\ 391 (count1 = MOD_CNTW (q3 DIV 2 + 1)) /\ 392 (rd' = ALU q2 q r alub)` by RW_TAC arith_ss [] 393 THEN RW_TAC arith_ss [MSHIFT_EQ,MOD_CNTW_EQ,ALU_EQ]); 394 395 396 397(* --------------------------------------------------------------- 398 T2B(STATEd(a,b,c,d,e)) = STATE a b c d e 399 400 This theorem makes use of some definitions and lemmas. 401--------------------------------------------------------------- *) 402 403(* --------------------------------------------- 404 (fEXP f n) applies f n times to some input 405--------------------------------------------- *) 406val fEXP_def = Define 407 `(fEXP f 0 = (\x.x)) /\ 408 (fEXP f (SUC n) = ((fEXP f n) o f))`; 409 410(* --------------------------------------------- 411 fEXP_LEMMA 412--------------------------------------------- *) 413val fEXP_LEMMA = store_thm("fEXP_LEMMA", 414 ``!f n inp. f (fEXP f n inp) 415 = (fEXP f (SUC n) inp)``, 416 Induct_on `n` 417 THEN METIS_TAC [fEXP_def,o_THM]); 418 419(* --------------------------------------------- 420 fEXP_NEXT 421--------------------------------------------- *) 422val fEXP_NEXT = store_thm("fEXP_NEXT", 423 ``!a. T2B(fEXP NEXTd n a) = fEXP NEXT n (T2B a)``, 424 Induct_on `n` 425 THENL [ 426 METIS_TAC[fEXP_def] 427 , 428 RW_TAC arith_ss [fEXP_def] 429 THEN REPEAT GEN_TAC 430 THEN METIS_TAC [fEXP_def,o_THM,NEXT_EQ] 431 ]); 432 433(* --------------------------------------------- 434 fEXP_APPLY_NEXTd 435--------------------------------------------- *) 436val fEXP_APPLY_NEXTd = store_thm("fEXP_APPLY_NEXTd", 437 ``!n inp. APPLY_NEXTd (n,inp) = fEXP NEXTd n inp``, 438 Induct_on `n` 439 THENL [ 440 METIS_TAC [APPLY_NEXTd_def,fEXP_def] 441 , 442 `~(SUC n = 0) /\ (SUC n - 1 = n)` 443 by RW_TAC arith_ss [] 444 THEN METIS_TAC [APPLY_NEXTd_def,fEXP_def, 445 o_THM,NEXT_EQ] 446 ]); 447 448(* --------------------------------------------- 449 fEXP_STATE 450--------------------------------------------- *) 451val fEXP_STATE = store_thm("fEXP_STATE", 452 ``!n b c d e. STATE n b c d e 453 = (fEXP NEXT n (INIT b c d e))``, 454 Induct_on `n` 455 THEN METIS_TAC [STATE_def,fEXP_def,fEXP_LEMMA]); 456 457(* -------------------------------------------- 458 T2B(STATEd(a,b,c,d,e)) = STATE a b c d e 459-------------------------------------------- *) 460val STATE_EQ = store_thm("STATE_EQ", 461 ``!a b c d e. T2B(STATEd(a,b,c,d,e)) = (STATE a b c d e)``, 462 REPEAT GEN_TAC 463 THEN `T2B(STATEd(a,b,c,d,e)) = (fEXP NEXT a (T2B(INITd(b,c,d,e))))` 464 by METIS_TAC [STATEd_def,APPLY_NEXTd_def,fEXP_APPLY_NEXTd,fEXP_NEXT] 465 THEN METIS_TAC [INIT_EQ,fEXP_STATE]); 466 467 468 469(* --------------------------------------------------------------- 470 DURd = DUR 471--------------------------------------------------------------- *) 472val DUR_EQ = store_thm("DUR_EQ", 473 ``DUR = DURd``, 474 `!w. DUR w = DURd w` by REWRITE_TAC [] 475 THENL [GEN_TAC 476 THEN `w = n2w(w2n w)` by METIS_TAC [word32Theory.w2n_ELIM] 477 THEN RW_TAC std_ss [DURd_def] 478 THEN METIS_TAC [DUR_EVAL] 479 , 480 METIS_TAC [] 481 ]); 482 483 484 485 486(* --------------------------------------------------------------- 487 PROJ_RDd a = PROJ_RD(T2B a) 488--------------------------------------------------------------- *) 489val PROJ_RD_EQ = store_thm("PROJ_RD_EQ", 490 ``!a. PROJ_RDd a = PROJ_RD(T2B a)``, 491 Cases_on `a` THEN 492 Cases_on `r` THEN 493 Cases_on `r1` THEN 494 Cases_on `r` THEN 495 Cases_on `r1` THEN 496 RW_TAC arith_ss [PROJ_RDd_def,PROJ_RD_def,T2B_def]); 497 498 499 500(* --------------------------------------------------------------- 501 BOOTHMULTIPLYd(a,b,c,d) = BOOTHMULTIPLY a b c d 502--------------------------------------------------------------- *) 503val BOOTHMULTIPLY_EQ = store_thm("BOOTHMULTIPLY_EQ", 504 ``!a b c d. BOOTHMULTIPLYd(a,b,c,d) = (BOOTHMULTIPLY a b c d)``, 505 `!a b c d. STATE (DURd c) a b c d = (T2B(STATEd(DURd c,a,b,c,d)))` 506 by METIS_TAC [STATE_EQ] 507 THEN `!a b c d. PROJ_RD(STATE (DURd c) a b c d) 508 = (PROJ_RD(T2B(STATEd(DURd c,a,b,c,d))))` 509 by METIS_TAC [STATE_EQ] 510 THEN RW_TAC arith_ss [BOOTHMULTIPLYd_def,BOOTHMULTIPLY_def,DUR_EQ] 511 THEN METIS_TAC [PROJ_RD_EQ]); 512 513 514 515(* --------------------------------------------------------------- 516 Define 517 |- MULT32(w1,w2) = w1 * w2 518 to avoid pretty printer problems 519--------------------------------------------------------------- *) 520val MULT32_def = 521 Define 522 `MULT32(w1,w2) = w1 * w2`; 523 524(* --------------------------------------------------------------- 525 MULTd = MULT32 526--------------------------------------------------------------- *) 527val MULTd_CORRECT = store_thm("MULTd_CORRECT", 528 ``MULTd = MULT32``, 529 `MULT32 = UNCURRY $*` 530 by RW_TAC std_ss [FUN_EQ_THM,UNCURRY,MULT32_def,FORALL_PROD] 531 THEN POP_ASSUM(fn th => RW_TAC std_ss [th]) 532 THEN `!a b. MULTd(a,b) = a*b` 533 by METIS_TAC [MULTd_def,BOOTHMULTIPLY_EQ,CORRECT,word32Theory.WORD_ADD_0] 534 THEN `!a b. MULTd(a,b) = a*b` by METIS_TAC [MULTd_def, CORRECT, BOOTHMULTIPLY_EQ] 535 THEN `!a b. (\p. MULTd p = UNCURRY $* p) (a,b)` by RW_TAC arith_ss [] 536 THEN `?P. P = (\p. MULTd p = UNCURRY $* p)` by RW_TAC arith_ss [] 537 THEN `!p. (\p. MULTd p = UNCURRY $* p) p` by METIS_TAC [pair_induction] 538 THEN `!p. MULTd p = UNCURRY $* p` by metisLib.METIS_TAC [pair_induction] 539 THEN PROVE_TAC [(PairRules.PEXT (ASSUME ``!p. MULTd p = UNCURRY $* p``))]); 540 541(* --------------------------------------------------------------- 542 Circuit ===> Dev MULT32 543--------------------------------------------------------------- *) 544val MULTd_dev0 = save_thm("MULTd", 545 REWRITE_RULE [MULTd_CORRECT] MULTd_dev); 546 547val MULTd_dev = inlineCompile (fst(dest_eq(concl MULTd_comb))) 548 [BOOTHMULTIPLYd_comb, 549 DURd_comb,STATEd_comb,PROJ_RDd_comb, 550 INITd_comb,APPLY_NEXTd_comb, 551 NEXTd_comb,ALUd_comb,MSHIFTd_comb, 552 MOD_CNTWd_comb, MULTd_comb] 553 [APPLY_NEXTd_tot]; 554 555(* runtime: 39.867s, gctime: 14.104s, systime: 0.155s. 556val MULTd_net = time MAKE_NETLIST MULTd_dev; 557time (MY_NETLIST []) MULTd_dev; 558 559 Takes rather a long time: 560val MULTd_cir = time MAKE_CIRCUIT MULTd_dev; 561val MULTd_cir = MAKE_CIRCUIT ((SIMP_RULE std_ss [DIVISION,WL_def,HB_def]) 562 MULTd_dev); 563*) 564 565val MULTd_cir = NEW_MAKE_CIRCUIT ((SIMP_RULE std_ss [DIVISION,WL_def,HB_def]) 566 MULTd_dev); 567 568(* 569val _ = PRINT_VERILOG MULTd_cir; 570 571val _ = load "fpgaCodeGenerator"; 572val _ = fpgaCodeGenerator.programFPGA MULTd_cir; 573*) 574 575 576(* Simulation 577val period = 5; 578val file_name = "MULTd_SIM"; 579val thm = MULTd_cir; 580val stimulus =[("inp1", "5"),("inp2","7")]; 581val name = "MULTd_SIM"; 582val dump_all = true; 583 584printToFile "MULTd_SIM.vl" (MAKE_SIMULATION name thm period stimulus dump_all); 585*) 586 587 588(*****************************************************************************) 589(* Temporary hack to work around a system prettyprinter bug *) 590(*****************************************************************************) 591val _ = temp_overload_on(" * ", numSyntax.mult_tm); 592 593val _ = export_theory(); 594