diff options
Diffstat (limited to 'src/hls/RTLParFU.v')
-rw-r--r-- | src/hls/RTLParFU.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v index b28c0ee..f97ed95 100644 --- a/src/hls/RTLParFU.v +++ b/src/hls/RTLParFU.v @@ -378,14 +378,14 @@ Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in max_reg_cfi max_body bb.(bb_exit). -Definition max_reg_function (f: function) := - Pos.max - (PTree.fold max_reg_bblock f.(fn_code) 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 - (pc + match Zlength i.(bb_body) - with Z.pos p => p | _ => 1 end))%positive) - f.(fn_code) 1%positive. +(* Definition max_reg_function (f: function) := *) +(* Pos.max *) +(* (PTree.fold max_reg_bblock f.(fn_code) 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 *) +(* (pc + match Zlength i.(bb_body) *) +(* with Z.pos p => p | _ => 1 end))%positive) *) +(* f.(fn_code) 1%positive. *) |