diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-15 21:01:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-15 21:01:59 +0000 |
| commit | 894789af7aa5b3f748b3d3be40fe8a4f227b693f (patch) | |
| tree | 81a4d74250a9ad3d99e664be6d43e6c0a8936703 | |
| parent | c7cc9a3eb82e36c23caf494e144a3391a31e6260 (diff) | |
| download | vericert-894789af7aa5b3f748b3d3be40fe8a4f227b693f.tar.gz vericert-894789af7aa5b3f748b3d3be40fe8a4f227b693f.zip | |
Fix max funtion in RTLParFU
| -rw-r--r-- | src/hls/RTLParFU.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v index b18aef6..f0ceafd 100644 --- a/src/hls/RTLParFU.v +++ b/src/hls/RTLParFU.v @@ -379,7 +379,8 @@ Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := Definition max_reg_function (f: function) := Pos.max (PTree.fold max_reg_bblock f.(fn_code) 1%positive) - (fold_left Pos.max f.(fn_params) 1%positive). + (Pos.max (fold_left Pos.max f.(fn_params) 1%positive) + (max_reg_resources f.(fn_funct_units))). Definition max_pc_function (f: function) : positive := PTree.fold (fun m pc i => (Pos.max m |