diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-16 21:40:39 +0000 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 19:21:43 +0000 |
| commit | ac9e9d76118833ceb098ad9111fff338bb5a7423 (patch) | |
| tree | 62c50d09f0c27cd705c409a323f07a081d81dc6f /src/verilog | |
| parent | dfaa3a9cbc07649feea3220693a8a854a32eafb6 (diff) | |
| download | vericert-ac9e9d76118833ceb098ad9111fff338bb5a7423.tar.gz vericert-ac9e9d76118833ceb098ad9111fff338bb5a7423.zip | |
Print all modules in verilog output
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index c513c8d..ca06038 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -74,7 +74,7 @@ let unop = function | Vnot -> " ! " let register a = sprintf "reg_%d" (P.to_int a) -let mod_name a = sprintf "module_%d" (P.to_int a) +let vmodule a = sprintf "module_%d" (P.to_int a) let instance a = sprintf "instance_%d" (P.to_int a) (*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) @@ -108,7 +108,7 @@ let rec pprint_stmnt i = ] | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] - | Vinstantiate (m, name, args) -> concat [ indent i; ident m; " "; ident name; + | Vinstantiate (m, name, args) -> concat [ indent i; vmodule m; " "; instance name; "("; concat (intersperse ", " (List.map register args)); ")"; ";\n" ] @@ -204,17 +204,15 @@ let print_initial i n stk = concat [ ] let pprint_module debug i n m = - if (extern_atom n) = "main" then - let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in - let outputs = [m.mod_finish; m.mod_return] in - 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; - if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; - if debug then debug_always i m.mod_clk m.mod_st else ""; - indent i; "endmodule\n\n" - ] - else "" + let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in + let outputs = [m.mod_finish; m.mod_return] in + 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; + if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; + if debug then debug_always i m.mod_clk m.mod_st else ""; + indent i; "endmodule\n\n" + ] let print_result pp lst = let rec print_result_in pp = function |