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