diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-03 14:09:20 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-03 14:09:20 +0100 |
commit | 25215f862dc8b768e16bfb86bd595947610af9f6 (patch) | |
tree | 34562cefd4524b040d469fe0eadae4d7abd0bdd5 /src | |
parent | 846abc1768531ac62601d2827e9ac53d125c443a (diff) | |
download | vericert-25215f862dc8b768e16bfb86bd595947610af9f6.tar.gz vericert-25215f862dc8b768e16bfb86bd595947610af9f6.zip |
Fix renamer skipping ram_mem
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Renaming.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index e4453d1..609757c 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -133,6 +133,7 @@ Program Definition renumber_ram (mr : option HTL.ram) : mon (option HTL.ram) := match mr with | None => ret None | Some r => + do ram_mem' <- renumber_reg (ram_mem r); do ram_addr' <- renumber_reg (ram_addr r); do ram_en' <- renumber_reg (ram_en r); do ram_d_in' <- renumber_reg (ram_d_in r); @@ -140,7 +141,7 @@ Program Definition renumber_ram (mr : option HTL.ram) : mon (option HTL.ram) := do ram_wr_en' <- renumber_reg (ram_wr_en r); do ram_u_en' <- renumber_reg (ram_u_en r); match decide_ram_ordering ram_addr' ram_en' ram_d_in' ram_d_out' ram_wr_en' ram_u_en' with - | left wf => ret (Some (mk_ram (ram_size r) (ram_mem r) ram_en' ram_u_en' ram_addr' ram_wr_en' ram_d_in' ram_d_out' wf)) + | left wf => ret (Some (mk_ram (ram_size r) ram_mem' ram_en' ram_u_en' ram_addr' ram_wr_en' ram_d_in' ram_d_out' wf)) | right _ => error (Errors.msg "Renaming: Incorrect ordering of RAM registers") end end. |