1(*****************************************************************************) 2(* Another example to illiustrate adding a component (see ../README). *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* Boilerplate theory loading stuff *) 7(*****************************************************************************) 8quietdec := true; 9loadPath := "../" :: "../dff/" :: !loadPath; 10app load 11 ["compileTheory","compile","metisLib","intLib", "wordsLib", 12 "dffTheory","vsynth"]; 13open compile metisLib wordsTheory; 14open arithmeticTheory intLib pairLib pairTheory PairRules combinTheory 15 devTheory composeTheory compileTheory compile vsynth dffTheory; 16quietdec := false; 17 18infixr 3 THENR; 19infixr 3 ORELSER; 20intLib.deprecate_int(); 21 22(*****************************************************************************) 23(* More boilerplate. Declaring combinational logic functions. *) 24(* Probably more than is needed. *) 25(*****************************************************************************) 26add_combinational ["MOD","DIV"]; 27add_combinational ["word_add","word_sub"]; 28add_combinational ["BITS","w2n","n2w"]; 29 30(*****************************************************************************) 31(* Start new theory "NotXor32" *) 32(*****************************************************************************) 33val _ = new_theory "NotXor32"; 34 35(*****************************************************************************) 36(* Add definitions of XOR32 and NOT32 *) 37(*****************************************************************************) 38AddBinop ("XOR32", (``UNCURRY $?? : word32#word32->word32``, "^")); 39add_vsynth [(``word_1comp:word32->word32``, fn l => ("~ " ^ hd l))]; 40add_vsynth [(``\(sel:bool,in1:word32,in2:word32). if sel then in1 else in2``, 41 fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3))]; 42 43(*****************************************************************************) 44(* Implement an atomic device computing XOR *) 45(*****************************************************************************) 46val (NotXor32,_,NotXor32_dev) = 47 hwDefine 48 `NotXor32(in1:word32,in2) = ((in1 ?? in2), ~(in1 ?? in2))`; 49 50(*****************************************************************************) 51(* Derivation using refinement combining combinators *) 52(*****************************************************************************) 53val NotXor32Imp_dev = 54 REFINE 55 (DEPTHR ATM_REFINE) 56 NotXor32_dev; 57 58val NotXor32_cir = 59 save_thm 60 ("NotXor32_cir", 61 time MAKE_CIRCUIT NotXor32Imp_dev); 62 63(*****************************************************************************) 64(* This dumps changes to all variables. Set to false to dump just the *) 65(* changes to module NotXor32. *) 66(*****************************************************************************) 67dump_all_flag := true; 68 69verilog_simulator := iverilog; 70waveform_viewer := gtkwave; 71 72SIMULATE NotXor32_cir [("inp1","537"),("inp2","917")]; 73 74val _ = export_theory(); 75