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