aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-11-15 21:01:15 +0000
committerYann Herklotz <git@yannherklotz.com>2021-11-15 21:01:15 +0000
commit39200b933b230579b90089539216077f016bacc5 (patch)
tree1fc425ca2c22489a4bdd0abd144c218784064b7b
parent1b0d7b8da1ab71af0577c516b2618aeb94abbc34 (diff)
downloadvericert-kvx-39200b933b230579b90089539216077f016bacc5.tar.gz
vericert-kvx-39200b933b230579b90089539216077f016bacc5.zip
Add helper functions to FunctionalUnits
-rw-r--r--src/hls/FunctionalUnits.v25
1 files changed, 22 insertions, 3 deletions
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v
index 4a9bf5b..9504bb1 100644
--- a/src/hls/FunctionalUnits.v
+++ b/src/hls/FunctionalUnits.v
@@ -135,10 +135,10 @@ Definition get_sdiv n res :=
end.
Definition set_res fu res :=
- let max := fold_left Pos.max ((arch_sdiv (res_arch res))
+ let max := ((fold_left Pos.max ((arch_sdiv (res_arch res))
++ (arch_div (res_arch res))
- ++ (arch_ram (res_arch res))) 1 in
- let nt := PTree.set (max + 1)%positive fu (res_funct_units res) in
+ ++ (arch_ram (res_arch res))) 1) + 1)%positive in
+ let nt := PTree.set max fu (res_funct_units res) in
match fu with
| UnsignedDiv _ => mk_resources nt (mk_arch (max :: arch_div (res_arch res))
(arch_sdiv (res_arch res))
@@ -164,3 +164,22 @@ Definition funct_unit_stages (f: funct_unit) : positive :=
| UnsignedDiv d => div_stages d
| _ => 1
end.
+
+Definition max_reg_ram r :=
+ fold_right Pos.max 1 (ram_mem r::ram_en r::ram_u_en r::ram_addr r
+ ::ram_wr_en r::ram_d_in r::ram_d_out r::nil).
+
+Definition max_reg_divider {b: bool} (d: divider b) :=
+ fold_right Pos.max 1 (div_numer d::div_denom d::div_quot d::div_rem d::nil).
+
+Definition max_reg_fu fu :=
+ match fu with
+ | SignedDiv d | UnsignedDiv d => max_reg_divider d
+ | Ram r => max_reg_ram r
+ end.
+
+Definition max_reg_funct_units r :=
+ PTree.fold (fun m _ a => Pos.max m (max_reg_fu a)) r 1.
+
+Definition max_reg_resources r :=
+ max_reg_funct_units r.(res_funct_units).