From 1be25f8fb37d44b22472d2ae7ca73dc38b04b147 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 2 Sep 2021 20:46:03 +0100 Subject: Do not apply externctrl to control registers --- src/hls/ApplyExternctrl.v | 52 ++++++++++++++++------------------------------- 1 file changed, 18 insertions(+), 34 deletions(-) (limited to 'src/hls') diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index 276ba74..e9aceec 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -143,53 +143,37 @@ Section APPLY_EXTERNCTRL. OK (AssocMap_Properties.of_list l). Definition module_apply_externctrl : res HTL.module := - do mod_start' <- reg_apply_externctrl (HTL.mod_start m); - do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m); - do mod_clk' <- global_clk; - do mod_finish' <- reg_apply_externctrl (HTL.mod_finish m); - do mod_return' <- reg_apply_externctrl (HTL.mod_return m); - do mod_st' <- reg_apply_externctrl (HTL.mod_st m); - do mod_stk' <- reg_apply_externctrl (HTL.mod_stk m); - do mod_params' <- mmap reg_apply_externctrl (HTL.mod_params m); do mod_controllogic' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_controllogic m); do mod_datapath' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_datapath m); - - do mod_scldecls' <- assocmap_apply_externctrl (HTL.mod_scldecls m); - do mod_arrdecls' <- assocmap_apply_externctrl (HTL.mod_arrdecls m); do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m); match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, - 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', - decide_ram_wf mod_clk' (HTL.mod_ram m) with - | left LEDATA, left LECTRL, left MORD, left WFPARAMS, left WFRAM => + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned + with + | left LEDATA, left LECTRL => OK (HTL.mkmodule - mod_params' + (HTL.mod_params m) mod_datapath' mod_controllogic' (HTL.mod_entrypoint m) - mod_st' - mod_stk' + (HTL.mod_st m) + (HTL.mod_stk m) (HTL.mod_stk_len m) - mod_finish' - mod_return' - mod_start' - mod_reset' - mod_clk' - mod_scldecls' - mod_arrdecls' + (HTL.mod_finish m) + (HTL.mod_return m) + (HTL.mod_start m) + (HTL.mod_reset m) + (HTL.mod_clk m) + (HTL.mod_scldecls m) + (HTL.mod_arrdecls m) mod_externctrl' (HTL.mod_ram m) (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)) - MORD - WFRAM - WFPARAMS) - | right _, _, _, _, _ => Error (Errors.msg "ApplyExternctrl: More than 2^32 datapath states") - | _, 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") - | _, _, _, _, right _ => Error (Errors.msg "ApplyExternctrl: Ram address register conflicts with control registers") + (HTL.mod_ordering_wf m) + (HTL.mod_ram_wf m) + (HTL.mod_params_wf m)) + | right _, _ => Error (Errors.msg "ApplyExternctrl: More than 2^32 datapath states") + | _, right _ => Error (Errors.msg "ApplyExternctrl: More than 2^32 controlpath states") end. End APPLY_EXTERNCTRL. -- cgit