diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 16:40:45 +0000 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 19:21:43 +0000 |
| commit | 982e6c69a52e8ec4e677147004cc5472f8a80d6d (patch) | |
| tree | ddbbebe17b3bfdf8069ab03735b5f0749839eb17 | |
| parent | 9b87637d3e4d6a75dee1221b017e3ccf6632642e (diff) | |
| download | vericert-982e6c69a52e8ec4e677147004cc5472f8a80d6d.tar.gz vericert-982e6c69a52e8ec4e677147004cc5472f8a80d6d.zip | |
Translate instantiations from HTL to verilog
| -rw-r--r-- | src/translation/Veriloggen.v | 5 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 1 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 3 |
3 files changed, 7 insertions, 2 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index a0be0fa..772dc89 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -37,6 +37,8 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. +Definition inst_to_Vdecl := map (fun (a: positive * instantiation) => match a with (_, decl) => Vinstancedecl decl end). + Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in @@ -46,7 +48,8 @@ Definition transl_module (m : HTL.module) : Verilog.module := (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls)) + ++ inst_to_Vdecl (AssocMap.elements m.(mod_insts))) in Verilog.mkmodule m.(mod_start) m.(mod_reset) m.(mod_clk) diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index da4dd5d..a2fd78f 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -148,6 +148,7 @@ let print_io = function let decl i = function | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] + | Vinstancedecl inst -> concat [indent i; pprint_instantiation inst] (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 8847615..4f5c838 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -208,7 +208,8 @@ Inductive io : Type := Inductive declaration : Type := | Vdecl : option io -> reg -> nat -> declaration -| Vdeclarr : option io -> reg -> nat -> nat -> declaration. +| Vdeclarr : option io -> reg -> nat -> nat -> declaration +| Vinstancedecl : instantiation -> declaration. Inductive module_item : Type := | Vdeclaration : declaration -> module_item |