From 540b1fb0494e6207d6bee63721dc5deee30e1c02 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 9 Mar 2021 22:20:17 +0000 Subject: Update RAM generation proofs --- src/hls/Veriloggen.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'src/hls/Veriloggen.v') diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 3defe9c..26dba7a 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -42,23 +42,27 @@ 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 := +Definition inst_ram clk ram := Valways (Vnegedge clk) - (Vcond (Vvar wr_en) - (Vnonblock (Vvari stk (Vvar addr)) (Vvar d_in)) - (Vnonblock (Vvar d_out) (Vvari stk (Vvar addr)))). + (Vcond (Vvar (ram_en ram)) + (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))))) + Vskip). 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 match m.(HTL.mod_ram) with - | Some (mk_ram ram addr wr_en d_in d_out) => + | 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) m.(HTL.mod_stk) addr d_in d_out wr_en + :: 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) -- cgit