diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:39:04 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:39:04 +0100 |
commit | 77c5c01146fa9e2fa09779c1da642b8f5469dff5 (patch) | |
tree | 30d98d7302451a0423635ec807f7c97026d48382 /src | |
parent | 1c8e0373d735ac88740f96c5da1d929ce3f7b688 (diff) | |
download | vericert-77c5c01146fa9e2fa09779c1da642b8f5469dff5.tar.gz vericert-77c5c01146fa9e2fa09779c1da642b8f5469dff5.zip |
Make externctrl application its own HTL pass
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 5 | ||||
-rw-r--r-- | src/hls/ApplyExternctrl.v | 180 | ||||
-rw-r--r-- | src/hls/HTL.v | 31 | ||||
-rw-r--r-- | src/hls/Veriloggen.v | 198 |
4 files changed, 229 insertions, 185 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 38a9d0e..ea3720a 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -61,6 +61,7 @@ Require Import compcert.lib.Coqlib. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. Require vericert.hls.Veriloggenproof. +Require vericert.hls.ApplyExternctrl. Require vericert.hls.Renaming. Require vericert.hls.HTLgen. Require vericert.hls.RTLBlock. @@ -194,6 +195,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_HTL 1) @@@ Renaming.transf_program @@ print (print_HTL 2) + @@@ ApplyExternctrl.transf_program + @@ print (print_HTL 3) @@@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@ -297,7 +300,7 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T. + unfold transf_backend, time in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. set (p8 := Renumber.transf_program p7) in *. set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *. diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v new file mode 100644 index 0000000..44c6b83 --- /dev/null +++ b/src/hls/ApplyExternctrl.v @@ -0,0 +1,180 @@ +Require Import compcert.common.Errors. +Require Import compcert.common.AST. + +Require Import vericert.common.Maps. +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.Verilog. + +Import ListNotations. + +Section APPLY_EXTERNCTRL. + Local Open Scope assocmap. + Local Open Scope error_monad_scope. + + Variable prog : HTL.program. + Variable m : HTL.module. + + Let modmap := prog_modmap prog. + + Definition get_mod_signal (othermod : HTL.module) (signal : HTL.controlsignal) := + match signal with + | ctrl_finish => OK (HTL.mod_finish othermod) + | ctrl_return => OK (HTL.mod_return othermod) + | ctrl_start => OK (HTL.mod_start othermod) + | ctrl_reset => OK (HTL.mod_reset othermod) + | ctrl_clk => OK (HTL.mod_clk othermod) + | ctrl_param idx => + match List.nth_error (HTL.mod_params othermod) idx with + | Some r => OK r + | None => Error (msg "Module does not have nth parameter") + end + end. + + Definition reg_apply_externctrl (r : Verilog.reg) : res reg := + match (HTL.mod_externctrl m) ! r with + | None => OK r + | Some (m, signal) => + match modmap ! m with + | None => Error (msg "Veriloggen: Could not find definition for called module") + | Some othermod => get_mod_signal othermod signal + end + end. + + Fixpoint expr_apply_externctrl (expr : Verilog.expr) {struct expr} : res Verilog.expr := + match expr with + | Vlit n => + OK (Vlit n) + | Vvar r => + do r' <- reg_apply_externctrl r; + OK (Vvar r') + | Vvari r e => + do r' <- reg_apply_externctrl r; + do e' <- expr_apply_externctrl e; + OK (Vvari r e) + | Vrange r e1 e2 => + do r' <- reg_apply_externctrl r; + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vrange r' e1' e2') + | Vinputvar r => + do r' <- reg_apply_externctrl r; + OK (Vinputvar r') + | Vbinop op e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vbinop op e1' e2') + | Vunop op e => + do e' <- expr_apply_externctrl e; + OK (Vunop op e') + | Vternary e1 e2 e3 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + do e3' <- expr_apply_externctrl e3; + OK (Vternary e1' e2' e3') + end. + + Definition mmap_option {A B} (f : A -> res B) (opt : option A) : res (option B) := + match opt with + | None => OK None + | Some a => do a' <- f a; OK (Some a') + end. + + Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) := + fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) := + match cs with + | nil => OK nil + | (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') + end. + + Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt := + match stmnt with + | Vskip => OK Vskip + | Vseq s1 s2 => + do s1' <- stmnt_apply_externctrl s1; + do s2' <- stmnt_apply_externctrl s2; + OK (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- expr_apply_externctrl e; + do s1' <- stmnt_apply_externctrl s1; + do s2' <- stmnt_apply_externctrl s2; + OK (Vcond e' s1' s2') + | Vcase e cases def => + do e' <- expr_apply_externctrl e; + do cases' <- cases_apply_externctrl_ stmnt_apply_externctrl cases; + do def' <- mmap_option (fun x => stmnt_apply_externctrl x) def; + OK (Vcase e' cases' def') + | Vblock e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vnonblock e1' e2') + end. + + (* Unused. Defined for completeness *) + Definition cases_apply_externctrl := cases_apply_externctrl_ stmnt_apply_externctrl. + + Fixpoint xassocmap_apply_externctrl {A} (regmap : list (reg * A)) : res (list (reg * A)) := + match regmap with + | nil => OK nil + | (r, v) :: l => + do r' <- reg_apply_externctrl r; + do l' <- xassocmap_apply_externctrl l; + OK ((r', v) :: l') + end. + + Definition assocmap_apply_externctrl {A} (regmap : AssocMap.t A) : res (AssocMap.t A) := + do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); + 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' <- reg_apply_externctrl (HTL.mod_clk m); + 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 with + | left LEDATA, left LECTRL => + 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.") + end. +End APPLY_EXTERNCTRL. + +Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog). +Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 1eb86e1..8d51750 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -105,6 +105,26 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := Definition empty_stack (m : module) : Verilog.assocmap_arr := (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + +Definition prog_modmap (p : HTL.program) := + PTree_Properties.of_list (Option.map_option + (fun a => match a with + | (ident, (AST.Gfun (AST.Internal f))) => Some (ident, f) + | _ => None + end) + (AST.prog_defs p)). + +Lemma max_pc_wf : + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -247,14 +267,3 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). - -Lemma max_pc_wf : - forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - @map_well_formed T m. -Proof. - unfold map_well_formed. intros. - exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. - apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. - unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. - simplify. transitivity (Z.pos (max_pc_map m)); eauto. -Qed. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 1438e95..1f0938b 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -29,152 +29,17 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. Import ListNotations. -Section APPLY_MAPPING. - Local Open Scope assocmap. - Local Open Scope error_monad_scope. - - Variable externctrl : AssocMap.t (ident * controlsignal). - Variable modmap : PTree.t HTL.module. - - Definition get_mod_signal (m : HTL.module) (signal : HTL.controlsignal) := - match signal with - | ctrl_finish => OK (HTL.mod_finish m) - | ctrl_return => OK (HTL.mod_return m) - | ctrl_start => OK (HTL.mod_start m) - | ctrl_reset => OK (HTL.mod_reset m) - | ctrl_clk => OK (HTL.mod_clk m) - | ctrl_param idx => - match List.nth_error (HTL.mod_params m) idx with - | Some r => OK r - | None => Error (msg "Module does not have nth parameter") - end - end. - - Definition reg_apply_map (r : Verilog.reg) : res reg := - match externctrl ! r with - | None => OK r - | Some (m, signal) => - match modmap ! m with - | None => Error (msg "Veriloggen: Could not find definition for called module") - | Some othermod => get_mod_signal othermod signal - end - end. - - Fixpoint expr_apply_map (expr : Verilog.expr) {struct expr} : res Verilog.expr := - match expr with - | Vlit n => - OK (Vlit n) - | Vvar r => - do r' <- reg_apply_map r; - OK (Vvar r') - | Vvari r e => - do r' <- reg_apply_map r; - do e' <- expr_apply_map e; - OK (Vvari r e) - | Vrange r e1 e2 => - do r' <- reg_apply_map r; - do e1' <- expr_apply_map e1; - do e2' <- expr_apply_map e2; - OK (Vrange r' e1' e2') - | Vinputvar r => - do r' <- reg_apply_map r; - OK (Vinputvar r') - | Vbinop op e1 e2 => - do e1' <- expr_apply_map e1; - do e2' <- expr_apply_map e2; - OK (Vbinop op e1' e2') - | Vunop op e => - do e' <- expr_apply_map e; - OK (Vunop op e') - | Vternary e1 e2 e3 => - do e1' <- expr_apply_map e1; - do e2' <- expr_apply_map e2; - do e3' <- expr_apply_map e3; - OK (Vternary e1' e2' e3') - end. - - Definition mmap_option {A B} (f : A -> res B) (opt : option A) : res (option B) := - match opt with - | None => OK None - | Some a => do a' <- f a; OK (Some a') - end. - - Definition cases_apply_map_ (stmnt_apply_map_ : Verilog.stmnt -> res Verilog.stmnt) := - fix cases_apply_map (cs : list (Verilog.expr * Verilog.stmnt)) := - match cs with - | nil => OK nil - | (c_e, c_s) :: tl => - do c_e' <- expr_apply_map c_e; - do c_s' <- stmnt_apply_map_ c_s; - do tl' <- cases_apply_map tl; - OK ((c_e', c_s') :: tl') - end. - - Fixpoint stmnt_apply_map (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt := - match stmnt with - | Vskip => OK Vskip - | Vseq s1 s2 => - do s1' <- stmnt_apply_map s1; - do s2' <- stmnt_apply_map s2; - OK (Vseq s1' s2') - | Vcond e s1 s2 => - do e' <- expr_apply_map e; - do s1' <- stmnt_apply_map s1; - do s2' <- stmnt_apply_map s2; - OK (Vcond e' s1' s2') - | Vcase e cases def => - do e' <- expr_apply_map e; - do cases' <- cases_apply_map_ stmnt_apply_map cases; - do def' <- mmap_option (fun x => stmnt_apply_map x) def; - OK (Vcase e' cases' def') - | Vblock e1 e2 => - do e1' <- expr_apply_map e1; - do e2' <- expr_apply_map e2; - OK (Vblock e1' e2') - | Vnonblock e1 e2 => - do e1' <- expr_apply_map e1; - do e2' <- expr_apply_map e2; - OK (Vnonblock e1' e2') - end. - - (* Unused. Defined for completeness *) - Definition cases_apply_map := cases_apply_map_ stmnt_apply_map. -End APPLY_MAPPING. - Section TRANSLATE. Local Open Scope error_monad_scope. - Definition transl_datapath_fun externctrl modmap (a : Verilog.node * HTL.datapath_stmnt) := - let (n, s) := a in - let node := Verilog.Vlit (posToValue n) in - do stmnt <- stmnt_apply_map externctrl modmap s; - OK (node, stmnt). + Definition transl_states : list (HTL.node * HTL.datapath_stmnt) -> list (Verilog.expr * Verilog.stmnt) := + map (fun '(n, s) => (Verilog.Vlit (posToValue n), s)). - Definition transl_datapath externctrl modmap st := Errors.mmap (transl_datapath_fun externctrl modmap) st. + Definition scl_to_Vdecls := + map (fun '(r, (io, Verilog.VScalar sz)) => Vdeclaration (Vdecl io r sz)). - Definition transl_ctrl_fun externctrl modmap (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):= - let (n, s) := a in - let node := Verilog.Vlit (posToValue n) in - do stmnt <- stmnt_apply_map externctrl modmap s; - OK (node, stmnt). - - Definition transl_ctrl externctrl modmap st := Errors.mmap (transl_ctrl_fun externctrl modmap) st. - - Definition scl_to_Vdecl_fun externctrl modmap (a : reg * (option Verilog.io * Verilog.scl_decl)) := - match a with (r, (io, Verilog.VScalar sz)) => - do r' <- reg_apply_map externctrl modmap r; - OK (Verilog.Vdecl io r' sz) - end. - - Definition scl_to_Vdecl externctrl modmap scldecl := mmap (scl_to_Vdecl_fun externctrl modmap) scldecl. - - Definition arr_to_Vdeclarr_fun externctrl modmap (a : reg * (option Verilog.io * Verilog.arr_decl)) := - match a with (r, (io, Verilog.VArray sz l)) => - do r' <- reg_apply_map externctrl modmap r; - OK (Verilog.Vdeclarr io r' sz l) - end. - - Definition arr_to_Vdeclarr externctrl modmap arrdecl := mmap (arr_to_Vdeclarr_fun externctrl modmap) arrdecl. + Definition arr_to_Vdeclarrs := + map (fun '(r, (io, Verilog.VArray sz l)) => Vdeclaration (Vdeclarr io r sz l)). Definition called_functions (main_name : ident) (m : HTL.module) : list ident := (* remove duplicates *) @@ -185,14 +50,6 @@ Section TRANSLATE. (List.filter (fun it => negb (Pos.eqb (fst (snd it)) main_name)) (PTree.elements (HTL.mod_externctrl m)))). - Definition prog_modmap (p : HTL.program) := - PTree_Properties.of_list (Option.map_option - (fun a => match a with - | (ident, (Gfun (Internal f))) => Some (ident, f) - | _ => None - end) - p.(prog_defs)). - (** Clean up declarations for an inlined module. Make IO decls into reg, and remove the clk declaration *) Definition clean_up_decl (clk : reg) (it : Verilog.module_item) := match it with @@ -225,50 +82,45 @@ Section TRANSLATE. translated_modules in - do case_el_ctrl <- transl_ctrl (HTL.mod_externctrl m) modmap (PTree.elements (HTL.mod_controllogic m)); - do case_el_data <- transl_datapath (HTL.mod_externctrl m) modmap (PTree.elements (HTL.mod_datapath m)); + let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in + let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in let externctrl := HTL.mod_externctrl m in - do rst <- reg_apply_map externctrl modmap (HTL.mod_reset m); - do st <- reg_apply_map externctrl modmap (HTL.mod_st m); - do finish <- reg_apply_map externctrl modmap (HTL.mod_finish m); - do params <- mmap (reg_apply_map externctrl modmap) (HTL.mod_params m); (* Only declare the clock if this is the top-level module, i.e. there is no inherited clock *) - do maybe_clk_decl <- match externclk with - | None => - do decl <- scl_to_Vdecl_fun externctrl modmap (clk, (Some Vinput, VScalar 1)); - OK [Vdeclaration decl] - | Some _ => OK [] - end; + let maybe_clk_decl := match externclk with + | None => scl_to_Vdecls [(clk, (Some Vinput, VScalar 1))] + | Some _ => [] + end in let local_arrdecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_arrdecls m) in - do arr_decls <- arr_to_Vdeclarr externctrl modmap (AssocMap.elements local_arrdecls); + let arr_decls := arr_to_Vdeclarrs (AssocMap.elements local_arrdecls) in let local_scldecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_scldecls m) in - do scl_decls <- scl_to_Vdecl externctrl modmap (AssocMap.elements local_scldecls); + let scl_decls := scl_to_Vdecls (AssocMap.elements local_scldecls) in let body : list Verilog.module_item:= - Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar rst) (Vlit (ZToValue 1))) + Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) (Vseq - (Vnonblock (Vvar st) (Vlit (posToValue (HTL.mod_entrypoint m)))) - (Vnonblock (Vvar finish) (Vlit (ZToValue 0)))) - (Vcase (Vvar st) case_el_ctrl (Some Vskip))) + (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m)))) + (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0)))) + (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip))) :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip)) - :: List.map Vdeclaration (arr_decls ++ scl_decls) + :: arr_decls + ++ scl_decls ++ maybe_clk_decl ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) in OK (Verilog.mkmodule (HTL.mod_start m) - rst - clk - finish + (HTL.mod_reset m) + (HTL.mod_clk m) + (HTL.mod_finish m) (HTL.mod_return m) - st + (HTL.mod_st m) (HTL.mod_stk m) (HTL.mod_stk_len m) - params + (HTL.mod_params m) body (HTL.mod_entrypoint m)) end. |