diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-11 00:57:55 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-11 00:57:55 +0100 |
| commit | 9b05e2cf60d8c8754a3742262a95be8bdd8911e9 (patch) | |
| tree | 3206bb244a324dc873b33f03cb13e28af3a5a731 /src/hls/HTLgen.v | |
| parent | 5e10b594320127a8ffa063e7ccba78a4a9f2b1a5 (diff) | |
| download | vericert-9b05e2cf60d8c8754a3742262a95be8bdd8911e9.tar.gz vericert-9b05e2cf60d8c8754a3742262a95be8bdd8911e9.zip | |
Guard join state with called module finish
Needed to match RTL semantics, since the join state executes once before
the call is initiated, and we need the destination register to not be
affected until after the call has returned.
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 39146ff..908c627 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -490,8 +490,9 @@ Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt := let assign_params := nonblock_all params in Vseq reset_mod assign_params. -Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := - let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in +Definition join (fn_fin fn_rst fn_rtrn fn_dst : reg) : datapath_stmnt := + let set_result := Vcond (boplitz Veq fn_fin 1) + (Vnonblock (Vvar fn_dst) (Vvar fn_rtrn)) Vskip in let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in Vseq stop_reset set_result. @@ -558,7 +559,7 @@ Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instru do return_reg <- map_externctrl fn ctrl_return; let fork_instr := fork reset_reg params in - let join_instr := join return_reg reset_reg dst in + let join_instr := join finish_reg reset_reg return_reg dst in do _ <- add_instr n join_state fork_instr; add_instr_wait finish_reg join_state n' join_instr |