diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-16 15:17:24 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-16 15:18:48 +0100 |
| commit | 29ef1d2d374dcca6ea719c63339f18900be2532f (patch) | |
| tree | 5a9225eddeeefae523f8eead3f26513f42bb28af /src/hls/HTLgenspec.v | |
| parent | 2429e158ecdb4ab8150fa26af776e806d7fd019c (diff) | |
| download | vericert-29ef1d2d374dcca6ea719c63339f18900be2532f.tar.gz vericert-29ef1d2d374dcca6ea719c63339f18900be2532f.zip | |
Most of Ireturn proof
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 1c2d090..d02aff6 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -107,7 +107,7 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c c!pc = Some (RTL.Ireturn r) -> (exists pc2, - stmnts!pc = Some (return_val fin rtrn r) /\ + stmnts!pc = Some (do_return fin rtrn r) /\ trans!pc = Some (state_goto st pc2) /\ stmnts!pc2 = Some (idle fin) /\ trans!pc2 = Some Vskip) -> |