diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-03-01 11:17:09 +0000 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-03-01 11:17:09 +0000 |
| commit | 52c41786bb4673ebea32a870e7a3ad948cfe574d (patch) | |
| tree | 30fbcad1f5ab0f792746f59d76680c550303758e /src/hls/HTLgen.v | |
| parent | dc518898cac3b8e06684b6e66377d430ab30a52e (diff) | |
| download | vericert-52c41786bb4673ebea32a870e7a3ad948cfe574d.tar.gz vericert-52c41786bb4673ebea32a870e7a3ad948cfe574d.zip | |
Add idle state after return
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 9373a33..052aaad 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -563,12 +563,13 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => - match r with - | Some r' => - add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))) - | None => - add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))) - end + do idle_state <- create_state; + let retval := match r with + | Some r' => Vvar r' + | None => Vlit (ZToValue 0%Z) + end in + do _ <- add_instr n idle_state (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval))); + add_instr_skip idle_state (data_vstmnt (nonblock fin (Vlit (ZToValue 0%Z)))) end end. |