diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-17 12:11:12 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-17 12:11:12 +0000 |
| commit | fea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57 (patch) | |
| tree | f8ac2fb75b23716adf369f7cfa8220aa10b11754 /src/hls/RTLParFUgen.v | |
| parent | 508d59dfb16f97cf5f1b9a994bd5a8159c9e1a3e (diff) | |
| download | vericert-fea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57.tar.gz vericert-fea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57.zip | |
Fix generation of RTLParFU
Diffstat (limited to 'src/hls/RTLParFUgen.v')
| -rw-r--r-- | src/hls/RTLParFUgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 55fe4e7..65ddf74 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -57,7 +57,7 @@ Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.ins :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r) :: FUop po (Op.Olea addr) args (ram_addr r) :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) - :: instr_list, update (cycle+1) + :: instr_list, update (Pos.pred cycle) (add_instr (FUop po Op.Omove (ram_d_out r::nil) d)) d_tree) | _ => Errors.Error (Errors.msg "Could not find RAM") |