aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/hls/HTL.v1
-rw-r--r--src/hls/HTLPargen.v1
-rw-r--r--src/hls/HTLgen.v1
-rw-r--r--src/hls/HTLgenspec.v2
4 files changed, 4 insertions, 1 deletions
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) ->