diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
| commit | 359194617de51adcc451b45b6c1b0a9332820906 (patch) | |
| tree | 7b1fce73244ebbb1195c37dd986de0bf1d081a0c /src/hls/IfConversion.v | |
| parent | a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 (diff) | |
| download | vericert-359194617de51adcc451b45b6c1b0a9332820906.tar.gz vericert-359194617de51adcc451b45b6c1b0a9332820906.zip | |
Add new instructions for pipelines
Diffstat (limited to 'src/hls/IfConversion.v')
| -rw-r--r-- | src/hls/IfConversion.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 39d9fd2..e893578 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -113,7 +113,7 @@ Definition transf_function (f: function) : function := let (_, c) := List.fold_left if_convert_code (find_blocks_with_cond f.(fn_code)) (1%nat, f.(fn_code)) in - mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint). + mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_funct_units) f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. |