From 57350a8ca5579b65978d7a723a20915e763a2d0b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Mar 2021 21:12:15 +0000 Subject: Add RAM semantics to HTL and fix proof --- src/hls/HTL.v | 43 ++++++++++++++++++++++-- src/hls/HTLgenproof.v | 14 ++++---- src/hls/Memorygen.v | 91 ++++++++++++++++++++++++++++++++++++++++++++++----- src/hls/Veriloggen.v | 2 +- 4 files changed, 132 insertions(+), 18 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 1949785..b83d313 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -51,6 +51,14 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> Z.pos p0 <= Integers.Int.max_unsigned. +Record ram := mk_ram { + ram_mem: reg; + ram_addr: reg; + ram_wr_en: reg; + ram_d_in: reg; + ram_d_out: reg; +}. + Record module: Type := mkmodule { mod_params : list reg; @@ -67,7 +75,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); - mod_ram : option (reg * reg * reg * reg); + mod_ram : option ram; mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. @@ -112,12 +120,35 @@ Inductive state : Type := (m : module) (args : list value), state. +Inductive exec_ram: + Verilog.reg_associations -> Verilog.arr_associations -> + option ram -> + Verilog.reg_associations -> Verilog.arr_associations -> + Prop := +| exec_ram_Some_write: + forall ra ar ram d_in addr, + (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 1) -> + (Verilog.assoc_blocking ra)!(ram_d_in ram) = Some d_in -> + (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> + exec_ram ra ar (Some ram) ra + (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in) +| exec_ram_Some_load: + forall ra ar ram addr v_d_out, + (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) -> + (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> + Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem ram) (valueToNat addr) = Some v_d_out -> + exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar +| exec_ram_None: + forall r a, + exec_ram r a None r a. + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 + basr3 basa3 nasr3 nasa3 asr' asa' f pstval, asr!(mod_reset m) = Some (ZToValue 0) -> @@ -138,8 +169,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> - asr' = Verilog.merge_regs nasr2 basr2 -> - asa' = Verilog.merge_arrs nasa2 basa2 -> + exec_ram + (Verilog.mkassociations basr2 nasr2) + (Verilog.mkassociations basa2 nasa2) + (mod_ram m) + (Verilog.mkassociations basr3 nasr3) + (Verilog.mkassociations basa3 nasa3) -> + asr' = Verilog.merge_regs nasr3 basr3 -> + asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> Z.pos pstval <= Integers.Int.max_unsigned -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 59ff55b..e3b0147 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1030,6 +1030,7 @@ Section CORRECTNESS. Ltac tac0 := match goal with + | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge @@ -1701,7 +1702,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -1981,7 +1982,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2229,7 +2230,7 @@ Section CORRECTNESS. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2463,7 +2464,7 @@ Section CORRECTNESS. 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. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2480,7 +2481,7 @@ Section CORRECTNESS. 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. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2535,7 +2536,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. constructor. + constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. destruct wf as [HCTRL HDATA]. apply HCTRL. @@ -2564,6 +2565,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. constructor. constructor. constructor. constructor. constructor. + constructor. unfold state_st_wf in WF; big_tac; eauto. diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index a845435..6219127 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -32,6 +32,7 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. Require Import vericert.hls.HTL. Require Import vericert.hls.AssocMap. +Require Import vericert.hls.Array. Local Open Scope positive. @@ -66,6 +67,43 @@ Definition transf_maps (st addr d_in d_out wr: reg) end end. +Lemma transf_maps_wf : + forall st addr d_in d_out wr n d c n' d' c' i, + map_well_formed c /\ map_well_formed d -> + transf_maps st addr d_in d_out wr (n, d, c) i = (n', d', c') -> + map_well_formed c' /\ map_well_formed d'. +Proof. + unfold map_well_formed; simplify; + repeat destruct_match; + match goal with | H: (_, _, _) = (_, _, _) |- _ => inv H end; eauto; + simplify. + apply H2. + exploit list_in_map_inv; eauto; intros. + inv H0. destruct x. inv H3. simplify. + replace p with (fst (p, s)) by auto. + apply in_map. + apply PTree.elements_correct. + apply PTree.elements_complete in H4. + Admitted. + +Definition set_mod_datapath d c wf m := + mkmodule (mod_params m) + d + c + (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) + wf. + Lemma is_wf: forall A nc nd, @map_well_formed A nc /\ @map_well_formed A nd. @@ -98,7 +136,7 @@ Definition transf_module (m: module): module := (AssocMap.set d_in (None, VScalar 32) (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls))))) (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up m.(mod_stk_len)))%nat m.(mod_arrdecls)) - (Some (addr, d_in, d_out, wr_en)) + (Some (mk_ram (mod_stk m) addr wr_en d_in d_out)) (is_wf _ nc nd) end. @@ -116,11 +154,27 @@ Definition transf_fundef := transf_fundef transf_module. Definition transf_program (p : program) := transform_program transf_fundef p. +Inductive match_assocmaps : assocmap -> assocmap -> Prop := + match_assocmap: forall rs rs', + (forall r v, rs!r = Some v -> rs'!r = Some v) -> + match_assocmaps rs rs'. + +Inductive match_arrs : assocmap_arr -> assocmap_arr -> Prop := + match_assocmap_arr: forall ar ar', + (forall s arr arr', + ar!s = Some arr -> + ar'!s = Some arr' -> + forall addr, + array_get_error addr arr = array_get_error addr arr') -> + match_arrs ar ar'. + Inductive match_states : HTL.state -> HTL.state -> Prop := | match_state : - forall res m st asr asa, + forall res m st asr asr' asa asa' + (ASSOC: match_assocmaps asr asr') + (ARRS: match_arrs asa asa'), match_states (HTL.State res m st asr asa) - (HTL.State res (transf_module m) st asr asa) + (HTL.State res (transf_module m) st asr' asa') | match_returnstate : forall res v, match_states (HTL.Returnstate res v) (HTL.Returnstate res v) @@ -148,6 +202,27 @@ Section CORRECTNESS. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. + Lemma transf_maps_preserves_behaviour : + forall m m' s addr d_in d_out wr n n' t stk rs ar d' c' wf' i, + m' = set_mod_datapath d' c' wf' m -> + transf_maps m.(mod_st) addr d_in d_out wr (n, mod_datapath m, mod_controllogic m) i = (n', d', c') -> + step ge (State stk m s rs ar) t (State stk m s rs ar) -> + forall R1, + match_states (State stk m s rs ar) R1 -> + exists R2, step ge R1 t R2 /\ match_states (State stk m s rs ar) R2. + Proof. + Admitted. + + Lemma fold_transf_maps_preserves_behaviour : + forall m m' s addr d_in d_out wr n' t stk rs ar d' c' wf' l rs' ar', + fold_left (transf_maps m.(mod_st) addr d_in d_out wr) l + (max_pc_function m + 1, m.(mod_datapath), m.(mod_controllogic)) = (n', d', c') -> + m' = set_mod_datapath d' c' wf' m -> + step ge (State stk m s rs ar) t (State stk m s rs' ar') -> + exists R2, step ge (State stk m' s rs ar) t R2 /\ match_states (State stk m s rs' ar') R2. + Proof. + Admitted. + Theorem transf_step_correct: forall (S1 : state) t S2, step ge S1 t S2 -> @@ -155,14 +230,14 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step ge R1 t R2 /\ match_states S2 R2. Proof. + pose proof fold_transf_maps_preserves_behaviour. induction 1. - - intros. inv H11. - unfold transf_module. + - exploit fold_transf_maps_preserves_behaviour. intros. inv H13. inv ASSOC. inv ARRS. econstructor. econstructor. eapply Smallstep.plus_one. - econstructor. - simplify. - all: repeat destruct_match; try assumption; simplify. + econstructor; unfold transf_module; repeat destruct_match; try solve [crush]. + + simplify. + End CORRECTNESS. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index cf36d27..3defe9c 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -52,7 +52,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in match m.(HTL.mod_ram) with - | Some (addr, d_in, d_out, wr_en) => + | Some (mk_ram ram addr wr_en d_in d_out) => 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)))) -- cgit