diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-01 14:06:51 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-01 14:06:51 +0100 |
| commit | e4a173f4ebd46b5e3f45ee4f65a93790d68544ab (patch) | |
| tree | 10494f0357c404604eb8756f6deb0f15d53d576a /src/hls/Renaming.v | |
| parent | adabec157b807bf6695bdcef64233c76f43c37bb (diff) | |
| download | vericert-e4a173f4ebd46b5e3f45ee4f65a93790d68544ab.tar.gz vericert-e4a173f4ebd46b5e3f45ee4f65a93790d68544ab.zip | |
Use sumbool instead of option for decide_ram_wf
Diffstat (limited to 'src/hls/Renaming.v')
| -rw-r--r-- | src/hls/Renaming.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index b088926..91a6673 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -166,8 +166,8 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned, decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk', max_list_dec mod_params' mod_st', - option_ram_wf mod_clk' (HTL.mod_ram m) with - | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some WFRAM => + decide_ram_wf mod_clk' (HTL.mod_ram m) with + | left LEDATA, left LECTRL, left MORD, left WFPARAMS, left WFRAM => ret (HTL.mkmodule mod_params' mod_datapath' @@ -193,7 +193,7 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := | _, right _, _, _, _ => error (Errors.msg "Renaming: More than 2^32 controlpath states") | _, _, right _, _, _ => error (Errors.msg "Renaming: Incorrect ordering of control registers") | _, _, _, right _, _ => error (Errors.msg "Renaming: Parameter registers conflict with control registers") - | _, _, _, _, None => error (Errors.msg "Renaming: Ram address register conflicts with control registers") + | _, _, _, _, right _ => error (Errors.msg "Renaming: Ram address register conflicts with control registers") end. Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := |