diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 13:05:20 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 13:56:56 +0100 |
commit | 4139d0f8772d20d2836be2ab34a18b5ce580590b (patch) | |
tree | 7383dc4009a91506c6431d1d9c5c72273c7d02c8 | |
parent | ea48228b89194d7904133983f44807289a93f040 (diff) | |
download | vericert-kvx-4139d0f8772d20d2836be2ab34a18b5ce580590b.tar.gz vericert-kvx-4139d0f8772d20d2836be2ab34a18b5ce580590b.zip |
Get Renaming compiling with RAM inference
-rw-r--r-- | src/hls/ApplyExternctrl.v | 14 | ||||
-rw-r--r-- | src/hls/HTL.v | 14 | ||||
-rw-r--r-- | src/hls/Renaming.v | 33 |
3 files changed, 37 insertions, 24 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index ef056cf..bd48adb 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -142,20 +142,6 @@ Section APPLY_EXTERNCTRL. do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); OK (AssocMap_Properties.of_list l). - Definition option_ram_wf (clk : reg) (mr : option HTL.ram) : - option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). - refine ( - match mr with - | Some r => - match (plt clk (ram_addr r)) with - | left LE => Some _ - | _ => None - end - | None => None - end). - crush. - Defined. - 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); diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c22497f..3116af3 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -447,3 +447,17 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True} | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H 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). + refine ( + match mr with + | Some r => + match (plt clk (ram_addr r)) with + | left LE => Some _ + | _ => None + end + | None => None + end). + crush. +Defined. diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index 6c816c2..9062e13 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -88,6 +88,17 @@ Fixpoint renumber_expr (expr : Verilog.expr) := ret (Vrange r e1' e2') end. + Definition renumber_cases_ (renumber_stmnt_ : Verilog.stmnt -> mon Verilog.stmnt) := + fix renumber_cases (cs : stmnt_expr_list) := + match cs with + | Stmntnil => ret Stmntnil + | Stmntcons c_e c_s tl => + do c_e' <- renumber_expr c_e; + do c_s' <- renumber_stmnt_ c_s; + do tl' <- renumber_cases tl; + ret (Stmntcons c_e' c_s' tl') + end. + Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := match stmnt with | Vskip => ret Vskip @@ -102,12 +113,7 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := ret (Vcond e' s1' s2') | Vcase e cs def => do e' <- renumber_expr e; - do cs_list' <- sequence (map - (fun '(c_expr, c_stmnt) => - do expr' <- renumber_expr c_expr; - do stmnt' <- renumber_stmnt c_stmnt; - ret (expr', stmnt')) (stmnt_to_list cs)); - let cs' := list_to_stmnt cs_list' in + do cs' <- renumber_cases_ renumber_stmnt cs; do def' <- match def with | None => ret None | Some d => do def' <- renumber_stmnt d; ret (Some def') @@ -155,8 +161,11 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := do _ <- clear_regmap; 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', + option_ram_wf mod_clk' (HTL.mod_ram m) with + | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some WFRAM => ret (HTL.mkmodule mod_params' mod_datapath' @@ -173,8 +182,12 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := mod_scldecls' mod_arrdecls' mod_externctrl' - (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) - | _, _ => error (Errors.msg "More than 2^32 states.") + (HTL.mod_ram m) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)) + MORD + WFRAM + WFPARAMS) + | _, _, _, _, _ => error (Errors.msg "More than 2^32 states.") end. Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := |