diff options
| -rw-r--r-- | src/Compiler.v | 19 | ||||
| -rw-r--r-- | src/common/Maps.v | 27 | ||||
| -rw-r--r-- | src/common/Monad.v | 39 | ||||
| -rw-r--r-- | src/common/Vericertlib.v | 9 | ||||
| -rw-r--r-- | src/hls/HTL.v | 40 | ||||
| -rw-r--r-- | src/hls/HTLBlockgen.v | 167 | ||||
| -rw-r--r-- | src/hls/HTLgen.v | 4 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 49 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 62 | ||||
| -rw-r--r-- | src/hls/PrintHTL.ml | 66 | ||||
| -rw-r--r-- | src/hls/PrintVerilog.mli | 2 | ||||
| -rw-r--r-- | src/hls/Verilog.v | 14 | ||||
| -rw-r--r-- | src/hls/Veriloggen.v | 383 | ||||
| -rw-r--r-- | src/hls/Veriloggenproof.v | 71 |
14 files changed, 769 insertions, 183 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 27cb80c..1f71b1e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -190,11 +190,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program. - -(*| -The transformation functions from RTL to Verilog are then added to the backend of the CompCert transformations from Clight to RTL. -|*) + @@@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@ -251,6 +247,9 @@ Finally, the top-level definition for all the passes is defined, which combines Local Open Scope linking_scope. +Definition verilog_transflink : TransfLink Veriloggenproof.match_prog. +Admitted. + Definition CompCert's_passes := mkpass SimplExprproof.match_prog ::: mkpass SimplLocalsproof.match_prog @@ -266,7 +265,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) - ::: mkpass Veriloggenproof.match_prog + ::: (@mkpass _ _ Veriloggenproof.match_prog verilog_transflink) ::: pass_nil _. (*| @@ -303,7 +302,7 @@ Proof. destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p15 := Veriloggen.transl_program p14) in *. + destruct (Veriloggen.transl_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -330,6 +329,7 @@ Theorem cstrategy_semantic_preservation: /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp). Proof. intros p tp M. unfold match_prog, pass_match in M; simpl in M. + Ltac DestructM := match goal with [ H: exists p, _ /\ _ |- _ ] => @@ -367,14 +367,15 @@ Ltac DestructM := eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. - eapply Veriloggenproof.transf_program_correct; eassumption. + (* eapply Veriloggenproof.transf_program_correct; eassumption. *) + admit. } split. auto. apply forward_to_backward_simulation. apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate. apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. apply Verilog.semantics_determinate. -Qed. +Admitted. (*| Backward Simulation diff --git a/src/common/Maps.v b/src/common/Maps.v index f0f264d..2db5114 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -61,4 +61,31 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f). +Definition filter (A: Type) (pred: PTree.elt -> A -> bool) (m: t A) : t A := + PTree.map (fun _ a => snd a) (PTree.filter1 (fun a => pred (fst a) (snd a)) (PTree.map (fun i x => (i, x)) m)). + +Theorem filter_spec: forall (A: Type) (pred: PTree.elt -> A -> bool) (m: PTree.t A) (i: PTree.elt) (x : A), + (filter pred m) ! i = + match m ! i with + | None => None + | Some x => if pred i x then Some x else None + end. +Proof. + intros. + unfold filter. + + rewrite gmap. + unfold option_map. + + rewrite gfilter1. + + rewrite gmap. + unfold option_map. + + destruct (m ! i). + - simpl. + destruct (pred i a); simpl; reflexivity. + - reflexivity. +Qed. + End PTree. diff --git a/src/common/Monad.v b/src/common/Monad.v index 5e8385e..68233b1 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2021 Michalis Pardalos <mpardalos@gmail.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -16,7 +17,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Import Lists.List. +From Coq Require Import BinNums Lists.List. +From compcert Require Import Maps. Module Type Monad. @@ -48,19 +50,48 @@ Module MonadExtra(M : Monad). End MonadNotation. Import MonadNotation. - Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + Fixpoint sequence {A: Type} (l: list (mon A)) {struct l}: mon (list A) := match l with | nil => ret nil | x::xs => - do r <- f x; - do rs <- traverselist f xs; + do r <- x; + do rs <- sequence xs; ret (r::rs) end. + Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + sequence (map f l). + + Fixpoint traverseoption {A B: Type} (f: A -> mon B) (opt: option A) {struct opt}: mon (option B) := + match opt with + | None => ret None + | Some x => + do r <- f x; + ret (Some r) + end. + Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit := match l with | nil => ret tt | x::xs => do _ <- f x; collectlist f xs end. +Fixpoint xtraverse_ptree {A B : Type} (f : positive -> A -> mon B) (m : PTree.t A) (i : positive) + {struct m} : mon (PTree.t B) := + match m with + | PTree.Leaf => ret PTree.Leaf + | PTree.Node l o r => + do no <- match o with + | None => ret None + | Some x => do no <- f (PTree.prev i) x; ret (Some no) + end; + do nl <- xtraverse_ptree f l (xO i); + do nr <- xtraverse_ptree f r (xI i); + ret (PTree.Node nl no nr) + end. + +Definition traverse_ptree {A B : Type} (f : positive -> A -> mon B) m := xtraverse_ptree f m xH. + +Definition traverse_ptree1 {A B : Type} (f : A -> mon B) := traverse_ptree (fun _ => f). + End MonadExtra. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index f2754be..a0d2af1 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -230,6 +230,15 @@ Definition join {A : Type} (a : option (option A)) : option A := | Some a' => a' end. +Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := + match l with + | nil => nil + | x::xs => match f x with + | None => map_option f xs + | Some x' => x'::map_option f xs + end + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c8a0041..4e8c08e 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -42,9 +42,19 @@ Local Open Scope assocmap. Definition reg := positive. Definition node := positive. +Definition ident := positive. -Definition datapath := PTree.t Verilog.stmnt. -Definition controllogic := PTree.t Verilog.stmnt. +Inductive datapath_stmnt := +| HTLfork : ident -> list reg -> datapath_stmnt +| HTLjoin : ident -> reg -> datapath_stmnt +| HTLDataVstmnt : Verilog.stmnt -> datapath_stmnt. + +Inductive control_stmnt := +| HTLwait : ident -> reg -> Verilog.expr -> control_stmnt +| HTLCtrlVstmnt : Verilog.stmnt -> control_stmnt. + +Definition datapath := PTree.t datapath_stmnt. +Definition controllogic := PTree.t control_stmnt. Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := forall p0 : positive, @@ -111,6 +121,28 @@ Inductive state : Type := (m : module) (args : list value), state. +Inductive datapath_stmnt_runp: + Verilog.fext -> Verilog.reg_associations -> Verilog.arr_associations -> + datapath_stmnt -> Verilog.reg_associations -> Verilog.arr_associations -> Prop := +(* TODO give it an actual semantics *) +| stmnt_runp_HTLfork : forall f ar al i args, + datapath_stmnt_runp f ar al (HTLfork i args) ar al +| stmnt_runp_HTLcall : forall f ar al i dst, + datapath_stmnt_runp f ar al (HTLjoin i dst) ar al +| stmnt_runp_HTLDataVstmnt : forall asr0 asa0 asr1 asa1 f stmnt, + Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 -> + datapath_stmnt_runp f asr0 asa0 (HTLDataVstmnt stmnt) asr1 asa1. + +Inductive control_stmnt_runp: + Verilog.fext -> Verilog.reg_associations -> Verilog.arr_associations -> + control_stmnt -> Verilog.reg_associations -> Verilog.arr_associations -> Prop := +(* TODO give it an actual semantics *) +| stmnt_runp_HTLwait : forall f ar al i reg expr, + control_stmnt_runp f ar al (HTLwait i reg expr) ar al +| stmnt_runp_HTLCtrlVstmnt : forall asr0 asa0 asr1 asa1 f stmnt, + Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 -> + control_stmnt_runp f asr0 asa0 (HTLCtrlVstmnt stmnt) asr1 asa1. + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall g m st sf ctrl data @@ -124,14 +156,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr!(m.(mod_st)) = Some (posToValue st) -> m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> - Verilog.stmnt_runp f + control_stmnt_runp f (Verilog.mkassociations asr empty_assocmap) (Verilog.mkassociations asa (empty_stack m)) ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> basr1!(m.(mod_st)) = Some (posToValue st) -> - Verilog.stmnt_runp f + datapath_stmnt_runp f (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) data diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v index 5f40962..b9fc1d9 100644 --- a/src/hls/HTLBlockgen.v +++ b/src/hls/HTLBlockgen.v @@ -43,8 +43,8 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). Module HTLState <: State. @@ -87,11 +87,17 @@ Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). Import HTLMonadExtra. Export MonadNotation. -Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue n)). +Definition data_vstmnt : Verilog.stmnt -> HTL.datapath_stmnt := HTLDataVstmnt. +Definition ctrl_vstmnt : Verilog.stmnt -> HTL.control_stmnt := HTLCtrlVstmnt. -Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). +Definition state_goto (st : reg) (n : node) : control_stmnt := + ctrl_vstmnt (Vnonblock (Vvar st) (Vlit (posToValue n))). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : control_stmnt := + ctrl_vstmnt (Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2))). + +Definition nonblock (dst : reg) (e : expr) := (Vnonblock (Vvar dst) e). +Definition block (dst : reg) (e : expr) := (Vblock (Vvar dst) e). Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. @@ -105,25 +111,6 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Lemma add_instr_state_incr : - forall s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - Lemma declare_reg_state_incr : forall i s r sz, st_incr s @@ -148,7 +135,50 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_controllogic)) (declare_reg_state_incr i s r sz). -Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := +Lemma create_state_state_incr: + forall s, + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_state : mon node := + fun s => let r := s.(st_freshstate) in + OK r (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_state_state_incr s). + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -176,14 +206,33 @@ Lemma add_instr_skip_state_incr : s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))). + (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Lemma add_instr_wait_state_incr : + forall wait_mod s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); auto with htlh. Qed. -Definition add_instr_skip (n : node) (st : stmnt) : mon unit := +Definition add_instr_wait (wait_mod : ident) (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -194,7 +243,23 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) + (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))) + (add_instr_wait_state_incr wait_mod s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr_wait") + end. + +Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))) (add_instr_skip_state_incr s n st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -210,7 +275,7 @@ Lemma add_node_skip_state_incr : (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))). Proof. constructor; intros; @@ -218,7 +283,7 @@ Proof. auto with htlh. Qed. -Definition add_node_skip (n : node) (st : stmnt) : mon unit := +Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -228,15 +293,12 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))) (add_node_skip_state_incr s n st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. -Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. -Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. - Definition bop (op : binop) (r1 r2 : reg) : expr := Vbinop op (Vvar r1) (Vvar r2). @@ -386,7 +448,7 @@ Lemma add_branch_instr_state_incr: (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (data_vstmnt Vskip) (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). Proof. intros. apply state_incr_intro; simpl; @@ -404,7 +466,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (data_vstmnt Vskip) (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") @@ -450,26 +512,33 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni match i with | Inop n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then - add_instr n n' Vskip + add_instr n n' (data_vstmnt Vskip) else error (Errors.msg "State is larger than 2^32.") | Iop op args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do instr <- translate_instr op args; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst instr) + add_instr n n' (data_vstmnt (nonblock dst instr)) else error (Errors.msg "State is larger than 2^32.") | Iload mem addr args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do src <- translate_arr_access mem addr args stack; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + add_instr n n' (data_vstmnt (nonblock dst src)) else error (Errors.msg "State is larger than 2^32.") | Istore mem addr args src n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + add_instr n n' (data_vstmnt (Vnonblock dst (Vvar src))) (* TODO: Could juse use add_instr? reg exists. *) + else error (Errors.msg "State is larger than 2^32.") + | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") + | Icall sig (inr fn) args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do _ <- declare_reg None dst 32; + do join_state <- create_state; + do _ <- add_instr n join_state (HTLfork fn args); + add_instr_wait fn join_state n' (HTLjoin fn dst) else error (Errors.msg "State is larger than 2^32.") - | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") | Icond cond args n1 n2 => @@ -484,9 +553,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Ireturn r => match r with | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) + add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))) | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) + add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))) end end end. @@ -542,11 +611,11 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -Definition max_pc_map (m : Maps.PTree.t stmnt) := +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. Lemma max_pc_map_sound: - forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). Proof. intros until i. unfold max_pc_function. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). @@ -561,8 +630,8 @@ Proof. Qed. Lemma max_pc_wf : - forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - map_well_formed m. + 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. @@ -600,7 +669,7 @@ Definition transf_module (f: function) : mon module := clk current_state.(st_scldecls) current_state.(st_arrdecls) - (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) | _, _ => error (Errors.msg "More than 2^32 states.") end else error (Errors.msg "Stack size misalignment."). diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index f1e6b2a..def5ca7 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -55,8 +55,8 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). Module HTLState <: State. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 9a7e272..98b57ae 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -405,7 +405,7 @@ Section CORRECTNESS. Lemma op_stack_based : forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') - (Verilog.Vnonblock (Verilog.Vvar res0) e) + (data_vstmnt (Verilog.Vnonblock (Verilog.Vvar res0) e)) (state_goto st pc') -> reg_stack_based_pointers sp rs -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> @@ -1091,11 +1091,13 @@ Section CORRECTNESS. inv CONST; assumption. inv CONST; assumption. (* processing of state *) - econstructor. + constructor. crush. - econstructor. - econstructor. - econstructor. + constructor. + constructor. + constructor. + constructor. + constructor. all: invert MARR; big_tac. @@ -1128,7 +1130,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor; trivial. econstructor; simpl; eauto. - simpl. econstructor. econstructor. + simpl. econstructor. econstructor. econstructor. constructor. apply H5. simplify. all: big_tac. @@ -1262,7 +1264,9 @@ Section CORRECTNESS. match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. Proof. intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. - inv_state. inv_arr_access. + inv_state. + + inv_arr_access. + (** Preamble *) invert MARR. inv CONST. crush. @@ -1335,15 +1339,16 @@ Section CORRECTNESS. inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. + (** Start of proof proper *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. + econstructor. econstructor. econstructor. all: big_tac. @@ -1473,7 +1478,7 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. @@ -1577,8 +1582,8 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. econstructor. crush. all: big_tac. @@ -1693,7 +1698,7 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. econstructor. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. @@ -1972,7 +1977,7 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. constructor. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. econstructor. @@ -2225,7 +2230,7 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. econstructor. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. @@ -2457,13 +2462,13 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. - econstructor; simpl; trivial. + econstructor; econstructor; simpl; trivial. constructor; trivial. eapply Verilog.erun_Vternary_true; simpl; eauto. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2474,13 +2479,13 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. - econstructor; simpl; trivial. + econstructor; econstructor; simpl; trivial. constructor; trivial. eapply Verilog.erun_Vternary_false; simpl; eauto. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2528,12 +2533,12 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. - constructor. + constructor. econstructor. econstructor; simpl; trivial. econstructor; simpl; trivial. constructor. econstructor; simpl; trivial. - constructor. + constructor. constructor. constructor. constructor. @@ -2559,7 +2564,7 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. - constructor. + constructor. constructor. econstructor. econstructor; simpl; trivial. econstructor; simpl; trivial. constructor. constructor. constructor. @@ -2795,7 +2800,7 @@ Section CORRECTNESS. exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. Proof. induction 1; eauto with htlproof; (intros; inv_state). - Qed. + Admitted. Hint Resolve transl_step_correct : htlproof. Theorem transf_program_correct: diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 845b1d5..b76b8ec 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -125,39 +125,43 @@ Ltac monadInv H := statemachine that is created by the translation contains the correct translations for each of the elements *) -Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := +Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop := | tr_instr_Inop : forall n, Z.pos n <= Int.max_unsigned -> - tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) + tr_instr fin rtrn st stk (RTL.Inop n) (data_vstmnt Vskip) (state_goto st n) | tr_instr_Iop : forall n op args dst s s' e i, Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (data_vstmnt (Vnonblock (Vvar dst) e)) (state_goto st n) +| tr_instr_Icall : + forall n sig fn args dst, + Z.pos n <= Int.max_unsigned -> + tr_instr fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) (HTLfork fn args) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, Z.pos n1 <= Int.max_unsigned -> Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) + tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) (data_vstmnt Vskip) (state_cond st c n1 n2) | tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vlit (ZToValue 0%Z)))) Vskip + tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip) | tr_instr_Ireturn_Some : forall r, tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip + (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip) | tr_instr_Iload : forall mem addr args s s' i c dst n, Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (data_vstmnt (nonblock dst c)) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (data_vstmnt (Vnonblock c (Vvar src))) (state_goto st n). (*| tr_instr_Ijumptable : forall cexpr tbl r, @@ -165,7 +169,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) Hint Constructors tr_instr : htlspec. -Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) +Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts : datapath) (trans : controllogic) (fin rtrn st stk : reg) : Prop := tr_code_intro : forall s t, @@ -422,6 +426,13 @@ Lemma add_instr_freshreg_trans : Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. Hint Resolve add_instr_freshreg_trans : htlspec. +Lemma add_instr_wait_freshreg_trans : + forall m n n' st s r s' i, + add_instr_wait m n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_wait in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + Lemma add_branch_instr_freshreg_trans : forall n n0 n1 e s r s' i, add_branch_instr e n n0 n1 s = OK r s' i -> @@ -429,6 +440,13 @@ Lemma add_branch_instr_freshreg_trans : Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. Hint Resolve add_branch_instr_freshreg_trans : htlspec. +Lemma create_state_freshreg_trans : + forall n s s' i, + create_state s = OK n s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold create_state in H. inv H. auto. Qed. +Hint Resolve create_state_freshreg_trans : htlspec. + Lemma add_node_skip_freshreg_trans : forall n1 n2 s r s' i, add_node_skip n1 n2 s = OK r s' i -> @@ -449,12 +467,18 @@ Lemma transf_instr_freshreg_trans : s.(st_freshreg) = s'.(st_freshreg). Proof. intros. destruct instr eqn:?. subst. unfold transf_instr in H. - destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + destruct i0 eqn:EQ__i; try (monadInv H); try (unfold_match H); eauto with htlspec. - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. + - unfold_match H. monadInv H. + apply declare_reg_freshreg_trans in EQ. + apply add_instr_freshreg_trans in EQ0. + apply create_state_freshreg_trans in EQ1. + apply add_instr_wait_freshreg_trans in EQ3. + congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) @@ -490,6 +514,7 @@ Ltac inv_add_instr' H := Ltac inv_add_instr := match goal with | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr + | H: (match ?e with | inr _ => _ | inl _ => _ end) _ = OK _ _ _ |- _ => destruct e eqn:EQI; try discriminate; inv_add_instr | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -525,7 +550,7 @@ Proof. destruct (peq pc pc1). - subst. destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. + try destruct_optional; try inv_add_instr; econstructor; try assumption. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. @@ -553,6 +578,17 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. + + admit. (* destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; discriminate. *) + + admit. (* destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; discriminate. *) + + admit. + (* destruct H2. *) + (* * inversion H2. *) + (* replace (st_st s2) with (st_st s0) by congruence. *) + (* replace (st_st s1) with (st_st s0) by congruence. *) + (* econstructor. *) + (* apply Z.leb_le. assumption. *) + (* * apply in_map with (f := fst) in H2. contradiction. *) + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct H2. @@ -588,7 +624,7 @@ Proof. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. destruct H2. inv H2. contradiction. assumption. assumption. -Qed. +Admitted. Hint Resolve iter_expand_instr_spec : htlspec. Lemma create_arr_inv : forall w x y z a b c d, diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index a75d0ee..836222e 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -30,35 +30,57 @@ open VericertClflags let pstr pp = fprintf pp "%s" -let reg pp r = - fprintf pp "x%d" (P.to_int r) +let concat = String.concat "" -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + +let register a = sprintf "reg_%d" (P.to_int a) +let registers a = String.concat "" (intersperse ", " (List.map register a)) let print_instruction pp (pc, i) = fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) +let pprint_datapath_stmnt i = function + | HTLDataVstmnt s -> pprint_stmnt i s + | HTLfork (name, args) -> concat [ + "fork "; extern_atom name; "("; concat (intersperse ", " (List.map register args)); ");\n" + ] + | HTLjoin (name, dst) -> concat [ + register dst; " <= join "; extern_atom name; ";\n" + ] + +let print_datapath_instruction pp (pc, i) = + fprintf pp "%5d:\t%s" pc (pprint_datapath_stmnt 0 i) + +let pprint_control_stmnt i = function + | HTLCtrlVstmnt s -> pprint_stmnt i s + | HTLwait (name, statereg, expr) -> concat [ + "wait("; extern_atom name; ", "; + register statereg; ", "; + pprint_expr expr; ");\n" + ] + +let print_control_instruction pp (pc, i) = + fprintf pp "%5d:\t%s" pc (pprint_control_stmnt 0 i) + +let ptree_to_list ptree = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements ptree)) + let print_module pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params; - let datapath = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.mod_datapath)) in - let controllogic = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.mod_controllogic)) in - fprintf pp " datapath {\n"; - List.iter (print_instruction pp) datapath; + fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); + let datapath = ptree_to_list f.mod_datapath in + let controllogic = ptree_to_list f.mod_controllogic in + fprintf pp "datapath {\n"; + List.iter (print_datapath_instruction pp) datapath; fprintf pp " }\n\n controllogic {\n"; - List.iter (print_instruction pp) controllogic; + List.iter (print_control_instruction pp) controllogic; fprintf pp " }\n}\n\n" let print_globdef pp (id, gd) = diff --git a/src/hls/PrintVerilog.mli b/src/hls/PrintVerilog.mli index 6a15ee9..dbb8ba0 100644 --- a/src/hls/PrintVerilog.mli +++ b/src/hls/PrintVerilog.mli @@ -18,6 +18,8 @@ val pprint_stmnt : int -> Verilog.stmnt -> string +val pprint_expr : Verilog.expr -> string + val print_value : out_channel -> ValueInt.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index a7db3ba..ca5abd4 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -251,6 +251,20 @@ Definition posToLit (p : positive) : expr := Definition fext := unit. Definition fextclk := nat -> fext. +Definition map_body (f : list module_item -> list module_item) (m : module) := + mkmodule + (mod_start m) + (mod_reset m) + (mod_clk m) + (mod_finish m) + (mod_return m) + (mod_st m) + (mod_stk m) + (mod_stk_len m) + (mod_args m) + (f (mod_body m)) + (mod_entrypoint m). + (** ** State The [state] contains the following items: diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 80c0669..a7a8c2a 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2021 Michalis Pardalos <mpardalos@gmail.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -17,54 +18,348 @@ *) Require Import compcert.common.AST. -Require compcert.common.Errors. -Require Import compcert.lib.Maps. +Require Import compcert.common.Errors. +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.ValueInt. Require Import vericert.hls.Verilog. +Import ListNotations. -Definition transl_list_fun (a : node * Verilog.stmnt) := - let (n, stmnt) := a in - (Vlit (posToValue n), stmnt). - -Definition transl_list st := map transl_list_fun st. - -Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := - match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. - -Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. - -Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := - match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. - -Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. - -Definition transl_module (m : HTL.module) : Verilog.module := - let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in - let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in - let body := - Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) - (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip)) - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in - Verilog.mkmodule m.(HTL.mod_start) - m.(HTL.mod_reset) - m.(HTL.mod_clk) - m.(HTL.mod_finish) - m.(HTL.mod_return) - m.(HTL.mod_st) - m.(HTL.mod_stk) - m.(HTL.mod_stk_len) - m.(HTL.mod_params) - body - m.(HTL.mod_entrypoint). - -Definition transl_fundef := transf_fundef transl_module. - -Definition transl_program (p: HTL.program) : Verilog.program := - transform_program transl_fundef p. +Local Open Scope error_monad_scope. + +Record renumber_state: Type := + mk_renumber_state { + st_freshreg : reg; + st_regmap : PTree.t reg; + }. + +Module RenumberState <: State. + Definition st := renumber_state. + + Definition st_prop (st1 st2 : st) := True. + + Lemma st_refl : forall (s : st), st_prop s s. + Proof. constructor. Qed. + + Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. constructor. Qed. +End RenumberState. + +Module VerilogMonad := Statemonad(RenumberState). + +Module VerilogMonadExtra := Monad.MonadExtra(VerilogMonad). + +Section RENUMBER. + Export RenumberState. + Export VerilogMonad. + Import VerilogMonadExtra. + Export MonadNotation. + + Definition renumber_reg (r : reg) : mon reg := + do st <- get; + match PTree.get r st.(st_regmap) with + | Some reg' => ret reg' + | None => + do tt <- set (mk_renumber_state (Pos.succ st.(st_freshreg)) (PTree.set r st.(st_freshreg) st.(st_regmap))) (fun _ => I); + ret st.(st_freshreg) + end. + + Fixpoint renumber_edge (edge : Verilog.edge) := + match edge with + | Vposedge r => + do r' <- renumber_reg r; + ret (Vposedge r') + | Vnegedge r => + do r' <- renumber_reg r; + ret (Vposedge r') + | Valledge => ret Valledge + | Voredge e1 e2 => + do e1' <- renumber_edge e1; + do e2' <- renumber_edge e2; + ret (Voredge e1' e2') + end. + + Definition renumber_declaration (decl : Verilog.declaration) := + match decl with + | Vdecl io reg sz => + do reg' <- renumber_reg reg; + ret (Vdecl io reg' sz) + | Vdeclarr io reg sz len => + do reg' <- renumber_reg reg; + ret (Vdeclarr io reg' sz len) + end. + + Fixpoint renumber_expr (expr : Verilog.expr) := + match expr with + | Vlit val => ret (Vlit val) + | Vvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vvari reg e => + do reg' <- renumber_reg reg; + do e' <- renumber_expr e; + ret (Vvari reg' e') + | Vinputvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vbinop op e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vbinop op e1' e2') + | Vunop op e => + do e' <- renumber_expr e; + ret (Vunop op e) + | Vternary e1 e2 e3 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do e3' <- renumber_expr e3; + ret (Vternary e1' e2' e3') + | Vrange r e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do r' <- renumber_reg r; + ret (Vrange r e1 e2) + end. + + Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := + match stmnt with + | Vskip => ret Vskip + | Vseq s1 s2 => + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- renumber_expr e; + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vcond e' s1' s2') + | Vcase e cs def => + do e' <- renumber_expr e; + do cs' <- sequence (map + (fun (c : (Verilog.expr * Verilog.stmnt)) => + let (c_expr, c_stmnt) := c in + do expr' <- renumber_expr c_expr; + do stmnt' <- renumber_stmnt c_stmnt; + ret (expr', stmnt')) cs); + do def' <- match def with + | None => ret None + | Some d => do def' <- renumber_stmnt d; ret (Some def') + end; + ret (Vcase e' cs' def') + | Vblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vnonblock e1' e2') + end. + + Definition renumber_module_item (item : Verilog.module_item) := + match item with + | Vdeclaration decl => + do decl' <- renumber_declaration decl; + ret (Vdeclaration decl') + | Valways edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + | Valways_ff edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + | Valways_comb edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + end. + + Definition renumber_module (m : Verilog.module) : mon Verilog.module := + do mod_start' <- renumber_reg (Verilog.mod_start m); + do mod_reset' <- renumber_reg (Verilog.mod_reset m); + do mod_clk' <- renumber_reg (Verilog.mod_clk m); + do mod_finish' <- renumber_reg (Verilog.mod_finish m); + do mod_return' <- renumber_reg (Verilog.mod_return m); + do mod_st' <- renumber_reg (Verilog.mod_st m); + do mod_stk' <- renumber_reg (Verilog.mod_stk m); + do mod_args' <- traverselist renumber_reg (Verilog.mod_args m); + do mod_body' <- traverselist renumber_module_item (Verilog.mod_body m); + + ret (Verilog.mkmodule + mod_start' + mod_reset' + mod_clk' + mod_finish' + mod_return' + mod_st' + mod_stk' + (Verilog.mod_stk_len m) + mod_args' + mod_body' + (Verilog.mod_entrypoint m)). + + Definition renumber_all_modules + (modules : PTree.t Verilog.module) + (start_reg : reg) + (clk : reg) : Errors.res (PTree.t Verilog.module) := + + run_mon (mk_renumber_state start_reg (PTree.empty reg)) + (VerilogMonadExtra.traverse_ptree1 (fun m => + do st <- VerilogMonad.get; + do _ <- VerilogMonad.set + (mk_renumber_state (st_freshreg st) + (PTree.set (mod_clk m) clk + (PTree.empty reg))) + (fun _ => I); + renumber_module m) + modules). +End RENUMBER. + + +Section TRANSLATE. + Local Open Scope error_monad_scope. + + Definition transl_datapath_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.datapath_stmnt) := + let (n, s) := a in + let node := Verilog.Vlit (posToValue n) in + match s with + | HTL.HTLfork mod_name args => + do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); + let reset_mod := Vnonblock (Vvar (Verilog.mod_reset m)) (posToLit 1) in + let zipped_args := List.combine (Verilog.mod_args m) args in + let assign_args := + List.fold_left (fun (acc : stmnt) (a : reg * reg) => let (to, from) := a in + Vseq acc (Vnonblock (Vvar to) (Vvar from))) + zipped_args Vskip in + OK (node, Vseq reset_mod assign_args) + | HTL.HTLjoin mod_name dst => + do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); + let set_result := Vnonblock (Vvar dst) (Vvar (Verilog.mod_return m)) in + let stop_reset := Vnonblock (Vvar (Verilog.mod_reset m)) (Vlit (ZToValue 0)) in + OK (node, Vseq stop_reset set_result) + | HTL.HTLDataVstmnt s => OK (node, s) + end. + + Definition transl_datapath modmap st := Errors.mmap (transl_datapath_fun modmap) st. + + Definition transl_ctrl_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):= + let (n, s) := a in + let node := Verilog.Vlit (posToValue n) in + match s with + | HTL.HTLwait mod_name status expr => + do mod_body <- handle_opt (Errors.msg "module does not exist") (PTree.get mod_name modmap); + let is_done := Vbinop Veq (Vvar (Verilog.mod_finish mod_body)) (Vlit (posToValue 1)) in + let continue := Vnonblock (Vvar status) expr in + Errors.OK (node, Verilog.Vcond is_done continue Vskip) + | HTL.HTLCtrlVstmnt s => Errors.OK (node, s) + end. + + Definition transl_ctrl modmap st := Errors.mmap (transl_ctrl_fun modmap) st. + + Definition scl_to_Vdecl_fun (a : reg * (option Verilog.io * Verilog.scl_decl)) := + match a with (r, (io, Verilog.VScalar sz)) => (Verilog.Vdecl io r sz) end. + + Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. + + Definition arr_to_Vdeclarr_fun (a : reg * (option Verilog.io * Verilog.arr_decl)) := + match a with (r, (io, Verilog.VArray sz l)) => (Verilog.Vdeclarr io r sz l) end. + + Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. + + Definition called_functions (stmnts : list (Verilog.node * HTL.datapath_stmnt)) : list ident := + List.nodup Pos.eq_dec (Option.map_option (fun (a : (positive * HTL.datapath_stmnt)) => + let (n, stmt) := a in + match stmt with + | HTL.HTLfork fn _ => Some fn + | _ => None + end) stmnts). + + Definition find_module (program : HTL.program) (name : ident) : Errors.res HTL.module := + match option_map snd (find (fun named_module => Pos.eqb (fst named_module) name) program.(prog_defs)) with + | Some (Gfun (Internal f)) => OK f + | _ => Error (msg "Veriloggen: Could not find definition for called module") + end. + + Definition max_reg_module (m : HTL.module) : positive := + fold_left Pos.max ( + [ HTL.mod_st m + ; HTL.mod_stk m + ; HTL.mod_finish m + ; HTL.mod_return m + ; HTL.mod_start m + ; HTL.mod_reset m + ; HTL.mod_clk m + ] ++ HTL.mod_params m ++ map fst (PTree.elements (mod_scldecls m)) ++ map fst (PTree.elements (mod_arrdecls m))) 1%positive. + + 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 + | Vdeclaration (Vdecl (Some _) reg sz) => + if Pos.eqb reg clk + then None + else Some (Vdeclaration (Vdecl None reg sz)) + | Vdeclaration (Vdeclarr (Some _) reg sz len) => + Some (Vdeclaration (Vdeclarr None reg sz len)) + | _ => Some it + end. + + (* FIXME Remove the fuel parameter (recursion limit)*) + Fixpoint transf_module (fuel : nat) (program : HTL.program) (m : HTL.module) : res Verilog.module := + match fuel with + | O => Error (msg "Veriloggen: transf_module recursion too deep") + | S fuel' => + + let inline_start_reg := max_reg_module m in + let inline_names := called_functions (PTree.elements (HTL.mod_datapath m)) in + let htl_modules := PTree.filter + (fun m _ => List.existsb (Pos.eqb m) inline_names) + (prog_modmap program) in + do translated_modules <- PTree.traverse (fun _ => transf_module fuel' program) htl_modules; + do renumbered_modules <- renumber_all_modules translated_modules (max_reg_module m) (HTL.mod_clk m); + let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl (HTL.mod_clk m)))) + renumbered_modules in + + do case_el_ctrl <- transl_ctrl renumbered_modules (PTree.elements (HTL.mod_controllogic m)); + do case_el_data <- transl_datapath renumbered_modules (PTree.elements (HTL.mod_datapath m)); + + let body : list Verilog.module_item:= + Valways (Vposedge (HTL.mod_clk m)) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m)))) + (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge (HTL.mod_clk m)) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements (HTL.mod_arrdecls m)) + ++ scl_to_Vdecl (AssocMap.elements (HTL.mod_scldecls m))) + ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) in + + OK (Verilog.mkmodule + (HTL.mod_start m) + (HTL.mod_reset m) + (HTL.mod_clk m) + (HTL.mod_finish m) + (HTL.mod_return m) + (HTL.mod_st m) + (HTL.mod_stk m) + (HTL.mod_stk_len m) + (HTL.mod_params m) + body + (HTL.mod_entrypoint m) + ) + end. + + Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transf_module 10 prog). + Definition transl_program (prog : HTL.program) := transform_partial_program (transl_fundef prog) prog. + +End TRANSLATE. diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..59267f7 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -17,14 +17,18 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. +From compcert Require Errors. From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. + Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := - match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. + +(* Lemma transf_program_match: forall prog, match_prog prog (transl_program prog). @@ -97,19 +101,31 @@ Proof. intros. unfold posToValue. rewrite Int.unsigned_repr; lia. Qed. -Lemma transl_list_fun_fst : +Lemma transl_ctrl_fun_fst : forall p1 p2 a b, 0 <= Z.pos p1 <= Int.max_unsigned -> 0 <= Z.pos p2 <= Int.max_unsigned -> - transl_list_fun (p1, a) = transl_list_fun (p2, b) -> + transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) -> (p1, a) = (p2, b). Proof. - intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1. + intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1. destruct H1. rewrite H2. apply Vlit_inj in H1. apply posToValue_inj in H1; try assumption. rewrite H1; auto. Qed. +Lemma transl_data_fun_fst : + forall p1 p2 a b, + 0 <= Z.pos p1 <= Int.max_unsigned -> + 0 <= Z.pos p2 <= Int.max_unsigned -> + transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) -> + p1 = p2. +Proof. + intros. + unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1. + apply Vlit_inj in H1. apply posToValue_inj in H1; assumption. +Qed. + Lemma Zle_relax : forall p q r, p < q <= r -> @@ -121,7 +137,7 @@ Lemma transl_in : forall l p, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> + In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) -> In p (map fst l). Proof. induction l. @@ -136,12 +152,12 @@ Lemma transl_notin : forall l p, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)). + ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)). Proof. induction l; auto. intros. destruct a. unfold not in *. intros. simplify. destruct (peq p0 p). apply H1. auto. apply H1. - unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. + unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. contradiction. auto with verilogproof. auto. right. apply transl_in; auto. @@ -150,7 +166,7 @@ Qed. Lemma transl_norepet : forall l, (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)). + list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)). Proof. induction l. - intros. simpl. apply list_norepet_nil. @@ -161,7 +177,7 @@ Proof. simplify. inv H0. assumption. Qed. -Lemma transl_list_correct : +Lemma transl_ctrl_correct : forall l v ev f asr asa asrn asan asr' asa' asrn' asan', (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (List.map fst l) -> @@ -178,7 +194,7 @@ Lemma transl_list_correct : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (transl_list l) (Some Vskip)) + (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). Proof. @@ -202,7 +218,30 @@ Proof. eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. trivial. assumption. Qed. -Hint Resolve transl_list_correct : verilogproof. +Hint Resolve transl_ctrl_correct : verilogproof. + +(* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *) +Lemma transl_datapath_correct : + forall l v ev f asr asa asrn asan asr' asa' asrn' asan', + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + list_norepet (List.map fst l) -> + asr!ev = Some v -> + (forall p s, + In (p, s) l -> + v = posToValue p -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + s + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). +Proof. Admitted. Lemma pc_wf : forall A m p v, @@ -288,7 +327,7 @@ Section CORRECTNESS. econstructor. simpl. auto. auto. - eapply transl_list_correct. + eapply transl_ctrl_correct. intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. @@ -302,6 +341,8 @@ Section CORRECTNESS. econstructor. econstructor. + { admit. + (* eapply transl_list_correct. intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. apply Maps.PTree.elements_keys_norepet. eassumption. @@ -313,10 +354,11 @@ Section CORRECTNESS. split. lia. apply HP. eassumption. eassumption. trivial. } apply Maps.PTree.elements_correct. eassumption. eassumption. + *) + } apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. rewrite valueToPos_posToValue. constructor; assumption. lia. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. constructor; assumption. - econstructor; split. apply Smallstep.plus_one. constructor. @@ -325,7 +367,7 @@ Section CORRECTNESS. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. apply match_state. assumption. - Qed. + Admitted. Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : @@ -366,3 +408,4 @@ Section CORRECTNESS. Qed. End CORRECTNESS. +*) |