diff options
Diffstat (limited to 'src/hls/ApplyExternctrl.v')
-rw-r--r-- | src/hls/ApplyExternctrl.v | 59 |
1 files changed, 36 insertions, 23 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index b024b9e..edd413c 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -89,14 +89,14 @@ Section APPLY_EXTERNCTRL. end. Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) := - fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) := + fix cases_apply_externctrl (cs : stmnt_expr_list) := match cs with - | nil => OK nil - | (c_e, c_s) :: tl => + | Stmntnil => OK Stmntnil + | Stmntcons c_e c_s tl => do c_e' <- expr_apply_externctrl c_e; do c_s' <- stmnt_apply_externctrl_ c_s; do tl' <- cases_apply_externctrl tl; - OK ((c_e', c_s') :: tl') + OK (Stmntcons c_e' c_s' tl') end. Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt := @@ -142,6 +142,12 @@ Section APPLY_EXTERNCTRL. do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); OK (AssocMap_Properties.of_list l). + + Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) : + option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). + destruct mr. + - intros. + 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); @@ -159,26 +165,33 @@ Section APPLY_EXTERNCTRL. 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 with - | left LEDATA, left LECTRL => + 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 => OK (HTL.mkmodule - mod_params' - mod_datapath' - mod_controllogic' - (HTL.mod_entrypoint m) - mod_st' - mod_stk' - (HTL.mod_stk_len m) - mod_finish' - mod_return' - mod_start' - mod_reset' - mod_clk' - mod_scldecls' - mod_arrdecls' - mod_externctrl' - (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) - | _, _ => Error (Errors.msg "More than 2^32 states.") + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + mod_stk' + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + mod_scldecls' + mod_arrdecls' + mod_externctrl' + (HTL.mod_ram m) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)) + MORD + (HTL.mod_ram_wf m) + WFPARAMS) + | _, _, _, _ => Error (Errors.msg "ApplyExternctrl") end. End APPLY_EXTERNCTRL. |