diff options
-rw-r--r-- | src/translation/Veriloggen.v | 34 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 186 | ||||
-rw-r--r-- | src/verilog/HTL.v | 4 | ||||
-rw-r--r-- | src/verilog/ValueInt.v | 2 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 10 |
5 files changed, 205 insertions, 31 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index b550ff9..f0ec576 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -19,32 +19,30 @@ From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST. -From coqup Require Import Verilog HTL Coquplib AssocMap Value. +From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt. -Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) := - match st with - | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls - | nil => nil - end. +Definition transl_list_fun (a : node * Verilog.stmnt) := + let (n, stmnt) := a in + (Vlit (posToValue n), stmnt). -Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := - match scldecl with - | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' - | nil => nil - end. +Definition transl_list st := map transl_list_fun st. -Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := - match arrdecl with - | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' - | nil => nil - end. +Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := + match a with (r, (io, VScalar sz)) => Vdeclaration (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)) => Vdeclaration (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.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) - (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint))) + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index ca4ecab..3052d03 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,9 +16,12 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Smallstep Linking. +From compcert Require Import Smallstep Linking Integers. From coqup Require HTL. -From coqup Require Import Coquplib Veriloggen Verilog. +From coqup Require Import Coquplib 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. @@ -52,6 +55,96 @@ Inductive match_states : HTL.state -> state -> Prop := forall m, match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). +Lemma Vlit_inj : + forall a b, Vlit a = Vlit b -> a = b. +Proof. inversion 1. trivial. Qed. + +Lemma posToValue_inj : + forall a b, + 0 <= Z.pos a <= Int.max_unsigned -> + 0 <= Z.pos b <= Int.max_unsigned -> + posToValue a = posToValue b -> + a = b. +Proof. + intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. + rewrite <- Int.unsigned_repr at 1; try assumption. + symmetry. + rewrite <- Int.unsigned_repr at 1; try assumption. + unfold posToValue in *. rewrite H1; auto. +Qed. + +Lemma valueToPos_inj : + forall a b, + 0 < Int.unsigned a -> + 0 < Int.unsigned b -> + valueToPos a = valueToPos b -> + a = b. +Proof. + intros. unfold valueToPos in *. + rewrite <- Int.repr_unsigned at 1. + rewrite <- Int.repr_unsigned. + apply Pos2Z.inj_iff in H1. + rewrite Z2Pos.id in H1; auto. + rewrite Z2Pos.id in H1; auto. + rewrite H1. auto. +Qed. + +Lemma transl_list_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) -> + (p1, a) = (p2, b). +Proof. + intros. unfold transl_list_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_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 p (map fst l). +Proof. + induction l. + - simplify. auto. + - intros. destruct a. simplify. destruct (peq p0 p); auto. + right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. + apply IHl; auto. +Qed. + +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)). +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. + contradiction. + apply H0; auto. auto. + right. apply transl_in; auto. +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)). +Proof. + induction l. + - intros. simpl. apply list_norepet_nil. + - destruct a. intros. simpl. apply list_norepet_cons. + inv H0. apply transl_notin. apply H. simplify; auto. + intros. apply H. destruct (peq p0 p); subst; simplify; auto. + assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. + simplify. inv H0. assumption. +Qed. + Section CORRECTNESS. Variable prog: HTL.program. @@ -59,6 +152,52 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. + Lemma transl_list_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_list l) (Some Vskip)) + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). + Proof. + induction l as [| a l IHl]. + - contradiction. + - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. + destruct a as [p' s']. simplify. + destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. + constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. + rewrite ASSOC. trivial. constructor. auto. + inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. + inv NOREP. eapply in_map with (f := fst) in INV. contradiction. + + eapply stmnt_runp_Vcase_nomatch. constructor. simplify. + unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. + trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. + apply BOUND. right. inv IN. inv H0; contradiction. eapply in_map with (f := fst) in H0. auto. + apply BOUND; auto. auto. + + eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. + trivial. assumption. + Qed. + + Lemma mis_stepp_decl : + forall l asr asa f, + mis_stepp f asr asa l asr asa. + Admitted. + Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog. @@ -69,10 +208,45 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. -(* induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. - - apply Smallstep.plus_one. econstructor. eassumption. trivial. - * econstructor. econstructor.*) - Admitted. + induction 1; intros R1 MSTATE; inv MSTATE. + - econstructor; split. apply Smallstep.plus_one. econstructor. + assumption. assumption. eassumption. trivial. + econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. + simpl. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite H. trivial. + + econstructor. simpl. auto. auto. + + eapply transl_list_correct. + assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_controllogic m))) + -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto. + admit. rewrite valueToPos_posToValue. trivial. admit. } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + econstructor. econstructor. + + eapply transl_list_correct. + assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_datapath m))) + -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto. + admit. rewrite valueToPos_posToValue. trivial. admit. } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. + constructor; assumption. + + - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. + constructor; assumption. + - econstructor; split. apply Smallstep.plus_one. constructor. + + constructor. constructor. + - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. + + apply match_state. assumption. + Admitted. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index df88f98..a7a6ecc 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -103,6 +103,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := basr2 basa2 nasr2 nasa2 asr' asa' f stval pstval, + asr!(mod_reset m) = Some (ZToValue 0) -> + asr!(mod_finish m) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> m.(mod_controllogic)!st = Some ctrl -> @@ -113,6 +115,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> + basr1!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> Verilog.stmnt_runp f (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index dff7b5c..aa99fbd 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -94,7 +94,7 @@ of [bool], so if they are in a condition, they will have to be converted before they can be used. *) Definition valueToBool (v : value) : bool := - if Z.eqb (uvalueToZ v) 0 then true else false. + if Z.eqb (uvalueToZ v) 0 then false else true. Definition boolToValue (b : bool) : value := natToValue (if b then 1 else 0). diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 3c1b36f..1513330 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -245,9 +245,6 @@ Definition program := AST.program fundef unit. Definition posToLit (p : positive) : expr := Vlit (posToValue p). -Coercion Vlit : value >-> expr. -Coercion Vvar : reg >-> expr. - Definition fext := assocmap. Definition fextclk := nat -> fext. @@ -533,7 +530,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> forall asr0 asa0 asr1 asa1 f c vc stt stf, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> valueToBool vc = false -> - stmnt_runp f asr0 asa0 stt asr1 asa1 -> + stmnt_runp f asr0 asa0 stf asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 | stmnt_runp_Vcase_nomatch: forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, @@ -716,6 +713,7 @@ Definition empty_stack (m : module) : assocmap_arr := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_reset)) = Some (ZToValue 0) -> asr!(m.(mod_finish)) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> @@ -746,7 +744,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) - (empty_stack m)). + asa). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := @@ -888,7 +886,7 @@ Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - invert H; invert H0; crush. - pose proof (mis_stepp_determinate H4 H13) + (*pose proof (mis_stepp_determinate H4 H13)*) admit. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. |