diff options
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/AssocMap.v | 29 | ||||
-rw-r--r-- | src/hls/ClockMemory.v | 79 | ||||
-rw-r--r-- | src/hls/ClockRegisters.v | 210 | ||||
-rw-r--r-- | src/hls/DHTL.v | 9 | ||||
-rw-r--r-- | src/hls/DMemorygen.v | 40 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 131 | ||||
-rw-r--r-- | src/hls/HTLPargenproof.v | 231 | ||||
-rw-r--r-- | src/hls/Memorygen.v | 6 | ||||
-rw-r--r-- | src/hls/Verilog.v | 18 |
9 files changed, 493 insertions, 260 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 4941b0e..1773c0c 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -252,15 +252,15 @@ Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : Local Open Scope assocmap. Lemma find_get_assocmap : - forall assoc r v, + forall n assoc r v, assoc ! r = Some v -> - assoc # r = v. + find_assocmap n r assoc = v. Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. Lemma merge_get_default : - forall ars ars' r x, + forall n ars ars' r x, ars ! r = Some x -> - (AssocMapExt.merge _ ars ars') # r = x. + find_assocmap n r (AssocMapExt.merge _ ars ars') = x. Proof. unfold AssocMapExt.merge; intros. unfold "#", AssocMapExt.get_default. @@ -270,9 +270,9 @@ Proof. Qed. Lemma merge_get_default2 : - forall ars ars' r, + forall n ars ars' r, ars ! r = None -> - (AssocMapExt.merge _ ars ars') # r = ars' # r. + find_assocmap n r (AssocMapExt.merge _ ars ars') = find_assocmap n r ars'. Proof. unfold AssocMapExt.merge; intros. unfold "#", AssocMapExt.get_default. @@ -324,3 +324,20 @@ Proof. rewrite ! AssocMap.gcombine by auto. now rewrite AssocMap.gso by auto. Qed. + +Lemma assocmap_gso : + forall n a a' c b, + a <> a' -> + find_assocmap n a (AssocMap.set a' c b) = find_assocmap n a b. +Proof. + intros. unfold find_assocmap, AssocMapExt.get_default. + now rewrite AssocMap.gso by auto. +Qed. + +Lemma assocmap_gss : + forall n a c b, + find_assocmap n a (AssocMap.set a c b) = c. +Proof. + intros. unfold find_assocmap, AssocMapExt.get_default. + now rewrite AssocMap.gss by auto. +Qed. diff --git a/src/hls/ClockMemory.v b/src/hls/ClockMemory.v new file mode 100644 index 0000000..3d068ad --- /dev/null +++ b/src/hls/ClockMemory.v @@ -0,0 +1,79 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.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 + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import Coq.FSets.FMapPositive. +Require Import Coq.micromega.Lia. + +Require compcert.common.Events. +Require compcert.common.Globalenvs. +Require compcert.common.Smallstep. +Require compcert.common.Values. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.common.AST. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.Array. +Require Import vericert.common.Monad. +Require Import vericert.common.Optionmonad. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.DHTL. + +Import OptionExtra. + +#[local] Open Scope monad_scope. + +Definition pred := positive. + +Definition transf_maps (d: stmnt) := + match d with + | Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2) => + Vseq rest (Vnonblock (Vvari r e1) e2) + | Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2)) => + Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vvari r e2)) + | _ => d + end. + +Program Definition transf_module (m: DHTL.module) : DHTL.module := + mkmodule m.(mod_params) + (PTree.map1 transf_maps m.(mod_datapath)) + m.(mod_entrypoint) + m.(mod_st) + m.(mod_stk) + m.(mod_stk_len) + m.(mod_finish) + m.(mod_return) + m.(mod_start) + m.(mod_reset) + m.(mod_clk) + m.(mod_scldecls) + m.(mod_arrdecls) + m.(mod_ram) + _ + m.(mod_ordering_wf) + m.(mod_ram_wf) + m.(mod_params_wf). +Next Obligation. +Admitted. + +Definition transf_fundef := transf_fundef transf_module. + +Definition transf_program (p : DHTL.program) : DHTL.program := + transform_program transf_fundef p. diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v index 4b1c37a..6ef15c7 100644 --- a/src/hls/ClockRegisters.v +++ b/src/hls/ClockRegisters.v @@ -32,14 +32,17 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. Require Import vericert.hls.DHTL. -Require Import vericert.common.Monad. -Require Import vericert.common.Optionmonad. Require vericert.hls.Verilog. -Import OptionExtra. +Require Import vericert.common.Errormonad. +Import ErrorMonad. +Import ErrorMonadExtra. +Import MonadNotation. #[local] Open Scope monad_scope. +Definition error {A} m := @Errors.Error A (Errors.msg m). + Definition pred := positive. Inductive lhs : Type := @@ -70,111 +73,90 @@ Module RTree := ITree(R_indexed). Inductive flat_expr : Type := | FVlit : value -> flat_expr -| FVvar : lhs -> flat_expr +| FVvar : reg -> flat_expr | FVbinop : Verilog.binop -> flat_expr -> flat_expr -> flat_expr | FVunop : Verilog.unop -> flat_expr -> flat_expr | FVternary : flat_expr -> flat_expr -> flat_expr -> flat_expr . Inductive flat_stmnt : Type := -| FVblock : lhs -> flat_expr -> flat_stmnt -| FVnonblock : lhs -> flat_expr -> flat_stmnt +| FVblock : reg -> flat_expr -> flat_stmnt +| FVnonblock : reg -> flat_expr -> flat_stmnt . -Fixpoint flatten_expr (preg: reg) (e: Verilog.expr) : option flat_expr := +Fixpoint flatten_expr (e: Verilog.expr) : Errors.res flat_expr := match e with - | Verilog.Vlit v => Some (FVlit v) - | Verilog.Vvar r => Some (FVvar (LhsReg r)) - | Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2) => - if Pos.eqb preg r && Int.eq i1 i2 then - match Int.unsigned i1 with - | Zpos p => Some (FVvar (LhsPred p)) - | _ => None - end - else None + | Verilog.Vlit v => ret (FVlit v) + | Verilog.Vvar r => ret (FVvar r) | Verilog.Vunop u e => - match flatten_expr preg e with - | Some fe => Some (FVunop u fe) - | _ => None - end + do fe <- flatten_expr e; + ret (FVunop u fe) | Verilog.Vbinop u e1 e2 => - match flatten_expr preg e1, flatten_expr preg e2 with - | Some fe1, Some fe2 => Some (FVbinop u fe1 fe2) - | _, _ => None - end + do fe1 <- flatten_expr e1; + do fe2 <- flatten_expr e2; + ret (FVbinop u fe1 fe2) | Verilog.Vternary e1 e2 e3 => - match flatten_expr preg e1, flatten_expr preg e2, flatten_expr preg e3 with - | Some fe1, Some fe2, Some fe3 => Some (FVternary fe1 fe2 fe3) - | _, _, _ => None - end - | _ => None + do fe1 <- flatten_expr e1; + do fe2 <- flatten_expr e2; + do fe3 <- flatten_expr e3; + ret (FVternary fe1 fe2 fe3) + | Verilog.Vrange _ _ _ => error "ClockRegisters: Could not translate Vrange" + | Verilog.Vvari _ _ => error "ClockRegisters: Could not translate Vvari" + | Verilog.Vinputvar _ => error "ClockRegisters: Could not translate Vinputvar" end. -Fixpoint flatten_seq_block (preg: reg) (s: Verilog.stmnt) : option (list flat_stmnt) := +Fixpoint flatten_seq_block (s: Verilog.stmnt) : Errors.res (list flat_stmnt) := match s with - | Verilog.Vskip => Some nil + | Verilog.Vskip => ret nil | Verilog.Vseq s1 s2 => - match flatten_seq_block preg s1, flatten_seq_block preg s2 with - | Some s1', Some s2' => - Some (s1' ++ s2') - | _, _ => None - end + do s1' <- flatten_seq_block s1; + do s2' <- flatten_seq_block s2; + ret (s1' ++ s2') | Verilog.Vblock (Verilog.Vvar r) e => - match flatten_expr preg e with - | Some fe => Some (FVblock (LhsReg r) fe :: nil) - | _ => None - end - | Verilog.Vblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => - if Pos.eqb preg r && Int.eq i1 i2 then - match Int.unsigned i1, flatten_expr preg e with - | Zpos p, Some fe => Some (FVblock (LhsPred p) fe :: nil) - | _, _ => None - end - else None + do fe <- flatten_expr e; + ret (FVblock r fe :: nil) + (* | Verilog.Vblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => *) + (* if Pos.eqb preg r && Int.eq i1 i2 then *) + (* match Int.unsigned i1, flatten_expr e with *) + (* | Zpos p, Some fe => Some (FVblock p fe :: nil) *) + (* | _, _ => None *) + (* end *) + (* else None *) | Verilog.Vnonblock (Verilog.Vvar r) e => - match flatten_expr preg e with - | Some fe => Some (FVnonblock (LhsReg r) fe :: nil) - | _ => None - end - | Verilog.Vnonblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => - if Pos.eqb preg r && Int.eq i1 i2 then - match Int.unsigned i1, flatten_expr preg e with - | Zpos p, Some fe => Some (FVnonblock (LhsPred p) fe :: nil) - | _, _ => None - end - else None - | _ => None + do fe <- flatten_expr e; + ret (FVnonblock r fe :: nil) + (* | Verilog.Vnonblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => *) + (* if Pos.eqb preg r && Int.eq i1 i2 then *) + (* match Int.unsigned i1, flatten_expr e with *) + (* | Zpos p, Some fe => Some (FVnonblock p fe :: nil) *) + (* | _, _ => None *) + (* end *) + (* else None *) + | _ => error "ClockRegisters: Could not translate seq_block" end. -Fixpoint expand_expr (preg: reg) (f: flat_expr): Verilog.expr := +Fixpoint expand_expr (f: flat_expr): Verilog.expr := match f with | FVlit l => Verilog.Vlit l - | FVvar (LhsReg r) => Verilog.Vvar r - | FVvar (LhsPred p) => Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) (Verilog.Vlit (Int.repr (Zpos p))) - | FVbinop b e1 e2 => Verilog.Vbinop b (expand_expr preg e1) (expand_expr preg e2) - | FVunop b e => Verilog.Vunop b (expand_expr preg e) - | FVternary e1 e2 e3 => Verilog.Vternary (expand_expr preg e1) (expand_expr preg e2) (expand_expr preg e3) + | FVvar r => Verilog.Vvar r + | FVbinop b e1 e2 => Verilog.Vbinop b (expand_expr e1) (expand_expr e2) + | FVunop b e => Verilog.Vunop b (expand_expr e) + | FVternary e1 e2 e3 => Verilog.Vternary (expand_expr e1) (expand_expr e2) (expand_expr e3) end. -Definition expand_assignment (preg: reg) (f: flat_stmnt): Verilog.stmnt := +Definition expand_assignment (f: flat_stmnt): Verilog.stmnt := match f with - | FVblock (LhsReg r) e => Verilog.Vblock (Verilog.Vvar r) (expand_expr preg e) - | FVnonblock (LhsReg r) e => Verilog.Vnonblock (Verilog.Vvar r) (expand_expr preg e) - | FVblock (LhsPred p) e => - Verilog.Vblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) - (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e) - | FVnonblock (LhsPred p) e => - Verilog.Vnonblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) - (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e) + | FVblock r e => Verilog.Vblock (Verilog.Vvar r) (expand_expr e) + | FVnonblock r e => Verilog.Vnonblock (Verilog.Vvar r) (expand_expr e) end. -Definition fold_seq_block (preg: reg) (s: list flat_stmnt): Verilog.stmnt := - fold_left (fun a b => Verilog.Vseq a (expand_assignment preg b)) s Verilog.Vskip. +Definition fold_seq_block (s: list flat_stmnt): Verilog.stmnt := + fold_left (fun a b => Verilog.Vseq a (expand_assignment b)) s Verilog.Vskip. -Fixpoint clock_expr (t: RTree.t flat_expr) (f: flat_expr): flat_expr := +Fixpoint clock_expr (t: PTree.t flat_expr) (f: flat_expr): flat_expr := match f with | FVvar r => - match RTree.get r t with + match PTree.get r t with | Some e => e | None => FVvar r end @@ -192,54 +174,44 @@ Definition clock_assignment (tl: RTree.t flat_expr * list flat_stmnt) (f: flat_s match f with | FVblock r e => let fe := clock_expr t e in - (RTree.set r fe t, l ++ (FVnonblock r fe :: nil)) + (PTree.set r fe t, l ++ (FVnonblock r fe :: nil)) | _ => (t, l ++ (f :: nil)) end. Definition clock_assignments (s: list flat_stmnt): list flat_stmnt := snd (fold_left clock_assignment s (RTree.empty _, nil)). -Definition clock_stmnt_assignments (preg: reg) (s: Verilog.stmnt): option Verilog.stmnt := - match flatten_seq_block preg s with - | Some fs => Some (fold_seq_block preg (clock_assignments fs)) - | None => None - end. - -Program Definition transf_module (m: DHTL.module) : option DHTL.module := - match (PTree.fold (fun b i a => - match b, clock_stmnt_assignments m.(mod_preg) a with - | Some tb, Some a' => Some (PTree.set i a' tb) - | _, _ => None - end)) m.(mod_datapath) (Some (PTree.empty _)) with - | Some dp => - Some (mkmodule m.(mod_params) - dp - m.(mod_entrypoint) - m.(mod_st) - m.(mod_stk) - m.(mod_stk_len) - m.(mod_finish) - m.(mod_return) - m.(mod_start) - m.(mod_reset) - m.(mod_clk) - m.(mod_preg) - m.(mod_scldecls) - m.(mod_arrdecls) - m.(mod_ram) - _ - m.(mod_ordering_wf) - m.(mod_ram_wf) - m.(mod_params_wf)) - | _ => None - end. +Definition clock_stmnt_assignments (s: Verilog.stmnt): Errors.res Verilog.stmnt := + do fs <- flatten_seq_block s; + ret (fold_seq_block (clock_assignments fs)). + +Program Definition transf_module (m: DHTL.module) : Errors.res DHTL.module := + do dp <- PTree.fold (fun b i a => + do tb <- b; + do a' <- clock_stmnt_assignments a; + ret (PTree.set i a' tb)) m.(mod_datapath) (Errors.OK (PTree.empty _)); + ret (mkmodule m.(mod_params) + dp + m.(mod_entrypoint) + m.(mod_st) + m.(mod_stk) + m.(mod_stk_len) + m.(mod_finish) + m.(mod_return) + m.(mod_start) + m.(mod_reset) + m.(mod_clk) + m.(mod_scldecls) + m.(mod_arrdecls) + m.(mod_ram) + _ + m.(mod_ordering_wf) + m.(mod_ram_wf) + m.(mod_params_wf)). Next Obligation. Admitted. -Definition transl_module (m : DHTL.module) : Errors.res DHTL.module := - Verilog.handle_opt (Errors.msg "ClockRegisters: not translated") (transf_module m). - -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transf_fundef := transf_partial_fundef transf_module. -Definition transl_program (p : DHTL.program) : Errors.res DHTL.program := - transform_partial_program transl_fundef p. +Definition transf_program (p : DHTL.program) : Errors.res DHTL.program := + transform_partial_program transf_fundef p. diff --git a/src/hls/DHTL.v b/src/hls/DHTL.v index 6be82ae..b80123c 100644 --- a/src/hls/DHTL.v +++ b/src/hls/DHTL.v @@ -70,7 +70,7 @@ Record ram := mk_ram { /\ ram_wr_en < ram_u_en) }. -Definition module_ordering a b c d e f g h := a < b < c /\ c < d < e /\ e < f < g /\ g < h. +Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. Record module: Type := mkmodule { @@ -85,13 +85,12 @@ Record module: Type := mod_start : reg; mod_reset : reg; mod_clk : reg; - mod_preg : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_ram : option ram; mod_wf : map_well_formed mod_datapath; - mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk mod_preg; - mod_ram_wf : forall r', mod_ram = Some r' -> mod_preg < ram_addr r'; + mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; + mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; mod_params_wf : Forall (Pos.gt mod_st) mod_params; }. @@ -266,7 +265,7 @@ Definition max_reg_module m := (Pos.max (mod_return m) (Pos.max (mod_start m) (Pos.max (mod_reset m) - (Pos.max (mod_clk m) (Pos.max (mod_preg m) (max_reg_ram (mod_ram m))))))))))). + (Pos.max (mod_clk m) (max_reg_ram (mod_ram m)))))))))). Lemma max_fold_lt : forall m l n, m <= n -> m <= (fold_left Pos.max l n). diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index 1b7d2e0..c0fc03d 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -163,6 +163,29 @@ Definition transf_maps state ram in_ (d: PTree.t stmnt) := match in_ with | (i, n) => match PTree.get i d with + (* Conditional store *) + | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) (Vternary cond e2 (Vvari r' e1')))) => + if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then + let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram)))) + (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vblock (Vvar (ram_d_in ram)) e2) + (Vblock (Vvar (ram_addr ram)) e1))) + in + PTree.set i (Vseq rest nd) d + else d + | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) => + if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z + && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state) + then + let nd := + Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) + (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) + (Vblock (Vvar (ram_addr ram)) e2)) + in + let aout := Vblock (Vvar e1) (Vternary cond (Vvar (ram_d_out ram)) edef) in + let redirect := Vblock (Vvar state) (Vlit (posToValue n)) in + (PTree.set i (Vseq redirect nd) (PTree.set n (Vseq (Vblock (Vvar st') e3) aout) d)) + else d | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) e2)) => if r =? (ram_mem ram) then let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) @@ -217,7 +240,7 @@ Proof. eapply H. eapply AssocMapExt.elements_iff; eauto. + rewrite PTree.gso in H1 by auto. eapply H. eapply AssocMapExt.elements_iff; eauto. -Qed. +Admitted. Definition max_pc {A: Type} (m: PTree.t A) := fold_right Pos.max 1%positive (map fst (PTree.elements m)). @@ -298,7 +321,7 @@ Proof. lia. Qed. Lemma module_ram_wf' : forall m addr, addr = max_reg_module m + 1 -> - mod_preg m < addr. + mod_clk m < addr. Proof. unfold max_reg_module; lia. Qed. Definition transf_module (m: module): module. @@ -326,7 +349,6 @@ Definition transf_module (m: module): module. (mod_start m) (mod_reset m) (mod_clk m) - (mod_preg m) (AssocMap.set u_en (None, VScalar 1) (AssocMap.set en (None, VScalar 1) (AssocMap.set wr_en (None, VScalar 1) @@ -792,6 +814,12 @@ Proof. apply IHexpr_runp2; eauto. econstructor. inv H2. simplify. assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia. eapply H5 in H2. apply H4 in H2. auto. auto. + - intros. econstructor. apply IHexpr_runp; eauto. constructor. inv H3. + intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. + eapply H1 in H0. eapply H5. instantiate (1:=1) in H0. lia. eauto. eauto. + inv H3. + intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. + unfold "#". unfold AssocMapExt.get_default. rewrite H5. auto. lia. Qed. #[local] Hint Resolve expr_runp_matches : mgen. @@ -1049,7 +1077,7 @@ Lemma transf_not_changed : (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vnonblock e3 (Vvari r e4)))) -> d!i = Some d_s -> transf_maps state ram (i, n) d = d. -Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed. +Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted. Lemma transf_not_changed_neq : forall state ram n d d' i a d_s, @@ -2242,7 +2270,7 @@ Proof. | |- _ = None => apply max_index_2; lia | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H end; auto. -Qed. +Admitted. Lemma transf_alternatives_neq : forall state ram a n' n d'' d' i d, @@ -3375,7 +3403,7 @@ Section CORRECTNESS. { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H15. auto. + unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). replace (mod_reset (transf_module m)) with (mod_reset m). diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index e9061a5..99461d0 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -36,6 +36,7 @@ Require Import vericert.hls.Predicate. Require Import vericert.common.Errormonad. Import ErrorMonad. Import ErrorMonadExtra. +Import MonadNotation. #[local] Open Scope monad_scope. @@ -48,59 +49,78 @@ Import ErrorMonadExtra. Record control_regs: Type := mk_control_regs { ctrl_st : reg; ctrl_stack : reg; - ctrl_preg : reg; ctrl_fin : reg; ctrl_return : reg; }. -Definition pred_lit (preg: reg) (pred: predicate) := - Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). - -Fixpoint pred_expr (preg: reg) (p: pred_op) := +(* Definition pred_lit (preg: reg) (pred: predicate) := *) +(* Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). *) + +(* Fixpoint pred_expr (preg: reg) (p: pred_op) := *) +(* match p with *) +(* | Plit (b, pred) => *) +(* if b *) +(* then pred_lit preg pred *) +(* else Vunop Vnot (pred_lit preg pred) *) +(* | Ptrue => Vlit (ZToValue 1) *) +(* | Pfalse => Vlit (ZToValue 0) *) +(* | Pand p1 p2 => *) +(* Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) *) +(* | Por p1 p2 => *) +(* Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) *) +(* end. *) + +Definition pred_enc (pred: predicate) := + xI pred. + +Definition reg_enc (r: reg) := + xO r. + +Fixpoint pred_expr (p: pred_op) := match p with | Plit (b, pred) => if b - then pred_lit preg pred - else Vunop Vnot (pred_lit preg pred) + then Vvar (pred_enc pred) + else Vunop Vnot (Vvar (pred_enc pred)) | Ptrue => Vlit (ZToValue 1) | Pfalse => Vlit (ZToValue 0) | Pand p1 p2 => - Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) + Vbinop Vand (pred_expr p1) (pred_expr p2) | Por p1 p2 => - Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) + Vbinop Vor (pred_expr p1) (pred_expr p2) end. Definition assignment : Type := expr -> expr -> stmnt. Definition translate_predicate (a : assignment) - (preg: reg) (p: option pred_op) (dst e: expr) := + (p: option pred_op) (dst e: expr) := match p with | None => a dst e | Some pos => let pos' := deep_simplify peq pos in match sat_pred_simple (negate pos') with | None => a dst e - | Some _ => a dst (Vternary (pred_expr preg pos') e dst) + | Some _ => a dst (Vternary (pred_expr pos') e dst) end end. -Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : stmnt := - translate_predicate Vblock preg p (Vvar st) (Vlit (posToValue n)). +Definition state_goto (p: option pred_op) (st : reg) (n : node) : stmnt := + translate_predicate Vblock p (Vvar st) (Vlit (posToValue n)). -Definition state_cond (preg: reg) (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt := - translate_predicate Vblock preg p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). +Definition state_cond (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt := + translate_predicate Vblock p (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 nonblock (dst : reg) (e : expr) := Vnonblock (Vvar (reg_enc dst)) e. +Definition block (dst : reg) (e : expr) := Vblock (Vvar (reg_enc dst)) e. Definition bop (op : binop) (r1 r2 : reg) : expr := - Vbinop op (Vvar r1) (Vvar r2). + Vbinop op (Vvar (reg_enc r1)) (Vvar (reg_enc r2)). Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := - Vbinop op (Vvar r) (Vlit (intToValue l)). + Vbinop op (Vvar (reg_enc r)) (Vlit (intToValue l)). Definition boplitz (op: binop) (r: reg) (l: Z) : expr := - Vbinop op (Vvar r) (Vlit (ZToValue l)). + Vbinop op (Vvar (reg_enc r)) (Vlit (ZToValue l)). Definition error {A} m := @Errors.Error A (Errors.msg m). @@ -180,7 +200,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then Errors.OK (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + then Errors.OK (Vbinop Vadd (Vvar (reg_enc r1)) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in @@ -196,9 +216,9 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors (** Translate an instruction to a statement. FIX mulhs mulhu *) Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res expr := match op, args with - | Op.Omove, r::nil => Errors.OK (Vvar r) + | Op.Omove, r::nil => Errors.OK (Vvar (reg_enc r)) | Op.Ointconst n, _ => Errors.OK (Vlit (intToValue n)) - | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar r)) + | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar (reg_enc r))) | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2) | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n) @@ -214,15 +234,15 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex | Op.Oorimm n, r::nil => Errors.OK (boplit Vor r n) | Op.Oxor, r1::r2::nil => Errors.OK (bop Vxor r1 r2) | Op.Oxorimm n, r::nil => Errors.OK (boplit Vxor r n) - | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar r)) + | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar (reg_enc r))) | Op.Oshl, r1::r2::nil => Errors.OK (bop Vshl r1 r2) | Op.Oshlimm n, r::nil => Errors.OK (boplit Vshl r n) | Op.Oshr, r1::r2::nil => Errors.OK (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => Errors.OK (boplit Vshr r n) | Op.Oshrximm n, r::nil => - Errors.OK (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) - (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) - (Vbinop Vshru (Vvar r) (Vlit n))) + Errors.OK (Vternary (Vbinop Vlt (Vvar (reg_enc r)) (Vlit (ZToValue 0))) + (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar (reg_enc r))) (Vlit n))) + (Vbinop Vshru (Vvar (reg_enc r)) (Vlit n))) | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n) | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: Ororimm") @@ -232,7 +252,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => do tc <- translate_condition c rl; - Errors.OK (Vternary tc (Vvar r1) (Vvar r2)) + Errors.OK (Vternary tc (Vvar (reg_enc r1)) (Vvar (reg_enc r2))) | Op.Olea a, _ => translate_eff_addressing a args | _, _ => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: other") end. @@ -267,18 +287,18 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := List.map (fun a => match a with - (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + (i, n) => (Vlit (natToValue i), Vblock (Vvar st) (Vlit (posToValue n))) end) (enumerate 0 ns). -Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr) +Definition translate_cfi (fin rtrn state: reg) p (cfi: cf_instr) : Errors.res stmnt := match cfi with | RBgoto n' => - Errors.OK (state_goto preg p state n') + Errors.OK (state_goto p state n') | RBcond c args n1 n2 => do e <- translate_condition c args; - Errors.OK (state_cond preg p state e n1 n2) + Errors.OK (state_cond p state e n1 n2) | RBreturn r => match r with | Some r' => @@ -296,7 +316,7 @@ Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr) Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.") end. -Definition transf_instr (fin rtrn stack state preg: reg) +Definition transf_instr (fin rtrn stack state: reg) (dc: pred_op * stmnt) (i: instr) : Errors.res (pred_op * stmnt) := let '(curr_p, d) := dc in @@ -305,38 +325,38 @@ Definition transf_instr (fin rtrn stack state preg: reg) | RBnop => Errors.OK dc | RBop p op args dst => do instr <- translate_instr op args; - let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) instr in + let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in Errors.OK (curr_p, Vseq d stmnt) | RBload p mem addr args dst => do src <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vnonblock preg (npred p) (Vvar dst) src in + let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in Errors.OK (curr_p, Vseq d stmnt) | RBstore p mem addr args src => do dst <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vnonblock preg (npred p) dst (Vvar src) in + let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in Errors.OK (curr_p, Vseq d stmnt) | RBsetpred p' cond args p => do cond' <- translate_condition cond args; - let stmnt := translate_predicate Vblock preg (npred p') (pred_expr preg (Plit (true, p))) cond' in + let stmnt := translate_predicate Vblock (npred p') (pred_expr (Plit (true, p))) cond' in Errors.OK (curr_p, Vseq d stmnt) | RBexit p cf => - do d_stmnt <- translate_cfi fin rtrn state preg (npred p) cf; + do d_stmnt <- translate_cfi fin rtrn state (npred p) cf; Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt) end. -Definition transf_chained_block (fin rtrn stack state preg: reg) +Definition transf_chained_block (fin rtrn stack state: reg) (dc: @pred_op positive * stmnt) (block: list instr) : Errors.res (pred_op * stmnt) := - mfold_left (transf_instr fin rtrn stack state preg) block (ret dc). + mfold_left (transf_instr fin rtrn stack state) block (ret dc). -Definition transf_parallel_block (fin rtrn stack state preg: reg) +Definition transf_parallel_block (fin rtrn stack state: reg) (dc: @pred_op positive * stmnt) (block: list (list instr)) : Errors.res (pred_op * stmnt) := - mfold_left (transf_chained_block fin rtrn stack state preg) block (ret dc). + mfold_left (transf_chained_block fin rtrn stack state) block (ret dc). -Definition transf_parallel_full_block (fin rtrn stack state preg: reg) +Definition transf_parallel_full_block (fin rtrn stack state: reg) (dc: node * @pred_op positive * datapath) (block: list (list instr)) : Errors.res (node * pred_op * datapath) := @@ -344,25 +364,25 @@ Definition transf_parallel_full_block (fin rtrn stack state preg: reg) match AssocMap.get n dt with | None => do ctrl_init_stmnt <- - translate_cfi fin rtrn state preg (Some curr_p) (RBgoto (n - 1)%positive); - do dc' <- transf_parallel_block fin rtrn stack state preg (curr_p, ctrl_init_stmnt) block; + translate_cfi fin rtrn state (Some curr_p) (RBgoto (n - 1)%positive); + do dc' <- transf_parallel_block fin rtrn stack state (curr_p, ctrl_init_stmnt) block; let '(curr_p', dt_stmnt) := dc' in Errors.OK ((n - 1)%positive, curr_p', AssocMap.set n dt_stmnt dt) | _ => Errors.Error (msg "HtlPargen.transf_parallel_full_block: block not empty") end. -Definition transf_seq_block (fin rtrn stack state preg: reg) +Definition transf_seq_block (fin rtrn stack state: reg) (d: datapath) (n: node) (block: list (list (list instr))) : Errors.res datapath := do res <- mfold_left - (transf_parallel_full_block fin rtrn stack state preg) block (ret (n, Ptrue, d)); + (transf_parallel_full_block fin rtrn stack state) block (ret (n, Ptrue, d)); let '(_, _, d') := res in Errors.OK d'. Definition transf_seq_blockM (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t): res datapath := let (n, i) := ni in - transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) ctrl.(ctrl_preg) d n i. + transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) d n i. Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). @@ -396,9 +416,9 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {True}. +Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) - && (d <? e) && (e <? f) && (f <? g) && (g <? h))%positive true with + && (d <? e) && (e <? f) && (f <? g))%positive true with | left t => left _ | _ => _ end); auto. @@ -407,20 +427,22 @@ Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {T end; unfold module_ordering; auto. Defined. +Definition max_resource_function (f: function) := + Pos.max (reg_enc (max_reg_function f)) (pred_enc (max_pred_function f)). + Program Definition transl_module (f: function) : res DHTL.module := if stack_correct f.(fn_stacksize) then - let st := Pos.succ (max_reg_function f) in + let st := Pos.succ (max_resource_function f) in let fin := Pos.succ st in let rtrn := Pos.succ fin in let stack := Pos.succ rtrn in let start := Pos.succ stack in let rst := Pos.succ start in let clk := Pos.succ rst in - let preg := Pos.succ clk in - do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack preg fin rtrn)) + do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack fin rtrn)) (Maps.PTree.elements f.(GiblePar.fn_code)) (ret (PTree.empty _)); match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned, - decide_order st fin rtrn stack start rst clk preg, + decide_order st fin rtrn stack start rst clk, max_list_dec (GiblePar.fn_params f) st with | left LEDATA, left MORD, left WFPARAMS => @@ -436,7 +458,6 @@ Program Definition transl_module (f: function) : res DHTL.module := start rst clk - preg (AssocMap.empty _) (AssocMap.empty _) None diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v index 5c0272f..0ebd264 100644 --- a/src/hls/HTLPargenproof.v +++ b/src/hls/HTLPargenproof.v @@ -55,25 +55,27 @@ Local Open Scope assocmap. #[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. -Inductive match_assocmaps : GiblePar.function -> Gible.regset -> assocmap -> Prop := - match_assocmap : forall f rs am, - (forall r, Ple r (max_reg_function f) -> - val_value_lessdef (Registers.Regmap.get r rs) am#r) -> - match_assocmaps f rs am. +Inductive match_assocmaps : positive -> positive -> Gible.regset -> Gible.predset -> assocmap -> Prop := + match_assocmap : forall rs pr am max_reg max_pred, + (forall r, Ple r max_reg -> + val_value_lessdef (Registers.Regmap.get r rs) (find_assocmap 32 (reg_enc r) am)) -> + (forall r, Ple r max_pred -> + find_assocmap 1 (pred_enc r) am = boolToValue (PMap.get r pr)) -> + match_assocmaps max_reg max_pred rs pr am. #[local] Hint Constructors match_assocmaps : htlproof. -Inductive match_arrs (m : DHTL.module) (f : GiblePar.function) (sp : Values.val) (mem : mem) : +Inductive match_arrs (stack_size: Z) (stk: positive) (stk_len: nat) (sp : Values.val) (mem : mem) : Verilog.assocmap_arr -> Prop := | match_arr : forall asa stack, - asa ! (m.(DHTL.mod_stk)) = Some stack /\ - stack.(arr_length) = Z.to_nat (f.(GiblePar.fn_stacksize) / 4) /\ + asa ! stk = Some stack /\ + stack.(arr_length) = Z.to_nat (stack_size / 4) /\ (forall ptr, - 0 <= ptr < Z.of_nat m.(DHTL.mod_stk_len) -> + 0 <= ptr < Z.of_nat stk_len -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr)))) (Option.default (NToValue 0) (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> - match_arrs m f sp mem asa. + match_arrs stack_size stk stk_len sp mem asa. Definition stack_based (v : Values.val) (sp : Values.block) : Prop := match v with @@ -105,31 +107,28 @@ Inductive match_frames : list GiblePar.stackframe -> list DHTL.stackframe -> Pro | match_frames_nil : match_frames nil nil. -Inductive match_constants : DHTL.module -> assocmap -> Prop := +Inductive match_constants (rst fin: reg) (asr: assocmap) : Prop := match_constant : - forall m asr, - asr!(DHTL.mod_reset m) = Some (ZToValue 0) -> - asr!(DHTL.mod_finish m) = Some (ZToValue 0) -> - match_constants m asr. - -Definition state_st_wf (m : DHTL.module) (s : DHTL.state) := - forall st asa asr res, - s = DHTL.State res m st asa asr -> - asa!(m.(DHTL.mod_st)) = Some (posToValue st). + asr!rst = Some (ZToValue 0) -> + asr!fin = Some (ZToValue 0) -> + match_constants rst fin asr. + +Definition state_st_wf (asr: assocmap) (st_reg: reg) (st: positive) := + asr!st_reg = Some (posToValue st). #[local] Hint Unfold state_st_wf : htlproof. Inductive match_states : GiblePar.state -> DHTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res ps - (MASSOC : match_assocmaps f rs asr) + (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr) (TF : transl_module f = Errors.OK m) - (WF : state_st_wf m (DHTL.State res m st asr asa)) + (WF : state_st_wf asr m.(DHTL.mod_st) st) (MF : match_frames sf res) - (MARR : match_arrs m f sp mem asa) + (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) sp mem asa) (SP : sp = Values.Vptr sp' (Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp) (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem) - (CONST : match_constants m asr), + (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr), (* Add a relation about ps compared with the state register. *) match_states (GiblePar.State sf f sp st rs ps mem) (DHTL.State res m st asr asa) @@ -189,26 +188,62 @@ Proof. assumption. Qed. -Lemma regs_lessdef_add_greater : - forall f rs1 rs2 n v, - Plt (max_reg_function f) n -> - match_assocmaps f rs1 rs2 -> - match_assocmaps f rs1 (AssocMap.set n v rs2). +Lemma max_reg_lt_resource : + forall f n, + Plt (max_resource_function f) n -> + Plt (reg_enc (max_reg_function f)) n. Proof. - inversion 2; subst. - intros. constructor. - intros. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite AssocMap.gso. eauto. - apply Pos.le_lt_trans with _ _ n in H2. - unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. + unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia. Qed. -#[local] Hint Resolve regs_lessdef_add_greater : htlproof. + +Lemma max_pred_lt_resource : + forall f n, + Plt (max_resource_function f) n -> + Plt (pred_enc (max_pred_function f)) n. +Proof. + unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia. +Qed. + +Lemma plt_reg_enc : + forall a b, Ple a b -> Ple (reg_enc a) (reg_enc b). +Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed. + +Lemma plt_pred_enc : + forall a b, Ple a b -> Ple (pred_enc a) (pred_enc b). +Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed. + +Lemma reg_enc_inj : + forall a b, reg_enc a = reg_enc b -> a = b. +Proof. unfold reg_enc; intros; lia. Qed. + +Lemma pred_enc_inj : + forall a b, pred_enc a = pred_enc b -> a = b. +Proof. unfold pred_enc; intros; lia. Qed. + +(* Lemma regs_lessdef_add_greater : *) +(* forall n m rs1 ps1 rs2 n v, *) +(* Plt (max_resource_function f) n -> *) +(* match_assocmaps n m rs1 ps1 rs2 -> *) +(* match_assocmaps n m rs1 ps1 (AssocMap.set n v rs2). *) +(* Proof. *) +(* inversion 2; subst. *) +(* intros. constructor. *) +(* - apply max_reg_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso. eauto. apply plt_reg_enc in H3. unfold Ple, Plt in *. lia. *) +(* - apply max_pred_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso. eauto. apply plt_pred_enc in H3. unfold Ple, Plt in *. lia. *) +(* Qed. *) +(* #[local] Hint Resolve regs_lessdef_add_greater : htlproof. *) + +Lemma pred_enc_reg_enc_ne : + forall a b, pred_enc a <> reg_enc b. +Proof. unfold not, pred_enc, reg_enc; lia. Qed. Lemma regs_lessdef_add_match : - forall f rs am r v v', + forall m n rs ps am r v v', val_value_lessdef v v' -> - match_assocmaps f rs am -> - match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). + match_assocmaps m n rs ps am -> + match_assocmaps m n (Registers.Regmap.set r v rs) ps (AssocMap.set (reg_enc r) v' am). Proof. inversion 2; subst. constructor. intros. @@ -219,7 +254,10 @@ Proof. rewrite Registers.Regmap.gso; try assumption. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite AssocMap.gso; eauto. + rewrite AssocMap.gso; eauto. unfold not in *; intros; apply n0. apply reg_enc_inj; auto. + + intros. pose proof (pred_enc_reg_enc_ne r0 r) as HNE. + rewrite assocmap_gso by auto. now apply H2. Qed. #[local] Hint Resolve regs_lessdef_add_match : htlproof. @@ -321,8 +359,8 @@ Ltac unfold_func H := end. Lemma init_reg_assoc_empty : - forall f l, - match_assocmaps f (Gible.init_regs nil l) (DHTL.init_regs nil l). + forall n m l, + match_assocmaps n m (Gible.init_regs nil l) (PMap.init false) (DHTL.init_regs nil l). Proof. induction l; simpl; constructor; intros. - rewrite Registers.Regmap.gi. unfold find_assocmap. @@ -332,6 +370,14 @@ Proof. - rewrite Registers.Regmap.gi. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gempty. constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. Qed. Lemma arr_lookup_some: @@ -553,7 +599,7 @@ Section CORRECTNESS. unfold Values.Val.shrx in *. destruct v0; try discriminate. destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate. - inversion H1. clear H1. + inversion H2. clear H2. assert (Int.unsigned n <= 30). { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate. rewrite Int.unsigned_repr in l by (simplify; lia). @@ -561,31 +607,31 @@ Section CORRECTNESS. apply Zlt_succ_le in l. auto. } - rewrite IntExtra.shrx_shrx_alt_equiv in H2 by auto. + rewrite IntExtra.shrx_shrx_alt_equiv in H3 by auto. unfold IntExtra.shrx_alt in *. destruct (zlt (Int.signed i) 0). - repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue; repeat (simplify; eval_correct_tac). - unfold valueToInt in *. inv INSTR. apply H in H4. rewrite H3 in H4. - inv H4. clear H5. + unfold valueToInt in *. inv INSTR. apply H in H5. rewrite H4 in H5. + inv H5. clear H6. unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify. rewrite Int.unsigned_repr in Heqb0. discriminate. simplify; lia. unfold ZToValue. rewrite Int.signed_repr by (simplify; lia). auto. rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia. - simplify. inv INSTR. clear H5. apply H in H4. rewrite H3 in H4. inv H4. auto. + simplify. inv INSTR. clear H6. apply H in H5. rewrite H4 in H5. inv H5. auto. - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue; repeat (simplify; eval_correct_tac). - inv INSTR. clear H5. apply H in H4. rewrite H3 in H4. - inv H4. + inv INSTR. clear H6. apply H in H5. rewrite H4 in H5. + inv H5. unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify. rewrite Int.unsigned_repr in Heqb0. lia. simplify; lia. unfold ZToValue. rewrite Int.signed_repr by (simplify; lia). auto. rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia. - simplify. inv INSTR. apply H in H4. unfold valueToInt in *. rewrite H3 in H4. inv H4. auto. + simplify. inv INSTR. apply H in H5. unfold valueToInt in *. rewrite H4 in H5. inv H5. auto. Qed. Lemma max_reg_function_use: @@ -888,16 +934,16 @@ Section CORRECTNESS. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_sub. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul'. - - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. do 2 econstructor; eauto. repeat econstructor. unfold binop_run. rewrite Heqb. auto. constructor; auto. - - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. do 2 econstructor; eauto. repeat econstructor. unfold binop_run. rewrite Heqb. auto. constructor; auto. - - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. do 2 econstructor; eauto. repeat econstructor. unfold binop_run. rewrite Heqb. auto. constructor; auto. - - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. do 2 econstructor; eauto. repeat econstructor. unfold binop_run. rewrite Heqb. auto. constructor; auto. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and. @@ -911,7 +957,7 @@ Section CORRECTNESS. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl'. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr'. - - inv H1. rewrite Heqv0 in HPLE. inv HPLE. + - inv H2. rewrite Heqv0 in HPLE. inv HPLE. assert (0 <= 31 <= Int.max_unsigned). { pose proof Int.two_wordsize_max_unsigned as Y. unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize in Y. lia. } @@ -919,17 +965,17 @@ Section CORRECTNESS. { unfold Int.ltu in Heqb. destruct_match; try discriminate. clear Heqs. rewrite Int.unsigned_repr in l by auto. lia. } rewrite IntExtra.shrx_shrx_alt_equiv by auto. - case_eq (Int.lt (asr # p) (ZToValue 0)); intros HLT. - + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = true). + case_eq (Int.lt (find_assocmap 32 (reg_enc p) asr) (ZToValue 0)); intros HLT. + + assert ((if zlt (Int.signed (valueToInt (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = true). { destruct_match; auto; unfold valueToInt in *. exfalso. - assert (Int.signed asr # p < 0 -> False) by auto. apply H2. unfold Int.lt in HLT. + assert (Int.signed (find_assocmap 32 (reg_enc p) asr) < 0 -> False) by auto. apply H3. unfold Int.lt in HLT. destruct_match; try discriminate. auto. } destruct_match; try discriminate. do 2 econstructor; eauto. repeat econstructor. now rewrite HLT. constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto. - + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = false). + + assert ((if zlt (Int.signed (valueToInt (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = false). { destruct_match; auto; unfold valueToInt in *. exfalso. - assert (Int.signed asr # p >= 0 -> False) by auto. apply H2. unfold Int.lt in HLT. + assert (Int.signed (find_assocmap 32 (reg_enc p) asr) >= 0 -> False) by auto. apply H3. unfold Int.lt in HLT. destruct_match; try discriminate. auto. } destruct_match; try discriminate. do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor. @@ -937,25 +983,25 @@ Section CORRECTNESS. constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru. - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru'. - - unfold translate_eff_addressing in H1. + - unfold translate_eff_addressing in H2. repeat (destruct_match; try discriminate); unfold boplitz in *; simplify; repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR)); try (apply H in HPLE); try (apply H in HPLE0). - + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. now apply eval_correct_add'. - + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. apply eval_correct_add; auto. apply eval_correct_add; auto. constructor; auto. - + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. apply eval_correct_add; try constructor; auto. apply eval_correct_mul; try constructor; auto. - + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. apply eval_correct_add; try constructor; auto. apply eval_correct_add; try constructor; auto. apply eval_correct_mul; try constructor; auto. - + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. assert (X: Archi.ptr64 = false) by auto. - rewrite X in H2. inv H2. + rewrite X in H3. inv H3. constructor. unfold valueToPtr. unfold Ptrofs.of_int. rewrite Int.unsigned_repr by auto with int_ptrofs. rewrite Ptrofs.repr_unsigned. apply Ptrofs.add_zero_l. @@ -966,7 +1012,7 @@ Section CORRECTNESS. exploit eval_cond_correct'; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto. - assert (HARCHI: Archi.ptr64 = false) by auto. - unfold Errors.bind in *. destruct_match; try discriminate; []. inv H1. + unfold Errors.bind in *. destruct_match; try discriminate; []. inv H2. remember (Op.eval_condition c (List.map (fun r : positive => rs !! r) l0) m). destruct o; cbn; symmetry in Heqo. + exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto. @@ -981,3 +1027,52 @@ Section CORRECTNESS. * econstructor. econstructor. econstructor. eauto. constructor. eauto. auto. constructor. * econstructor. econstructor. eapply erun_Vternary_false. eauto. constructor. eauto. auto. constructor. Qed. + +Ltac name_goal name := refine ?[name]. + +Ltac unfold_merge := + unfold merge_assocmap; repeat (rewrite AssocMapExt.merge_add_assoc); + try (rewrite AssocMapExt.merge_base_1). + + Lemma match_assocmaps_merge_empty: + forall n m rs ps ars, + match_assocmaps n m rs ps ars -> + match_assocmaps n m rs ps (AssocMapExt.merge value empty_assocmap ars). + Proof. + inversion 1; subst; clear H. + constructor; intros. + rewrite merge_get_default2 by auto. auto. + rewrite merge_get_default2 by auto. auto. + Qed. + + Opaque AssocMap.get. + Opaque AssocMap.set. + Opaque AssocMapExt.merge. + Opaque Verilog.merge_arr. + + Lemma match_assocmaps_ext : + forall n m rs ps ars1 ars2, + (forall x, Ple x n -> ars1 ! (reg_enc x) = ars2 ! (reg_enc x)) -> + (forall x, Ple x m -> ars1 ! (pred_enc x) = ars2 ! (pred_enc x)) -> + match_assocmaps n m rs ps ars1 -> + match_assocmaps n m rs ps ars2. + Proof. + intros * YFRL YFRL2 YMATCH. + inv YMATCH. constructor; intros x' YPLE. + unfold "#", AssocMapExt.get_default in *. + rewrite <- YFRL by auto. + eauto. + unfold "#", AssocMapExt.get_default. rewrite <- YFRL2 by auto. + eauto. + Qed. + + (* Lemma transl_iop_correct: *) + (* forall ge sp max_reg max_pred d d' curr_p next_p fin rtrn stack state rs ps m rs' ps' m' p op args dst asr arr asr' arr', *) + (* transf_instr fin rtrn stack state (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') -> *) + (* step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) -> *) + (* stmnt_runp tt asr arr d asr' arr' -> *) + (* match_assocmaps max_reg max_pred rs ps asr' -> *) + (* exists asr'', stmnt_runp tt asr arr d' asr'' arr' /\ match_assocmaps max_reg max_pred rs' ps' asr''. *) + (* Proof. *) + +End CORRECTNESS. diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 34e264d..2bf0419 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -686,6 +686,12 @@ Proof. apply IHexpr_runp2; eauto. econstructor. inv H2. simplify. assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia. eapply H5 in H2. apply H4 in H2. auto. auto. + - intros. econstructor. apply IHexpr_runp; eauto. constructor. inv H3. + intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. + eapply H1 in H0. eapply H5. instantiate (1:=1) in H0. lia. eauto. eauto. + inv H3. + intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. + unfold "#". unfold AssocMapExt.get_default. rewrite H5. auto. lia. Qed. #[local] Hint Resolve expr_runp_matches : mgen. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 56d7332..79ee723 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -441,7 +441,14 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack c vc -> expr_runp fext reg stack fs vf -> valueToBool vc = false -> - expr_runp fext reg stack (Vternary c ts fs) vf. + expr_runp fext reg stack (Vternary c ts fs) vf + | erun_Vrange : + forall fext reg stack r e1 e2 v vc vres b, + expr_runp fext reg stack e1 vc -> + reg#r = v -> + Int.testbit v (Int.unsigned vc) = b -> + vres = boolToValue b -> + expr_runp fext reg stack (Vrange r e1 e2) vres. #[export] Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) @@ -681,6 +688,15 @@ Fixpoint stmnt_to_list st := | Stmntnil => nil end. + Lemma int_inj : + forall x y, + Int.unsigned x = Int.unsigned y -> + x = y. + Proof. + intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned. + rewrite <- H. trivial. + Qed. + Lemma expr_runp_determinate : forall f e asr asa v, expr_runp f asr asa e v -> |