diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-07-31 11:36:57 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-31 11:36:57 +0100 |
| commit | 13cd1c16d36402318150615475de85ac3b2cff52 (patch) | |
| tree | f5b4c8c3ac2854e28666eeb4ef653344af5efa31 /src/hls/RTLParFU.v | |
| parent | 502e49e2f8c95b40cd0761cbb69c863904169f8b (diff) | |
| download | vericert-13cd1c16d36402318150615475de85ac3b2cff52.tar.gz vericert-13cd1c16d36402318150615475de85ac3b2cff52.zip | |
Remove RTLParFu and fix DMemorygen.v
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. *) |