diff options
Diffstat (limited to 'src/hls/Veriloggen.v')
| -rw-r--r-- | src/hls/Veriloggen.v | 76 |
1 files changed, 55 insertions, 21 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 6ea00e0..035e7a4 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -25,6 +25,7 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. +Require Import vericert.hls.FunctionalUnits. Definition transl_list_fun (a : node * Verilog.stmnt) := let (n, stmnt) := a in @@ -42,28 +43,61 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. +Definition inst_ram clk ram := + Valways (Vnegedge clk) + (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) + (Vseq (Vcond (Vvar (ram_wr_en ram)) + (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) + (Vvar (ram_d_in ram))) + (Vnonblock (Vvar (ram_d_out ram)) + (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) + (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) + Vskip). + 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.(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.(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) - m.(HTL.mod_funct_units) - body - m.(HTL.mod_entrypoint). + let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in + let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in + match m.(HTL.mod_ram) with + | Some ram => + let body := + 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)) + :: inst_ram m.(HTL.mod_clk) ram + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + 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.(HTL.mod_entrypoint) + | None => + let body := + 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.(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.(HTL.mod_entrypoint) + end. Definition transl_fundef := transf_fundef transl_module. |