diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-02 10:26:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-02 10:26:34 +0000 |
| commit | 5b2e88abeb23ac8b6e570e8c80422e3635088891 (patch) | |
| tree | 1eb513b964a46035a6888a3e04cdfab4999590b2 | |
| parent | a2199f6bf69ae5cbbdb15227f8828b914baa4348 (diff) | |
| download | vericert-5b2e88abeb23ac8b6e570e8c80422e3635088891.tar.gz vericert-5b2e88abeb23ac8b6e570e8c80422e3635088891.zip | |
Add Verilog generation for rams
| -rw-r--r-- | src/hls/Veriloggen.v | 65 |
1 files changed, 47 insertions, 18 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 894d309..cf36d27 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -42,27 +42,56 @@ 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 stk addr d_in d_out wr_en := + Valways (Vnegedge clk) + (Vcond (Vvar wr_en) + (Vnonblock (Vvari stk (Vvar addr)) (Vvar d_in)) + (Vnonblock (Vvar d_out) (Vvari stk (Vvar addr)))). + Definition transl_module (m : HTL.module) : Verilog.module := 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 - 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). + match m.(HTL.mod_ram) with + | Some (addr, d_in, d_out, wr_en) => + 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) m.(HTL.mod_stk) addr d_in d_out wr_en + :: 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. |