diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-02 16:57:56 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-02 16:57:56 +0100 |
| commit | 05afcff334725e885522e9859b9ab735a404014c (patch) | |
| tree | 5d92cb894bb05256072d26d0f997ab8220aaf2d1 /src/hls/HTLPargen.v | |
| parent | a4c8b2b92fca07e16570c2522d83e6c361d0a6dc (diff) | |
| download | vericert-05afcff334725e885522e9859b9ab735a404014c.tar.gz vericert-05afcff334725e885522e9859b9ab735a404014c.zip | |
Put every load/store into it's own cycle
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 10c4357..f22cc39 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -409,11 +409,11 @@ Definition transf_instr (fin rtrn stack state preg: reg) Errors.OK (curr_p, Vseq d stmnt) | RBload p mem addr args dst => do src <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) src in + let stmnt := translate_predicate Vnonblock preg (npred p) (Vvar dst) src in Errors.OK (curr_p, Vseq d stmnt) | RBstore p mem addr args src => do dst <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vblock preg (npred p) dst (Vvar src) in + let stmnt := translate_predicate Vnonblock preg (npred p) dst (Vvar src) in Errors.OK (curr_p, Vseq d stmnt) | RBsetpred p' cond args p => do cond' <- translate_condition cond args; |