diff options
Diffstat (limited to 'src/hls/PrintVerilog.ml')
| -rw-r--r-- | src/hls/PrintVerilog.ml | 40 |
1 files changed, 21 insertions, 19 deletions
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index da3bd6e..46b001e 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -76,14 +76,14 @@ let pprint_binop l r = let unop = function | Vneg -> " - " - | Vnot -> " ! " + | Vnot -> " ~ " let register a = match PMap.find_opt a !name_map with | Some s -> s | None -> sprintf "reg_%d" (P.to_int a) -(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) +(*let literal l = s printf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) let literal l = let l' = camlint_of_coqint l in @@ -119,7 +119,9 @@ let rec pprint_stmnt i = indent i; "end\n" ] | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case (List.sort compare_expr es |> List.rev); + fold_map pprint_case (stmnt_to_list es + |> List.sort compare_expr + |> List.rev); indent (i+1); "default:;\n"; indent i; "endcase\n" ] @@ -138,22 +140,22 @@ let pprint_edge_top i = function | Valledge -> "@*" | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] -let declare t = +let declare (t, i) = function (r, sz) -> concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; - register r; ";\n" ] + register r; if i then " = 0;\n" else ";\n" ] -let declarearr t = +let declarearr (t, _) = function (r, sz, ln) -> concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] let print_io = function - | Some Vinput -> "input logic" - | Some Voutput -> "output logic" - | Some Vinout -> "inout logic" - | None -> "logic" + | Some Vinput -> "input", false + | Some Voutput -> "output logic", true + | Some Vinout -> "inout", false + | None -> "logic", true let decl i = function | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] @@ -163,11 +165,14 @@ let decl i = function let pprint_module_item i = function | Vdeclaration d -> decl i d | Valways (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_ff (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_comb (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] let rec intersperse c = function | [] -> [] @@ -176,7 +181,7 @@ let rec intersperse c = function let make_io i io r = concat [indent i; io; " "; register r; ";\n"] -let print_funct_units clk = function +(**let print_funct_units clk = function | SignedDiv (stages, numer, denom, quot, rem) -> sprintf ("div_signed #(.stages(%d)) divs(.clk(%s), " ^^ ".clken(1'b1), .numer(%s), .denom(%s), " ^^ @@ -188,7 +193,7 @@ let print_funct_units clk = function ".clken(1'b1), .numer(%s), .denom(%s), " ^^ ".quotient(%s), .remain(%s))\n") (P.to_int stages) - (register clk) (register numer) (register denom) (register quot) (register rem) + (register clk) (register numer) (register denom) (register quot) (register rem)*) let compose f g x = g x |> f @@ -260,10 +265,7 @@ let pprint_module debug i n m = ]; concat [ indent i; "module "; (extern_atom n); "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; - fold_map (pprint_module_item (i+1)) m.mod_body; - concat (List.map (print_funct_units m.mod_clk) - (Maps.PTree.elements m.mod_funct_units.avail_units - |> List.map snd)); + fold_map (pprint_module_item (i+1)) (List.rev m.mod_body); if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; if debug then debug_always_verbose i m.mod_clk m.mod_st else ""; indent i; "endmodule\n\n" |