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