1(*****************************************************************************)
2(* The sources have lots of cut-and-paste-and-tweak style repetition for the *)
3(* various combinational components (NOT, AND, OR, MUX, ADD, SUB, LESS, EQ). *)
4(* I may eventually implement some generic tools to make adding new          *)
5(* combinational components a one-liner. However, this will be a tricky      *)
6(* and possibly -- at least for now -- not worth the effort, since adding    *)
7(* new components is likely to be relatively rare.                           *)
8(*                                                                           *)
9(* Here are the steps currently needed to add a new component,               *)
10(* illustrated with the addition of 32-bit bitwise exclusive-or (XOR32).     *)
11(*****************************************************************************)
12
13(*****************************************************************************)
14(* Step 1                                                                    *)
15(* ------                                                                    *)
16(* Define the component in HOL                                               *)
17(* (assumes wordsTheory loaded and open)                                     *)
18(*****************************************************************************)
19val XOR32_def =
20 Define 
21  `XOR32(in1:num->word32,in2,out) = !t. out t = (in1 t) ?? (in2 t)`;
22
23(*****************************************************************************)
24(* Step 2                                                                    *)
25(* ------                                                                    *)
26(* Prove some boilerplate theorems and add to global lists:                  *)
27(*****************************************************************************)
28val COMB_XOR32 =
29 store_thm
30  ("COMB_XOR32",
31   ``COMB (UNCURRY $??) (in1 <> in2, out) = XOR32(in1,in2,out)``,
32   RW_TAC std_ss [COMB_def,BUS_CONCAT_def,XOR32_def]);
33
34add_combinational_components[COMB_XOR32];
35
36val XOR32_at =
37 store_thm
38  ("XOR32_at",
39   ``XOR32(in1,in2,out)
40     ==>
41     XOR32(in1 at clk,in2 at clk,out at clk)``,
42   RW_TAC std_ss [XOR32_def,at_def,tempabsTheory.when]);
43
44add_temporal_abstractions[XOR32_at];
45
46(*****************************************************************************)
47(* Step 3                                                                    *)
48(* ------                                                                    *)
49(* Define a Verilog module as an ML string (XOR32vDef), a function to        *)
50(* create an instance with a given size as a string (XOR32vInst), an         *)
51(* instance counter (XOR32vInst_count -- used to create unique names for     *)
52(* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as   *)
53(* an instance, using the type of ``out`` to compute the word width          *)
54(* needed to set parameter "size" in XOR32vDef (termToVerilog_XOR32).        *)
55(* These functions are added to a couple of global lists.                    *)
56(*****************************************************************************)
57val XOR32vDef =
58"// Combinational bitwise XOR32\n\
59\module XOR32 (in1,in2,out);\n\
60\ parameter size = 31;\n\
61\ input  [size:0] in1,in2;\n\
62\ output [size:0] out;\n\
63\\n\
64\ assign out = in1 ^ in2;\n\
65\\n\
66\endmodule\n\
67\\n";
68
69val XOR32vInst_count = ref 0;
70fun XOR32vInst (out:string->unit) [("size",size)] [in1_name,in2_name,out_name] =
71 let val count = !XOR32vInst_count
72     val _ = (XOR32vInst_count := count+1);
73     val inst_name = "XOR32" ^ "_" ^ Int.toString count
74 in
75 (out " XOR32        "; out inst_name;
76  out " (";out in1_name;out",";out in2_name;out",";out out_name; out ");\n";
77  out "   defparam ";out inst_name; out ".size = "; out size;
78  out ";\n\n")
79 end;
80
81add_module ("XOR32", (XOR32vDef, XOR32vInst));
82
83fun termToVerilog_XOR32 (out:string->unit) tm =
84 if is_comb tm
85     andalso is_const(fst(strip_comb tm))
86     andalso (fst(dest_const(fst(strip_comb tm))) = "XOR32")
87     andalso is_pair(rand tm)
88     andalso (length(strip_pair(rand tm)) = 3)
89     andalso all is_var (strip_pair(rand tm))
90  then XOR32vInst
91        out
92        [("size", var2size(last(strip_pair(rand tm))))]
93        (map (fst o dest_var) (strip_pair(rand tm)))
94  else raise ERR "termToVerilog_XOR32" "bad component term";
95
96termToVerilogLib := (!termToVerilogLib) @ [termToVerilog_XOR32];
97
98
99
100
101