1(*****************************************************************************) 2(* Example to illiustrate adding a component: XOR32 (see ../README). *) 3(*****************************************************************************) 4 5quietdec := true; 6loadPath := "../" :: "../dff/" :: !loadPath; 7map load 8 ["compileTheory","compile","metisLib","intLib","wordsLib", 9 "dffTheory","vsynth"]; 10open compile metisLib wordsTheory; 11open arithmeticTheory intLib pairLib pairTheory PairRules combinTheory 12 devTheory composeTheory compileTheory compile vsynth dffTheory; 13quietdec := false; 14 15infixr 3 THENR; 16infixr 3 ORELSER; 17intLib.deprecate_int(); 18 19(*****************************************************************************) 20(* Boilerplate. Probably more than is needed. *) 21(*****************************************************************************) 22add_combinational ["MOD","DIV"]; 23add_combinational ["word_add","word_sub"]; 24add_combinational ["BITS","w2n","n2w"]; 25 26(*****************************************************************************) 27(* Start new theory "Xor32" *) 28(*****************************************************************************) 29val _ = new_theory "Xor32"; 30 31(*****************************************************************************) 32(* Add definition of XOR32 *) 33(*****************************************************************************) 34AddBinop ("XOR32", (``UNCURRY $?? : word32#word32->word32``, "^")); 35 36(*****************************************************************************) 37(* Implement an atomic device computing XOR *) 38(*****************************************************************************) 39val (Xor32,_,Xor32_dev) = 40 hwDefine 41 `Xor32(in1:word32,in2) = in1 ?? in2`; 42 43(*****************************************************************************) 44(* Derivation using refinement combining combinators *) 45(*****************************************************************************) 46val Xor32Imp_dev = 47 REFINE 48 (DEPTHR ATM_REFINE) 49 Xor32_dev; 50 51val Xor32_cir = 52 save_thm 53 ("Xor32_cir", 54 time MAKE_CIRCUIT Xor32Imp_dev); 55 56(*****************************************************************************) 57(* This dumps changes to all variables. Set to false to dump just the *) 58(* changes to module Xor32. *) 59(*****************************************************************************) 60dump_all_flag := true; 61 62verilog_simulator := iverilog; 63waveform_viewer := gtkwave; 64 65(*****************************************************************************) 66(* Stop zillions of warning messages that HOL variables of type ``:num`` *) 67(* are being converted to Verilog wires or registers of type [31:0]. *) 68(*****************************************************************************) 69numWarning := false; 70 71SIMULATE Xor32_cir [("inp1","537"),("inp2","917")]; 72 73val _ = export_theory(); 74