1 2val NOT32_def = 3 Define 4 `NOT32(inp,out) = !t. out t = ~(inp t : word32)`; 5 6val COMB_NOT32 = 7 store_thm 8 ("COMB_NOT32", 9 ``COMB ($~:word32->word32) (inp, out) = NOT32(inp,out)``, 10 RW_TAC std_ss [COMB_def,BUS_CONCAT_def,NOT32_def]); 11 12add_combinational_components[COMB_NOT32]; 13 14val NOT32_at = 15 store_thm 16 ("NOT32_at", 17 ``NOT32(inp,out) 18 ==> 19 NOT32(inp at clk,out at clk)``, 20 RW_TAC std_ss [NOT32_def,at_def,tempabsTheory.when]); 21 22add_temporal_abstractions[NOT32_at]; 23 24val NOT32vDef = 25"// Combinational 32-bit inverter\n\ 26\module NOT32 (inp,out);\n\ 27\ parameter size = 31;\n\ 28\ input [size:0] inp;\n\ 29\ output [size:0] out;\n\ 30\\n\ 31\ assign out = ~inp;\n\ 32\\n\ 33\endmodule\n\ 34\\n"; 35 36val NOT32vInst_count = ref 0; 37fun NOT32vInst (out:string->unit) [("size",size)] [inp_name,out_name] = 38 let val count = !NOT32vInst_count 39 val _ = (NOT32vInst_count := count+1); 40 val inst_name = "NOT32" ^ "_" ^ Int.toString count 41 in 42 (out " NOT32 "; out inst_name; 43 out " (";out inp_name;out",";out out_name; out ");\n"; 44 out " defparam ";out inst_name; out ".size = "; out size; 45 out ";\n\n") 46 end; 47 48add_module ("NOT32", NOT32vDef); 49 50fun termToVerilog_NOT32 (out:string->unit) tm = 51 if is_comb tm 52 andalso is_const(fst(strip_comb tm)) 53 andalso (fst(dest_const(fst(strip_comb tm))) = "NOT32") 54 andalso is_pair(rand tm) 55 andalso (length(strip_pair(rand tm)) = 2) 56 andalso all is_var (strip_pair(rand tm)) 57 then NOT32vInst 58 out 59 [("size", var2size(last(strip_pair(rand tm))))] 60 (map (fst o dest_var) (strip_pair(rand tm))) 61 else raise ERR "termToVerilog_NOT32" "bad component term"; 62 63termToVerilogLib := (!termToVerilogLib) @ [termToVerilog_NOT32]; 64 65 66 67 68