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