From 05347ca5126f335b0479b71a4576b141e082fab5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Mar 2021 10:27:33 +0000 Subject: Add RAM to HTL --- src/hls/HTL.v | 1 + src/hls/HTLPargen.v | 1 + src/hls/HTLgen.v | 1 + src/hls/HTLgenspec.v | 2 +- 4 files changed, 4 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c8a0041..1949785 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -67,6 +67,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + mod_ram : option (reg * reg * reg * reg); mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 618c5e6..9bf7ed7 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -821,6 +821,7 @@ Definition transf_module (f: function) : mon HTL.module := clk current_state.(st_scldecls) current_state.(st_arrdecls) + None (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) | _, _ => error (Errors.msg "More than 2^32 states.") end diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index f1e6b2a..c071868 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -612,6 +612,7 @@ Definition transf_module (f: function) : mon HTL.module := clk current_state.(st_scldecls) current_state.(st_arrdecls) + None (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) | _, _ => error (Errors.msg "More than 2^32 states.") end diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 845b1d5..7cb6d8c 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -183,7 +183,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> -- cgit