From e4a173f4ebd46b5e3f45ee4f65a93790d68544ab Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 1 Sep 2021 14:06:51 +0100 Subject: Use sumbool instead of option for decide_ram_wf --- src/hls/ApplyExternctrl.v | 6 +++--- src/hls/HTL.v | 12 ++++++------ src/hls/Renaming.v | 6 +++--- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index 8b24336..276ba74 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -162,8 +162,8 @@ Section APPLY_EXTERNCTRL. 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 => OK (HTL.mkmodule mod_params' mod_datapath' @@ -189,7 +189,7 @@ Section APPLY_EXTERNCTRL. | _, right _, _, _, _ => Error (Errors.msg "ApplyExternctrl: More than 2^32 controlpath states") | _, _, right _, _, _ => Error (Errors.msg "ApplyExternctrl: Incorrect ordering of control registers") | _, _, _, right _, _ => Error (Errors.msg "ApplyExternctrl: Parameter registers conflict with control registers") - | _, _, _, _, None => Error (Errors.msg "ApplyExternctrl: Ram address register conflicts with control registers") + | _, _, _, _, right _ => Error (Errors.msg "ApplyExternctrl: Ram address register conflicts with control registers") end. End APPLY_EXTERNCTRL. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 3116af3..303dc70 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -448,16 +448,16 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True} end; unfold module_ordering; auto. Defined. -Definition option_ram_wf (clk : reg) (mr : option HTL.ram) : - option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). +Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) : + {forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive} + {True}. refine ( match mr with | Some r => match (plt clk (ram_addr r)) with - | left LE => Some _ - | _ => None + | left LE => left _ + | _ => right I end - | None => None + | None => left _ end). - crush. + all: crush. Defined. 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 := -- cgit