diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 18:21:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 18:21:00 +0100 |
| commit | 92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2 (patch) | |
| tree | 7e8d76015cb35828e371817dfdf1defc46fcfe89 /src/hls/ClockMemory.v | |
| parent | afcb12b5e443da586459455dbc637fc04b9d0634 (diff) | |
| download | vericert-92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2.tar.gz vericert-92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2.zip | |
Finished most of the giblesubpar proof
Diffstat (limited to 'src/hls/ClockMemory.v')
| -rw-r--r-- | src/hls/ClockMemory.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/ClockMemory.v b/src/hls/ClockMemory.v index 3d068ad..549b310 100644 --- a/src/hls/ClockMemory.v +++ b/src/hls/ClockMemory.v @@ -44,9 +44,9 @@ Definition pred := positive. Definition transf_maps (d: stmnt) := match d with - | Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2) => + | Vseq (Vseq Vskip (Vblock (Vvari r e1) e2)) ((Vblock (Vvar _) _) as rest) => Vseq rest (Vnonblock (Vvari r e1) e2) - | Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2)) => + | Vseq (Vseq Vskip (Vblock (Vvar e1) (Vvari r e2))) (Vblock (Vvar st') e3) => Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vvari r e2)) | _ => d end. |