diff options
Diffstat (limited to 'src/hls/Veriloggen.v')
-rw-r--r-- | src/hls/Veriloggen.v | 41 |
1 files changed, 23 insertions, 18 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..80c0669 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -16,10 +16,15 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Maps. -From compcert Require Errors. -From compcert Require Import AST. -From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. Definition transl_list_fun (a : node * Verilog.stmnt) := let (n, stmnt) := a in @@ -41,23 +46,23 @@ 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 let body := - Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) - (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)) + Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) + (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.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 - Verilog.mkmodule m.(mod_start) - m.(mod_reset) - m.(mod_clk) - m.(mod_finish) - m.(mod_return) - m.(mod_st) - m.(mod_stk) - m.(mod_stk_len) - m.(mod_params) + Verilog.mkmodule m.(HTL.mod_start) + m.(HTL.mod_reset) + m.(HTL.mod_clk) + m.(HTL.mod_finish) + m.(HTL.mod_return) + m.(HTL.mod_st) + m.(HTL.mod_stk) + m.(HTL.mod_stk_len) + m.(HTL.mod_params) body - m.(mod_entrypoint). + m.(HTL.mod_entrypoint). Definition transl_fundef := transf_fundef transl_module. |