From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/verilog/Array.v | 337 ---------------- src/verilog/AssocMap.v | 217 ----------- src/verilog/HTL.v | 171 --------- src/verilog/PrintHTL.ml | 81 ---- src/verilog/PrintVerilog.ml | 232 ----------- src/verilog/PrintVerilog.mli | 25 -- src/verilog/Value.v | 551 -------------------------- src/verilog/ValueInt.v | 167 -------- src/verilog/Verilog.v | 893 ------------------------------------------- 9 files changed, 2674 deletions(-) delete mode 100644 src/verilog/Array.v delete mode 100644 src/verilog/AssocMap.v delete mode 100644 src/verilog/HTL.v delete mode 100644 src/verilog/PrintHTL.ml delete mode 100644 src/verilog/PrintVerilog.ml delete mode 100644 src/verilog/PrintVerilog.mli delete mode 100644 src/verilog/Value.v delete mode 100644 src/verilog/ValueInt.v delete mode 100644 src/verilog/Verilog.v (limited to 'src/verilog') diff --git a/src/verilog/Array.v b/src/verilog/Array.v deleted file mode 100644 index fe0f6b2..0000000 --- a/src/verilog/Array.v +++ /dev/null @@ -1,337 +0,0 @@ -Set Implicit Arguments. - -Require Import Lia. -Require Import Vericertlib. -From Coq Require Import Lists.List Datatypes. - -Import ListNotations. - -Local Open Scope nat_scope. - -Record Array (A : Type) : Type := - mk_array - { arr_contents : list A - ; arr_length : nat - ; arr_wf : length arr_contents = arr_length - }. - -Definition make_array {A : Type} (l : list A) : Array A := - @mk_array A l (length l) eq_refl. - -Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A := - match i, l with - | _, nil => nil - | S n, h :: t => h :: list_set n x t - | O, h :: t => x :: t - end. - -Lemma list_set_spec1 {A : Type} : - forall l i (x : A), - i < length l -> nth_error (list_set i x l) i = Some x. -Proof. - induction l; intros; destruct i; crush; firstorder. -Qed. -Hint Resolve list_set_spec1 : array. - -Lemma list_set_spec2 {A : Type} : - forall l i (x : A) d, - i < length l -> nth i (list_set i x l) d = x. -Proof. - induction l; intros; destruct i; crush; firstorder. -Qed. -Hint Resolve list_set_spec2 : array. - -Lemma list_set_spec3 {A : Type} : - forall l i1 i2 (x : A), - i1 <> i2 -> - nth_error (list_set i1 x l) i2 = nth_error l i2. -Proof. - induction l; intros; destruct i1; destruct i2; crush; firstorder. -Qed. -Hint Resolve list_set_spec3 : array. - -Lemma array_set_wf {A : Type} : - forall l ln i (x : A), - length l = ln -> length (list_set i x l) = ln. -Proof. - induction l; intros; destruct i; auto. - - invert H; crush; auto. -Qed. - -Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := - let l := a.(arr_contents) in - let ln := a.(arr_length) in - let WF := a.(arr_wf) in - @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF). - -Lemma array_set_spec1 {A : Type} : - forall a i (x : A), - i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x. -Proof. - intros. - - rewrite <- a.(arr_wf) in H. - unfold array_set. crush. - eauto with array. -Qed. -Hint Resolve array_set_spec1 : array. - -Lemma array_set_spec2 {A : Type} : - forall a i (x : A) d, - i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x. -Proof. - intros. - - rewrite <- a.(arr_wf) in H. - unfold array_set. crush. - eauto with array. -Qed. -Hint Resolve array_set_spec2 : array. - -Lemma array_set_len {A : Type} : - forall a i (x : A), - a.(arr_length) = (array_set i x a).(arr_length). -Proof. - unfold array_set. crush. -Qed. - -Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := - nth_error a.(arr_contents) i. - -Lemma array_get_error_equal {A : Type} : - forall (a b : Array A) i, - a.(arr_contents) = b.(arr_contents) -> - array_get_error i a = array_get_error i b. -Proof. - unfold array_get_error. crush. -Qed. - -Lemma array_get_error_bound {A : Type} : - forall (a : Array A) i, - i < a.(arr_length) -> exists x, array_get_error i a = Some x. -Proof. - intros. - - rewrite <- a.(arr_wf) in H. - assert (~ length (arr_contents a) <= i) by lia. - - pose proof (nth_error_None a.(arr_contents) i). - apply not_iff_compat in H1. - apply <- H1 in H0. - - destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto. -Qed. - -Lemma array_get_error_set_bound {A : Type} : - forall (a : Array A) i x, - i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x. -Proof. - intros. - - unfold array_get_error. - eauto with array. -Qed. - -Lemma array_gso {A : Type} : - forall (a : Array A) i1 i2 x, - i1 <> i2 -> - array_get_error i2 (array_set i1 x a) = array_get_error i2 a. -Proof. - intros. - - unfold array_get_error. - unfold array_set. - crush. - eauto with array. -Qed. - -Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A := - nth i a.(arr_contents) x. - -Lemma array_get_set_bound {A : Type} : - forall (a : Array A) i x d, - i < a.(arr_length) -> array_get i d (array_set i x a) = x. -Proof. - intros. - - unfold array_get. - eauto with array. -Qed. - -Lemma array_get_get_error {A : Type} : - forall (a : Array A) i x d, - array_get_error i a = Some x -> - array_get i d a = x. -Proof. - intros. - unfold array_get. - unfold array_get_error in H. - auto using nth_error_nth. -Qed. - -(** Tail recursive version of standard library function. *) -Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := - match n with - | O => acc - | S n => list_repeat' (a::acc) a n - end. - -Lemma list_repeat'_len {A : Type} : forall (a : A) n l, - length (list_repeat' l a n) = (n + Datatypes.length l)%nat. -Proof. - induction n; intros; crush; try reflexivity. - - specialize (IHn (a :: l)). - rewrite IHn. - crush. -Qed. - -Lemma list_repeat'_app {A : Type} : forall (a : A) n l, - list_repeat' l a n = list_repeat' [] a n ++ l. -Proof. - induction n; intros; crush; try reflexivity. - - pose proof IHn. - specialize (H (a :: l)). - rewrite H. clear H. - specialize (IHn (a :: nil)). - rewrite IHn. clear IHn. - remember (list_repeat' [] a n) as l0. - - rewrite <- app_assoc. - f_equal. -Qed. - -Lemma list_repeat'_head_tail {A : Type} : forall n (a : A), - a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]. -Proof. - induction n; intros; crush; try reflexivity. - rewrite list_repeat'_app. - - replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]). - 2: { rewrite app_comm_cons. rewrite IHn; auto. - rewrite app_assoc. reflexivity. } - rewrite app_assoc. reflexivity. -Qed. - -Lemma list_repeat'_cons {A : Type} : forall (a : A) n, - list_repeat' [a] a n = a :: list_repeat' [] a n. -Proof. - intros. - - rewrite list_repeat'_head_tail; auto. - apply list_repeat'_app. -Qed. - -Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil. - -Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n. -Proof. - intros. - unfold list_repeat. - rewrite list_repeat'_len. - crush. -Qed. - -Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a', - (forall x x' : A, {x' = x} + {~ x' = x}) -> - In a' (list_repeat a n) -> a' = a. -Proof. - induction n; intros; crush. - - unfold list_repeat in *. - crush. - - rewrite list_repeat'_app in H. - pose proof (X a a'). - destruct H0; auto. - - (* This is actually a degenerate case, not an unprovable goal. *) - pose proof (in_app_or (list_repeat' [] a n) ([a])). - apply H0 in H. invert H. - - - eapply IHn in X; eassumption. - - invert H1; contradiction. -Qed. - -Lemma list_repeat_head_tail {A : Type} : forall n (a : A), - a :: list_repeat a n = list_repeat a n ++ [a]. -Proof. - unfold list_repeat. apply list_repeat'_head_tail. -Qed. - -Lemma list_repeat_cons {A : Type} : forall n (a : A), - list_repeat a (S n) = a :: list_repeat a n. -Proof. - intros. - - unfold list_repeat. - apply list_repeat'_cons. -Qed. - -Lemma list_repeat_lookup {A : Type} : - forall n i (a : A), - i < n -> - nth_error (list_repeat a n) i = Some a. -Proof. - induction n; intros. - - destruct i; crush. - - rewrite list_repeat_cons. - destruct i; crush; firstorder. -Qed. - -Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). - -Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n. -Proof. - unfold list_repeat. crush. apply list_repeat_len. -Qed. - -Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := - match x, y with - | a :: t, b :: t' => f a b :: list_combine f t t' - | _, _ => nil - end. - -Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B), - length (list_combine f x y) = min (length x) (length y). -Proof. - induction x; intros; crush. - - destruct y; crush; auto. -Qed. - -Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := - make_array (list_combine f x.(arr_contents) y.(arr_contents)). - -Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C), - x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length). -Proof. - intros. - - unfold combine. - unfold make_array. - crush. - - rewrite <- (arr_wf x) in *. - rewrite <- (arr_wf y) in *. - - destruct (arr_contents x); destruct (arr_contents y); crush. - rewrite list_combine_length. - destruct (Min.min_dec (length l) (length l0)); congruence. -Qed. - -Ltac array := - try match goal with - | [ |- context[arr_length (combine _ _ _)] ] => - rewrite combine_length - | [ |- context[length (list_repeat _ _)] ] => - rewrite list_repeat_len - | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] => - unfold array_get_error, arr_repeat - | |- context[nth_error (list_repeat ?x _) _ = Some ?x] => - apply list_repeat_lookup - end. diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v deleted file mode 100644 index 8d8788a..0000000 --- a/src/verilog/AssocMap.v +++ /dev/null @@ -1,217 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * 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 . - *) - -From vericert Require Import Vericertlib ValueInt. -From compcert Require Import Maps. - -Definition reg := positive. - -Module AssocMap := Maps.PTree. - -Module AssocMapExt. - Import AssocMap. - - Hint Resolve elements_correct elements_complete - elements_keys_norepet : assocmap. - Hint Resolve gso gss : assocmap. - - Section Operations. - - Variable A : Type. - - Definition get_default (a : A) (k : reg) (m : t A) : A := - match get k m with - | None => a - | Some v => v - end. - - Fixpoint merge (m1 m2 : t A) : t A := - match m1, m2 with - | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2) - | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2) - | Leaf, _ => m2 - | _, _ => m1 - end. - - Lemma merge_base_1 : - forall am, - merge (empty A) am = am. - Proof. auto. Qed. - Hint Resolve merge_base_1 : assocmap. - - Lemma merge_base_2 : - forall am, - merge am (empty A) = am. - Proof. - unfold merge. - destruct am; trivial. - destruct o; trivial. - Qed. - Hint Resolve merge_base_2 : assocmap. - - Lemma merge_add_assoc : - forall r am am' v, - merge (set r v am) am' = set r v (merge am am'). - Proof. - induction r; intros; destruct am; destruct am'; try (destruct o); simpl; - try rewrite IHr; try reflexivity. - Qed. - Hint Resolve merge_add_assoc : assocmap. - - Lemma merge_correct_1 : - forall am bm k v, - get k am = Some v -> - get k (merge am bm) = Some v. - Proof. - induction am; intros; destruct k; destruct bm; try (destruct o); simpl; - try rewrite gempty in H; try discriminate; try assumption; auto. - Qed. - Hint Resolve merge_correct_1 : assocmap. - - Lemma merge_correct_2 : - forall am bm k v, - get k am = None -> - get k bm = Some v -> - get k (merge am bm) = Some v. - Proof. - induction am; intros; destruct k; destruct bm; try (destruct o); simpl; - try rewrite gempty in H; try discriminate; try assumption; auto. - Qed. - Hint Resolve merge_correct_2 : assocmap. - - Definition merge_fold (am bm : t A) : t A := - fold_right (fun p a => set (fst p) (snd p) a) bm (elements am). - - Lemma add_assoc : - forall (k : elt) (v : A) l bm, - List.In (k, v) l -> - list_norepet (List.map fst l) -> - @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. - Proof. - induction l; intros. - - contradiction. - - destruct a as [k' v']. - destruct (peq k k'). - + inversion H. inversion H1. inversion H0. subst. - simpl. auto with assocmap. - - inversion H0; subst. apply in_map with (f:=fst) in H1. contradiction. - - + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption. - apply IHl. contradiction. contradiction. - simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. - Qed. - Hint Resolve add_assoc : assocmap. - - Lemma not_in_assoc : - forall k v l bm, - ~ List.In k (List.map (@fst elt A) l) -> - @get A k bm = Some v -> - get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. - Proof. - induction l; intros. - - assumption. - - destruct a as [k' v']. - destruct (peq k k'); subst; - simpl in *; apply Decidable.not_or in H; destruct H. contradiction. - rewrite AssocMap.gso; auto. - Qed. - Hint Resolve not_in_assoc : assocmap. - - Lemma elements_iff : - forall am k, - (exists v, get k am = Some v) <-> - List.In k (List.map (@fst _ A) (elements am)). - Proof. - split; intros. - destruct H. apply elements_correct in H. apply in_map with (f := fst) in H. apply H. - apply list_in_map_inv in H. destruct H. destruct H. subst. - exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing. - rewrite H in H0; assumption. - Qed. - Hint Resolve elements_iff : assocmap. - - Lemma elements_correct' : - forall am k, - ~ (exists v, get k am = Some v) <-> - ~ List.In k (List.map (@fst _ A) (elements am)). - Proof. auto using not_iff_compat with assocmap. Qed. - Hint Resolve elements_correct' : assocmap. - - Lemma elements_correct_none : - forall am k, - get k am = None -> - ~ List.In k (List.map (@fst _ A) (elements am)). - Proof. - intros. apply elements_correct'. unfold not. intros. - destruct H0. rewrite H in H0. discriminate. - Qed. - Hint Resolve elements_correct_none : assocmap. - - Lemma merge_fold_add : - forall k v am bm, - am ! k = Some v -> - (merge_fold am bm) ! k = Some v. - Proof. unfold merge_fold; auto with assocmap. Qed. - Hint Resolve merge_fold_add : assocmap. - - Lemma merge_fold_not_in : - forall k v am bm, - get k am = None -> - get k bm = Some v -> - get k (merge_fold am bm) = Some v. - Proof. intros. apply not_in_assoc; auto with assocmap. Qed. - Hint Resolve merge_fold_not_in : assocmap. - - Lemma merge_fold_base : - forall am, - merge_fold (empty A) am = am. - Proof. auto. Qed. - Hint Resolve merge_fold_base : assocmap. - - End Operations. - -End AssocMapExt. -Import AssocMapExt. - -Definition assocmap := AssocMap.t value. - -Definition find_assocmap (n : nat) : reg -> assocmap -> value := - get_default value (ZToValue 0). - -Definition empty_assocmap : assocmap := AssocMap.empty value. - -Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. - -Ltac unfold_merge := - unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); - rewrite AssocMapExt.merge_base_1. - -Declare Scope assocmap. -Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. -Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. -Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. -Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. -Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. - -Local Open Scope assocmap. -Lemma find_get_assocmap : - forall assoc r v, - assoc ! r = Some v -> - assoc # r = v. -Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v deleted file mode 100644 index 620ef14..0000000 --- a/src/verilog/HTL.v +++ /dev/null @@ -1,171 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * 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 . - *) - -From Coq Require Import FSets.FMapPositive. -From vericert Require Import Vericertlib ValueInt AssocMap Array. -From vericert Require Verilog. -From compcert Require Events Globalenvs Smallstep Integers Values. -From compcert Require Import Maps. - -(** The purpose of the hardware transfer language (HTL) is to create a more -hardware-like layout that is still similar to the register transfer language -(RTL) that it came from. The main change is that function calls become module -instantiations and that we now describe a state machine instead of a -control-flow graph. *) - -Local Open Scope assocmap. - -Definition reg := positive. -Definition node := positive. - -Definition datapath := PTree.t Verilog.stmnt. -Definition controllogic := PTree.t Verilog.stmnt. - -Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := - forall p0 : positive, - In p0 (map fst (Maps.PTree.elements m)) -> - Z.pos p0 <= Integers.Int.max_unsigned. - -Record module: Type := - mkmodule { - mod_params : list reg; - mod_datapath : datapath; - mod_controllogic : controllogic; - mod_entrypoint : node; - mod_st : reg; - mod_stk : reg; - mod_stk_len : nat; - mod_finish : reg; - mod_return : reg; - mod_start : reg; - mod_reset : reg; - mod_clk : reg; - mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); - mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); - mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); - }. - -Definition fundef := AST.fundef module. - -Definition program := AST.program fundef unit. - -Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := - match rl, vl with - | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl') - | _, _ => empty_assocmap - end. - -Definition empty_stack (m : module) : Verilog.assocmap_arr := - (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). - -(** * Operational Semantics *) - -Definition genv := Globalenvs.Genv.t fundef unit. - -Inductive stackframe : Type := - Stackframe : - forall (res : reg) - (m : module) - (pc : node) - (reg_assoc : Verilog.assocmap_reg) - (arr_assoc : Verilog.assocmap_arr), - stackframe. - -Inductive state : Type := -| State : - forall (stack : list stackframe) - (m : module) - (st : node) - (reg_assoc : Verilog.assocmap_reg) - (arr_assoc : Verilog.assocmap_arr), state -| Returnstate : - forall (res : list stackframe) - (v : value), state -| Callstate : - forall (stack : list stackframe) - (m : module) - (args : list value), state. - -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 - asr' asa' - f pstval, - asr!(mod_reset m) = Some (ZToValue 0) -> - asr!(mod_finish m) = Some (ZToValue 0) -> - asr!(m.(mod_st)) = Some (posToValue st) -> - m.(mod_controllogic)!st = Some ctrl -> - m.(mod_datapath)!st = Some data -> - Verilog.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 - (Verilog.mkassociations basr1 nasr1) - (Verilog.mkassociations basa1 nasa1) - data - (Verilog.mkassociations basr2 nasr2) - (Verilog.mkassociations basa2 nasa2) -> - asr' = Verilog.merge_regs nasr2 basr2 -> - asa' = Verilog.merge_arrs nasa2 basa2 -> - 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') -| step_finish : - forall g m st asr asa retval sf, - asr!(m.(mod_finish)) = Some (ZToValue 1) -> - asr!(m.(mod_return)) = Some retval -> - step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) -| step_call : - forall g m args res, - step g (Callstate res m args) Events.E0 - (State res m m.(mod_entrypoint) - (AssocMap.set (mod_reset m) (ZToValue 0) - (AssocMap.set (mod_finish m) (ZToValue 0) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))))) - (empty_stack m)) -| step_return : - forall g m asr asa i r sf pc mst, - 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) asa). -Hint Constructors step : htl. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b m0 m, - let ge := Globalenvs.Genv.globalenv p in - Globalenvs.Genv.init_mem p = Some m0 -> - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> - initial_state p (Callstate nil m nil). - -Inductive final_state : state -> Integers.int -> Prop := -| final_state_intro : forall retval retvali, - retvali = valueToInt retval -> - final_state (Returnstate nil retval) retvali. - -Definition semantics (m : program) := - Smallstep.Semantics step (initial_state m) final_state - (Globalenvs.Genv.globalenv m). diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml deleted file mode 100644 index 44f8b01..0000000 --- a/src/verilog/PrintHTL.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* -*- mode: tuareg -*- - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -open Value -open Datatypes -open Camlcoq -open AST -open Clflags -open Printf -open Maps -open AST -open HTL -open PrintAST -open PrintVerilog -open VericertClflags - -let pstr pp = fprintf pp "%s" - -let reg pp r = - fprintf pp "x%d" (P.to_int r) - -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl - -let print_instruction pp (pc, i) = - fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) - -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 " }\n\n controllogic {\n"; - List.iter (print_instruction pp) controllogic; - fprintf pp " }\n}\n\n" - -let print_globdef pp (id, gd) = - match gd with - | Gfun(Internal f) -> print_module pp id f - | _ -> () - -let print_program pp prog = - List.iter (print_globdef pp) prog.prog_defs - -let destination : string option ref = ref None - -let print_if prog = - match !destination with - | None -> () - | Some f -> - let oc = open_out f in - print_program oc prog; - close_out oc diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml deleted file mode 100644 index 0f64066..0000000 --- a/src/verilog/PrintVerilog.ml +++ /dev/null @@ -1,232 +0,0 @@ -(* -*- mode: tuareg -*- - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -open Verilog -open ValueInt -open Datatypes - -open Camlcoq -open AST -open Clflags - -open Printf - -open VericertClflags - -let concat = String.concat "" - -let indent i = String.make (2 * i) ' ' - -let fold_map f s = List.map f s |> concat - -let pstr pp = fprintf pp "%s" - -let pprint_binop l r = - let unsigned op = sprintf "{%s %s %s}" l op r in - let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in - function - | Vadd -> unsigned "+" - | Vsub -> unsigned "-" - | Vmul -> unsigned "*" - | Vdiv -> signed "/" - | Vdivu -> unsigned "/" - | Vmod -> signed "%" - | Vmodu -> unsigned "%" - | Vlt -> signed "<" - | Vltu -> unsigned "<" - | Vgt -> signed ">" - | Vgtu -> unsigned ">" - | Vle -> signed "<=" - | Vleu -> unsigned "<=" - | Vge -> signed ">=" - | Vgeu -> unsigned ">=" - | Veq -> unsigned "==" - | Vne -> unsigned "!=" - | Vand -> unsigned "&" - | Vor -> unsigned "|" - | Vxor -> unsigned "^" - | Vshl -> unsigned "<<" - | Vshr -> signed ">>>" - | Vshru -> unsigned ">>" - -let unop = function - | Vneg -> " ~ " - | Vnot -> " ! " - -let register a = sprintf "reg_%d" (P.to_int a) - -(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) - -let literal l = sprintf "32'd%ld" (camlint_of_coqint l) - -let rec pprint_expr = function - | Vlit l -> literal l - | Vvar s -> register s - | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] - | Vinputvar s -> register s - | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] - | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op] - | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] - -let rec pprint_stmnt i = - let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s; - indent (i + 1); "end\n" - ] - in function - | Vskip -> concat [indent i; ";\n"] - | Vseq (s1, s2) -> concat [ pprint_stmnt i s1; pprint_stmnt i s2] - | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ") begin\n"; - pprint_stmnt (i + 1) st; indent i; "end else begin\n"; - pprint_stmnt (i + 1) sf; - indent i; "end\n" - ] - | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case es; indent (i+1); "default:;\n"; - indent i; "endcase\n" - ] - | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] - | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] - -let rec pprint_edge = function - | Vposedge r -> concat ["posedge "; register r] - | Vnegedge r -> concat ["negedge "; register r] - | Valledge -> "*" - | Voredge (e1, e2) -> concat [pprint_edge e1; " or "; pprint_edge e2] - -let pprint_edge_top i = function - | Vposedge r -> concat ["@(posedge "; register r; ")"] - | Vnegedge r -> concat ["@(negedge "; register r; ")"] - | Valledge -> "@*" - | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] - -let declare t = - function (r, sz) -> - concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; - register r; ";\n" ] - -let declarearr t = - function (r, sz, ln) -> - concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; - register r; - " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] - -let print_io = function - | Some Vinput -> "input" - | Some Voutput -> "output reg" - | Some Vinout -> "inout" - | None -> "reg" - -let decl i = function - | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] - | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] - -(* TODO Fix always blocks, as they currently always print the same. *) -let pprint_module_item i = function - | Vdeclaration d -> decl i d - | Valways (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] - | Valways_ff (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] - | Valways_comb (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] - -let rec intersperse c = function - | [] -> [] - | [x] -> [x] - | x :: xs -> x :: c :: intersperse c xs - -let make_io i io r = concat [indent i; io; " "; register r; ";\n"] - -let compose f g x = g x |> f - -let testbench = "module testbench; - reg start, reset, clk; - wire finish; - wire [31:0] return_val; - - main m(start, reset, clk, finish, return_val); - - initial begin - clk = 0; - start = 0; - reset = 0; - @(posedge clk) reset = 1; - @(posedge clk) reset = 0; - end - - always #5 clk = ~clk; - - always @(posedge clk) begin - if (finish == 1) begin - $display(\"finished: %d\", return_val); - $finish; - end - end -endmodule -" - -let debug_always i clk state = concat [ - indent i; "reg [31:0] count;\n"; - indent i; "initial count = 0;\n"; - indent i; "always @(posedge " ^ register clk ^ ") begin\n"; - indent (i+1); "if(count[0:0] == 10'd0) begin\n"; - indent (i+2); "$display(\"Cycle count %d\", count);\n"; - indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n"; - indent (i+1); "end\n"; - indent (i+1); "count <= count + 1;\n"; - indent i; "end\n" - ] - -let print_initial i n stk = concat [ - indent i; "integer i;\n"; - indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n"; - indent (i+1); register stk; "[i] = 0;\n" - ] - -let pprint_module debug i n m = - if (extern_atom n) = "main" then - let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in - let outputs = [m.mod_finish; m.mod_return] in - concat [ indent i; "module "; (extern_atom n); - "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; - fold_map (pprint_module_item (i+1)) m.mod_body; - if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; - if debug then debug_always i m.mod_clk m.mod_st else ""; - indent i; "endmodule\n\n" - ] - else "" - -let print_result pp lst = - let rec print_result_in pp = function - | [] -> fprintf pp "]\n" - | (r, v) :: ls -> - fprintf pp "%s -> %s; " (register r) (literal v); - print_result_in pp ls in - fprintf pp "[ "; - print_result_in pp lst - -let print_value pp v = fprintf pp "%s" (literal v) - -let print_globdef debug pp (id, gd) = - match gd with - | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f) - | _ -> () - -let print_program debug pp prog = - List.iter (print_globdef debug pp) prog.prog_defs; - pstr pp testbench diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli deleted file mode 100644 index 6a15ee9..0000000 --- a/src/verilog/PrintVerilog.mli +++ /dev/null @@ -1,25 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -val pprint_stmnt : int -> Verilog.stmnt -> string - -val print_value : out_channel -> ValueInt.value -> unit - -val print_program : bool -> out_channel -> Verilog.program -> unit - -val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit diff --git a/src/verilog/Value.v b/src/verilog/Value.v deleted file mode 100644 index d6a3d8b..0000000 --- a/src/verilog/Value.v +++ /dev/null @@ -1,551 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * 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 . - *) - -(* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. -From compcert Require Import lib.Integers common.Values. -From vericert Require Import Vericertlib. -(* end hide *) - -(** * Value - -A [value] is a bitvector with a specific size. We are using the implementation -of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. -However, we need to wrap it with an [Inductive] so that we can specify and match -on the size of the [value]. This is necessary so that we can easily store -[value]s of different sizes in a list or in a map. - -Using the default [word], this would not be possible, as the size is part of the type. *) - -Record value : Type := - mkvalue { - vsize: nat; - vword: word vsize - }. - -(** ** Value conversions - -Various conversions to different number types such as [N], [Z], [positive] and -[int], where the last one is a theory of integers of powers of 2 in CompCert. *) - -Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. - -Definition valueToWord : forall v : value, word (vsize v) := vword. - -Definition valueToNat (v :value) : nat := - wordToNat (vword v). - -Definition natToValue sz (n : nat) : value := - mkvalue sz (natToWord sz n). - -Definition valueToN (v : value) : N := - wordToN (vword v). - -Definition NToValue sz (n : N) : value := - mkvalue sz (NToWord sz n). - -Definition ZToValue (s : nat) (z : Z) : value := - mkvalue s (ZToWord s z). - -Definition valueToZ (v : value) : Z := - wordToZ (vword v). - -Definition uvalueToZ (v : value) : Z := - uwordToZ (vword v). - -Definition posToValue sz (p : positive) : value := - ZToValue sz (Zpos p). - -Definition posToValueAuto (p : positive) : value := - let size := Pos.to_nat (Pos.size p) in - ZToValue size (Zpos p). - -Definition valueToPos (v : value) : positive := - Z.to_pos (uvalueToZ v). - -Definition intToValue (i : Integers.int) : value := - ZToValue Int.wordsize (Int.unsigned i). - -Definition valueToInt (i : value) : Integers.int := - Int.repr (uvalueToZ i). - -Definition ptrToValue (i : Integers.ptrofs) : value := - ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). - -Definition valueToPtr (i : value) : Integers.ptrofs := - Ptrofs.repr (uvalueToZ i). - -Definition valToValue (v : Values.val) : option value := - match v with - | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z - then Some (ptrToValue off) - else None - | Values.Vundef => Some (ZToValue 32 0%Z) - | _ => None - end. - -(** Convert a [value] to a [bool], so that choices can be made based on the -result. This is also because comparison operators will give back [value] instead -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 := - negb (weqb (@wzero (vsize v)) (vword v)). - -Definition boolToValue (sz : nat) (b : bool) : value := - natToValue sz (if b then 1 else 0). - -(** ** Arithmetic operations *) - -Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -intros; subst; assumption. Defined. - -Lemma unify_word_unfold : - forall sz w, - unify_word sz sz w eq_refl = w. -Proof. auto. Qed. - -Definition value_eq_size: - forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. -Proof. - intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?. - left; apply Nat.eqb_eq in Heqb; assumption. - right; trivial. -Defined. - -Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) - (EQ : vsize v1 = vsize v2) : A := - let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in - f (vword v1) w2. - -Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) - : option A := - match value_eq_size v1 v2 with - | left EQ => - Some (map_any v1 v2 f EQ) - | _ => None - end. - -Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value := - mkvalue (vsize v) (f (vsize v) (vword v)). - -Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) - (EQ : (vsize v1 = vsize v2)) : value := - let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in - mkvalue (vsize v1) (f (vsize v1) (vword v1) w2). - -Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) - : option value := - match value_eq_size v1 v2 with - | left EQ => Some (map_word2 f v1 v2 EQ) - | _ => None - end. - -Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) - : option value := - match value_eq_size v1 v2 with - | left EQ => Some (f EQ) - | _ => None - end. - -Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y. -Proof. - split; intros. - subst. reflexivity. inversion H. apply existT_wordToZ in H1. - apply wordToZ_inj. assumption. -Qed. - -Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y. -Proof. apply eqvalue. Qed. - -Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y. -Proof. split; intros; intuition. apply H. apply eqvalue. assumption. - apply H. rewrite H0. trivial. -Qed. - -Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. -Proof. apply nevalue. Qed. - -(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz) - : option (word finalsz) := - match Nat.eqb initsz finalsz return option (word finalsz) with - | true => Some _ - | false => None - end.*) - -Definition valueeq (sz : nat) (x y : word sz) : - {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} := - match weq x y with - | left eq => left (eqvaluef x y eq) - | right ne => right (nevaluef x y ne) - end. - -Definition valueeqb (x y : value) : bool := - match value_eq_size x y with - | left EQ => - weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ) - | right _ => false - end. - -Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2). - -Theorem value_projZ_eqb_true : - forall v1 v2, - v1 = v2 -> value_projZ_eqb v1 v2 = true. -Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed. - -Theorem valueeqb_true_iff : - forall v1 v2, - valueeqb v1 v2 = true <-> v1 = v2. -Proof. - split; intros. - unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. - - destruct v1, v2. simpl in H. -Abort. - -Definition value_int_eqb (v : value) (i : int) : bool := - Z.eqb (valueToZ v) (Int.unsigned i). - -(** Arithmetic operations over [value], interpreting them as signed or unsigned -depending on the operation. - -The arithmetic operations over [word] are over [N] by default, however, can also -be called over [Z] explicitly, which is where the bits are interpreted in a -signed manner. *) - -Definition vplus v1 v2 := map_word2 wplus v1 v2. -Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2. -Definition vminus v1 v2 := map_word2 wminus v1 v2. -Definition vmul v1 v2 := map_word2 wmult v1 v2. -Definition vdiv v1 v2 := map_word2 wdiv v1 v2. -Definition vmod v1 v2 := map_word2 wmod v1 v2. - -Definition vmuls v1 v2 := map_word2 wmultZ v1 v2. -Definition vdivs v1 v2 := map_word2 wdivZ v1 v2. -Definition vmods v1 v2 := map_word2 wremZ v1 v2. - -(** ** Bitwise operations - -Bitwise operations over [value], which is independent of whether the number is -signed or unsigned. *) - -Definition vnot v := map_word wnot v. -Definition vneg v := map_word wneg v. -Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)). -Definition vor v1 v2 := map_word2 wor v1 v2. -Definition vand v1 v2 := map_word2 wand v1 v2. -Definition vxor v1 v2 := map_word2 wxor v1 v2. - -(** ** Comparison operators - -Comparison operators that return a bool, there should probably be an equivalent -which returns another number, however I might just add that as an explicit -conversion. *) - -Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)). -Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ). - -Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ). -Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ). - -Definition vltb v1 v2 := map_any v1 v2 wltb. -Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)). -Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ). -Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ). - -Definition vltsb v1 v2 := map_any v1 v2 wsltb. -Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)). -Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ). -Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ). - -Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ). -Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ). -Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ). -Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ). - -Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ). -Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ). -Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ). -Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ). - -(** ** Shift operators - -Shift operators on values. *) - -Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) := - f w1 (wordToNat w2). - -Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. -Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. - -Module HexNotationValue. - Export HexNotation. - Import WordScope. - - Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). - -End HexNotationValue. - -Inductive val_value_lessdef: val -> value -> Prop := -| val_value_lessdef_int: - forall i v', - i = valueToInt v' -> - val_value_lessdef (Vint i) v' -| val_value_lessdef_ptr: - forall b off v', - off = valueToPtr v' -> - (Z.modulo (uvalueToZ v') 4) = 0%Z -> - val_value_lessdef (Vptr b off) v' -| lessdef_undef: forall v, val_value_lessdef Vundef v. - -Inductive opt_val_value_lessdef: option val -> value -> Prop := -| opt_lessdef_some: - forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' -| opt_lessdef_none: forall v, opt_val_value_lessdef None v. - -Lemma valueToZ_ZToValue : - forall n z, - (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> - valueToZ (ZToValue (S n) z) = z. -Proof. - unfold valueToZ, ZToValue. simpl. - auto using wordToZ_ZToWord. -Qed. - -Lemma uvalueToZ_ZToValue : - forall n z, - (0 <= z < 2 ^ Z.of_nat n)%Z -> - uvalueToZ (ZToValue n z) = z. -Proof. - unfold uvalueToZ, ZToValue. simpl. - auto using uwordToZ_ZToWord. -Qed. - -Lemma uvalueToZ_ZToValue_full : - forall sz : nat, - (0 < sz)%nat -> - forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z. -Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed. - -Lemma ZToValue_uvalueToZ : - forall v, - ZToValue (vsize v) (uvalueToZ v) = v. -Proof. - intros. - unfold ZToValue, uvalueToZ. - rewrite ZToWord_uwordToZ. destruct v; auto. -Qed. - -Lemma valueToPos_posToValueAuto : - forall p, valueToPos (posToValueAuto p) = p. -Proof. - intros. unfold valueToPos, posToValueAuto. - rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. - split. apply Zle_0_pos. - - assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. - inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. - simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. -Qed. - -Lemma valueToPos_posToValue : - forall p, valueToPos (posToValueAuto p) = p. -Proof. - intros. unfold valueToPos, posToValueAuto. - rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. - split. apply Zle_0_pos. - - assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. - inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. - simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. -Qed. - -Lemma valueToInt_intToValue : - forall v, - valueToInt (intToValue v) = v. -Proof. - intros. - unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned. - split. apply Int.unsigned_range_2. - assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2. - apply Z.lt_le_pred in H. apply H. -Qed. - -Lemma valueToPtr_ptrToValue : - forall v, - valueToPtr (ptrToValue v) = v. -Proof. - intros. - unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. - split. apply Ptrofs.unsigned_range_2. - assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. - apply Z.lt_le_pred in H. apply H. -Qed. - -Lemma intToValue_valueToInt : - forall v, - vsize v = 32%nat -> - intToValue (valueToInt v) = v. -Proof. - intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. - unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. - pose proof (uwordToZ_bound (vword v)). - rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. - rewrite <- H. rewrite two_power_nat_equiv. apply H0. -Qed. - -Lemma ptrToValue_valueToPtr : - forall v, - vsize v = 32%nat -> - ptrToValue (valueToPtr v) = v. -Proof. - intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. - unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. - pose proof (uwordToZ_bound (vword v)). - rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. - rewrite <- H. rewrite two_power_nat_equiv. apply H0. -Qed. - -Lemma valToValue_lessdef : - forall v v', - valToValue v = Some v' -> - val_value_lessdef v v'. -Proof. - intros. - destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. - symmetry. apply valueToInt_intToValue. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. - inv H1. symmetry. apply valueToPtr_ptrToValue. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. - inv H1. apply Z.eqb_eq. apply Heqb0. -Qed. - -Lemma boolToValue_ValueToBool : - forall b, - valueToBool (boolToValue 32 b) = b. -Proof. destruct b; auto. Qed. - -Local Open Scope Z. - -Ltac word_op_value H := - intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. - -Lemma zadd_vplus : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_plus. Qed. - -Lemma zadd_vplus2 : - forall z1 z2, - vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2). -Proof. - intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl. - rewrite ZToWord_plus; auto. -Qed. - -Lemma ZToValue_eq : - forall w1, - (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. - -Lemma wordsize_32 : - Int.wordsize = 32%nat. -Proof. auto. Qed. - -Lemma intadd_vplus : - forall i1 i2, - valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. -Proof. - intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus. - rewrite <- Int.unsigned_repr_eq. - rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. -Qed. - -(*Lemma intadd_vplus2 : - forall v1 v2 EQ, - vsize v1 = 32%nat -> - Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). -Proof. - intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). - rewrite (@vadd_vplus v1 v2 EQ). trivial. - unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)). - rewrite H in EQ. rewrite <- EQ in H0 at 3.*) - (*rewrite zadd_vplus3. trivia*) - -Lemma valadd_vplus : - forall v1 v2 v1' v2' v v' EQ, - val_value_lessdef v1 v1' -> - val_value_lessdef v2 v2' -> - Val.add v1 v2 = v -> - vplus v1' v2' EQ = v' -> - val_value_lessdef v v'. -Proof. - intros. inv H; inv H0; constructor; simplify. - Abort. - -Lemma zsub_vminus : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_minus. Qed. - -Lemma zmul_vmul : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_mult. Qed. - -Local Open Scope N. -Lemma zdiv_vdiv : - forall n1 n2, - n1 < 2 ^ 32 -> - n2 < 2 ^ 32 -> - n1 / n2 < 2 ^ 32 -> - valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2. -Proof. - intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv. - unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. -Qed. - -Lemma ZToValue_valueToNat : - forall x sz, - (sz > 0)%nat -> - (0 <= x < 2^(Z.of_nat sz))%Z -> - valueToNat (ZToValue sz x) = Z.to_nat x. -Proof. - destruct x; intros; unfold ZToValue, valueToNat; crush. - - rewrite wzero'_def. apply wordToNat_wzero. - - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. - clear H1. - lazymatch goal with - | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H - end. - 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. } - - rewrite Z2Nat.inj_pow in H2; crush. - replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity. - rewrite Nat2Z.id in H2. - rewrite <- positive_nat_Z in H2. - apply Nat2Z.inj_lt in H2. - assumption. -Qed. diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v deleted file mode 100644 index f1fd056..0000000 --- a/src/verilog/ValueInt.v +++ /dev/null @@ -1,167 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * 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 . - *) - -(* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. -From compcert Require Import lib.Integers common.Values. -From vericert Require Import Vericertlib. -(* end hide *) - -(** * Value - -A [value] is a bitvector with a specific size. We are using the implementation -of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. -However, we need to wrap it with an [Inductive] so that we can specify and match -on the size of the [value]. This is necessary so that we can easily store -[value]s of different sizes in a list or in a map. - -Using the default [word], this would not be possible, as the size is part of the type. *) - -Definition value : Type := int. - -(** ** Value conversions - -Various conversions to different number types such as [N], [Z], [positive] and -[int], where the last one is a theory of integers of powers of 2 in CompCert. *) - -Definition valueToNat (v : value) : nat := - Z.to_nat (Int.unsigned v). - -Definition natToValue (n : nat) : value := - Int.repr (Z.of_nat n). - -Definition valueToN (v : value) : N := - Z.to_N (Int.unsigned v). - -Definition NToValue (n : N) : value := - Int.repr (Z.of_N n). - -Definition ZToValue (z : Z) : value := - Int.repr z. - -Definition valueToZ (v : value) : Z := - Int.signed v. - -Definition uvalueToZ (v : value) : Z := - Int.unsigned v. - -Definition posToValue (p : positive) : value := - Int.repr (Z.pos p). - -Definition valueToPos (v : value) : positive := - Z.to_pos (Int.unsigned v). - -Definition intToValue (i : Integers.int) : value := i. - -Definition valueToInt (i : value) : Integers.int := i. - -Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i. - -Definition valueToPtr (i : value) : Integers.ptrofs := - Ptrofs.of_int i. - -Definition valToValue (v : Values.val) : option value := - match v with - | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => Some (ptrToValue off) - | Values.Vundef => Some (ZToValue 0%Z) - | _ => None - end. - -(** Convert a [value] to a [bool], so that choices can be made based on the -result. This is also because comparison operators will give back [value] instead -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 false else true. - -Definition boolToValue (b : bool) : value := - natToValue (if b then 1 else 0). - -(** ** Arithmetic operations *) - -Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -intros; subst; assumption. Defined. - -Lemma unify_word_unfold : - forall sz w, - unify_word sz sz w eq_refl = w. -Proof. auto. Qed. - -Inductive val_value_lessdef: val -> value -> Prop := -| val_value_lessdef_int: - forall i v', - i = valueToInt v' -> - val_value_lessdef (Vint i) v' -| val_value_lessdef_ptr: - forall b off v', - off = valueToPtr v' -> - val_value_lessdef (Vptr b off) v' -| lessdef_undef: forall v, val_value_lessdef Vundef v. - -Inductive opt_val_value_lessdef: option val -> value -> Prop := -| opt_lessdef_some: - forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' -| opt_lessdef_none: forall v, opt_val_value_lessdef None v. - -Lemma valueToZ_ZToValue : - forall z, - (Int.min_signed <= z <= Int.max_signed)%Z -> - valueToZ (ZToValue z) = z. -Proof. auto using Int.signed_repr. Qed. - -Lemma uvalueToZ_ZToValue : - forall z, - (0 <= z <= Int.max_unsigned)%Z -> - uvalueToZ (ZToValue z) = z. -Proof. auto using Int.unsigned_repr. Qed. - -Lemma valueToPos_posToValue : - forall v, - 0 <= Z.pos v <= Int.max_unsigned -> - valueToPos (posToValue v) = v. -Proof. - unfold valueToPos, posToValue. - intros. rewrite Int.unsigned_repr. - apply Pos2Z.id. assumption. -Qed. - -Lemma valueToInt_intToValue : - forall v, - valueToInt (intToValue v) = v. -Proof. auto. Qed. - -Lemma valToValue_lessdef : - forall v v', - valToValue v = Some v' -> - val_value_lessdef v v'. -Proof. - intros. - destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. - unfold valueToInt. unfold intToValue in H1. auto. - inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. -Qed. - -Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, - ptrToValue in *). - -Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v deleted file mode 100644 index 3b0dd0a..0000000 --- a/src/verilog/Verilog.v +++ /dev/null @@ -1,893 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -From Coq Require Import - Structures.OrderedTypeEx - FSets.FMapPositive - Program.Basics - PeanoNat - ZArith - Lists.List - Program. - -Require Import Lia. - -Import ListNotations. - -From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array. -From compcert Require Events. -From compcert Require Import Integers Errors Smallstep Globalenvs. - -Local Open Scope assocmap. - -Set Implicit Arguments. - -Definition reg : Type := positive. -Definition node : Type := positive. -Definition szreg : Type := reg * nat. - -Record associations (A : Type) : Type := - mkassociations { - assoc_blocking : AssocMap.t A; - assoc_nonblocking : AssocMap.t A - }. - -Definition arr := (Array (option value)). - -Definition reg_associations := associations value. -Definition arr_associations := associations arr. - -Definition assocmap_reg := AssocMap.t value. -Definition assocmap_arr := AssocMap.t arr. - -Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := - AssocMapExt.merge value new old. - -Definition merge_cell (new : option value) (old : option value) : option value := - match new, old with - | Some _, _ => new - | _, _ => old - end. - -Definition merge_arr (new : option arr) (old : option arr) : option arr := - match new, old with - | Some new', Some old' => Some (combine merge_cell new' old') - | Some new', None => Some new' - | None, Some old' => Some old' - | None, None => None - end. - -Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := - AssocMap.combine merge_arr new old. - -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := - match a ! r with - | None => None - | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr))) - end. - -Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := - match a ! r with - | None => a - | Some arr => a # r <- (array_set i (Some v) arr) - end. - -Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). - -Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). - -Definition block_reg (r : reg) (asr : reg_associations) (v : value) := - mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). - -Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := - mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). - -Inductive scl_decl : Type := VScalar (sz : nat). -Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). - -(** * Verilog AST - -The Verilog AST is defined here, which is the target language of the -compilation. - -** Value - -The Verilog [value] is a bitvector containg a size and the actual bitvector. In -this case, the [Word.word] type is used as many theorems about that bitvector -have already been proven. *) - -(** ** Binary Operators - -These are the binary operations that can be represented in Verilog. Ideally, -multiplication and division would be done by custom modules which could al so be -scheduled properly. However, for now every Verilog operator is assumed to take -one clock cycle. *) - -Inductive binop : Type := -| Vadd : binop (** addition (binary [+]) *) -| Vsub : binop (** subtraction (binary [-]) *) -| Vmul : binop (** multiplication (binary [*]) *) -| Vdiv : binop (** division (binary [/]) *) -| Vdivu : binop (** division unsigned (binary [/]) *) -| Vmod : binop (** remainder ([%]) *) -| Vmodu : binop (** remainder unsigned ([%]) *) -| Vlt : binop (** less than ([<]) *) -| Vltu : binop (** less than unsigned ([<]) *) -| Vgt : binop (** greater than ([>]) *) -| Vgtu : binop (** greater than unsigned ([>]) *) -| Vle : binop (** less than or equal ([<=]) *) -| Vleu : binop (** less than or equal unsigned ([<=]) *) -| Vge : binop (** greater than or equal ([>=]) *) -| Vgeu : binop (** greater than or equal unsigned ([>=]) *) -| Veq : binop (** equal to ([==]) *) -| Vne : binop (** not equal to ([!=]) *) -| Vand : binop (** and (binary [&]) *) -| Vor : binop (** or (binary [|]) *) -| Vxor : binop (** xor (binary [^|]) *) -| Vshl : binop (** shift left ([<<]) *) -| Vshr : binop (** shift right ([>>>]) *) -| Vshru : binop. (** shift right unsigned ([>>]) *) -(*| Vror : binop (** shift right unsigned ([>>]) *)*) - -(** ** Unary Operators *) - -Inductive unop : Type := -| Vneg (** negation ([~]) *) -| Vnot. (** not operation [!] *) - -(** ** Expressions *) - -Inductive expr : Type := -| Vlit : value -> expr -| Vvar : reg -> expr -| Vvari : reg -> expr -> expr -| Vinputvar : reg -> expr -| Vbinop : binop -> expr -> expr -> expr -| Vunop : unop -> expr -> expr -| Vternary : expr -> expr -> expr -> expr. - -Definition posToExpr (p : positive) : expr := - Vlit (posToValue p). - -(** ** Statements *) - -Inductive stmnt : Type := -| Vskip : stmnt -| Vseq : stmnt -> stmnt -> stmnt -| Vcond : expr -> stmnt -> stmnt -> stmnt -| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt -| Vblock : expr -> expr -> stmnt -| Vnonblock : expr -> expr -> stmnt. - -(** ** Edges - -These define when an always block should be triggered, for example if the always -block should be triggered synchronously at the clock edge, or asynchronously for -combinational logic. - -[edge] is not part of [stmnt] in this formalisation because is closer to the -semantics that are used. *) - -Inductive edge : Type := -| Vposedge : reg -> edge -| Vnegedge : reg -> edge -| Valledge : edge -| Voredge : edge -> edge -> edge. - -(** ** Module Items - -Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). -The declarations are always register declarations as combinational logic can be -done using combinational always block instead of continuous assignments. *) - -Inductive io : Type := -| Vinput : io -| Voutput : io -| Vinout : io. - -Inductive declaration : Type := -| Vdecl : option io -> reg -> nat -> declaration -| Vdeclarr : option io -> reg -> nat -> nat -> declaration. - -Inductive module_item : Type := -| Vdeclaration : declaration -> module_item -| Valways : edge -> stmnt -> module_item -| Valways_ff : edge -> stmnt -> module_item -| Valways_comb : edge -> stmnt -> module_item. - -(** The main module type containing all the important control signals - -- [mod_start] If set, starts the computations in the module. -- [mod_reset] If set, reset the state in the module. -- [mod_clk] The clock that controls the computation in the module. -- [mod_args] The arguments to the module. -- [mod_finish] Bit that is set if the result is ready. -- [mod_return] The return value that was computed. -- [mod_body] The body of the module, including the state machine. -*) - -Record module : Type := mkmodule { - mod_start : reg; - mod_reset : reg; - mod_clk : reg; - mod_finish : reg; - mod_return : reg; - mod_st : reg; (**r Variable that defines the current state, it should be internal. *) - mod_stk : reg; - mod_stk_len : nat; - mod_args : list reg; - mod_body : list module_item; - mod_entrypoint : node; -}. - -Definition fundef := AST.fundef module. - -Definition program := AST.program fundef unit. - -(** Convert a [positive] to an expression directly, setting it to the right - size. *) -Definition posToLit (p : positive) : expr := - Vlit (posToValue p). - -Definition fext := unit. -Definition fextclk := nat -> fext. - -(** ** State - -The [state] contains the following items: -n -- Current [module] that is being worked on, so that the state variable can be -retrieved and set appropriately. -- Current [module_item] which is being worked on. -- A contiunation ([cont]) which defines what to do next. The option is to - either evaluate another module item or go to the next clock cycle. Finally - it could also end if the finish flag of the module goes high. -- Association list containing the blocking assignments made, or assignments made - in previous clock cycles. -- Nonblocking association list containing all the nonblocking assignments made - in the current module. -- The environment containing values for the input. -- The program counter which determines the value for the state in this version of - Verilog, as the Verilog was generated by the RTL, which means that we have to - make an assumption about how it looks. In this case, that it contains state - which determines which part of the Verilog is executed. This is then the part - of the Verilog that should match with the RTL. *) - -Inductive stackframe : Type := - Stackframe : - forall (res : reg) - (m : module) - (pc : node) - (reg_assoc : assocmap_reg) - (arr_assoc : assocmap_arr), - stackframe. - -Inductive state : Type := -| State : - forall (stack : list stackframe) - (m : module) - (st : node) - (reg_assoc : assocmap_reg) - (arr_assoc : assocmap_arr), state -| Returnstate : - forall (res : list stackframe) - (v : value), state -| Callstate : - forall (stack : list stackframe) - (m : module) - (args : list value), state. - -Definition binop_run (op : binop) (v1 v2 : value) : option value := - match op with - | Vadd => Some (Int.add v1 v2) - | Vsub => Some (Int.sub v1 v2) - | Vmul => Some (Int.mul v1 v2) - | Vdiv => if Int.eq v2 Int.zero - || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone - then None - else Some (Int.divs v1 v2) - | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2) - | Vmod => if Int.eq v2 Int.zero - || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone - then None - else Some (Int.mods v1 v2) - | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2) - | Vlt => Some (boolToValue (Int.lt v1 v2)) - | Vltu => Some (boolToValue (Int.ltu v1 v2)) - | Vgt => Some (boolToValue (Int.lt v2 v1)) - | Vgtu => Some (boolToValue (Int.ltu v2 v1)) - | Vle => Some (boolToValue (negb (Int.lt v2 v1))) - | Vleu => Some (boolToValue (negb (Int.ltu v2 v1))) - | Vge => Some (boolToValue (negb (Int.lt v1 v2))) - | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2))) - | Veq => Some (boolToValue (Int.eq v1 v2)) - | Vne => Some (boolToValue (negb (Int.eq v1 v2))) - | Vand => Some (Int.and v1 v2) - | Vor => Some (Int.or v1 v2) - | Vxor => Some (Int.xor v1 v2) - | Vshl => Some (Int.shl v1 v2) - | Vshr => Some (Int.shr v1 v2) - | Vshru => Some (Int.shru v1 v2) - end. - -Definition unop_run (op : unop) (v1 : value) : value := - match op with - | Vneg => Int.neg v1 - | Vnot => Int.not v1 - end. - -Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := - | erun_Vlit : - forall fext reg stack v, - expr_runp fext reg stack (Vlit v) v - | erun_Vvar : - forall fext reg stack v r, - reg#r = v -> - expr_runp fext reg stack (Vvar r) v - | erun_Vvari : - forall fext reg stack v iexp i r, - expr_runp fext reg stack iexp i -> - arr_assocmap_lookup stack r (valueToNat i) = Some v -> - expr_runp fext reg stack (Vvari r iexp) v - | erun_Vbinop : - forall fext reg stack op l r lv rv resv, - expr_runp fext reg stack l lv -> - expr_runp fext reg stack r rv -> - Some resv = binop_run op lv rv -> - expr_runp fext reg stack (Vbinop op l r) resv - | erun_Vunop : - forall fext reg stack u vu op oper resv, - expr_runp fext reg stack u vu -> - oper = unop_run op -> - resv = oper vu -> - expr_runp fext reg stack (Vunop op u) resv - | erun_Vternary_true : - forall fext reg stack c ts fs vc vt, - expr_runp fext reg stack c vc -> - expr_runp fext reg stack ts vt -> - valueToBool vc = true -> - expr_runp fext reg stack (Vternary c ts fs) vt - | erun_Vternary_false : - forall fext reg stack c ts fs vc vf, - 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. -Hint Constructors expr_runp : verilog. - -Definition handle_opt {A : Type} (err : errmsg) (val : option A) - : res A := - match val with - | Some a => OK a - | None => Error err - end. - -Definition handle_def {A : Type} (a : A) (val : option A) - : res A := - match val with - | Some a' => OK a' - | None => OK a - end. - -Local Open Scope error_monad_scope. - -(*Definition access_fext (f : fext) (r : reg) : res value := - match AssocMap.get r f with - | Some v => OK v - | _ => OK (ZToValue 0) - end.*) - -(* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assocmap) (e : expr) - {struct e} : res value := - match e with - | Vlit v => OK v - | Vvar r => match s with - | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r - | _ => Error (msg "Verilog: Wrong state") - end - | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") - | Vinputvar r => access_fext s r - | Vbinop op l r => - let lv := expr_run s l in - let rv := expr_run s r in - let oper := binop_run op in - do lv' <- lv; - do rv' <- rv; - handle_opt (msg "Verilog: sizes are not equal") - (eq_to_opt lv' rv' (oper lv' rv')) - | Vunop op e => - let oper := unop_run op in - do ev <- expr_run s e; - OK (oper ev) - | Vternary c te fe => - do cv <- expr_run s c; - if valueToBool cv then expr_run s te else expr_run s fe - end.*) - -(** Return the location of the lhs of an assignment. *) - -Inductive location : Type := -| LocReg (_ : reg) -| LocArray (_ : reg) (_ : nat). - -Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := -| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) -| Indexed : forall f asr asa r iexp iv, - expr_runp f asr asa iexp iv -> - location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). - -(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) -(* match e with *) -(* | Vvar r => OK r *) -(* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *) -(* end. *) - -(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := - match st with - | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) - | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) - | Vcase _ ls (Some st) => - S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) - | _ => 1 - end. - -Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) - {struct cl} : option (res stmnt) := - match cl with - | (e, st)::xs => - match expr_run s e with - | OK v' => - match eq_to_opt v v' (veq v v') with - | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs - | None => Some (Error (msg "Verilog: equality check sizes not equal")) - end - | Error msg => Some (Error msg) - end - | _ => None - end. - -Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := - match n with - | S n' => - match st with - | Vskip => OK s - | Vseq s1 s2 => - do s' <- stmnt_run' n' s s1; - stmnt_run' n' s' s2 - | Vcond c st sf => - do cv <- expr_run s c; - if valueToBool cv - then stmnt_run' n' s st - else stmnt_run' n' s sf - | Vcase e cl defst => - do v <- expr_run s e; - match find_case_stmnt s v cl with - | Some (OK st') => stmnt_run' n' s st' - | Some (Error msg) => Error msg - | None => do s' <- handle_opt (msg "Verilog: no case was matched") - (option_map (stmnt_run' n' s) defst); s' - end - | Vblock lhs rhs => - match s with - | State m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) - | _ => Error (msg "Verilog: Wrong state") - end - | Vnonblock lhs rhs => - match s with - | State m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) - | _ => Error (msg "Verilog: Wrong state") - end - end - | _ => OK s - end. - -Definition stmnt_run (s : state) (st : stmnt) : res state := - stmnt_run' (stmnt_height st) s st. *) - -Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> - stmnt -> reg_associations -> arr_associations -> Prop := -| stmnt_runp_Vskip: - forall f ar al, stmnt_runp f ar al Vskip ar al -| stmnt_runp_Vseq: - forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2, - stmnt_runp f asr0 asa0 st1 asr1 asa1 -> - stmnt_runp f asr1 asa1 st2 asr2 asa2 -> - stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2 -| stmnt_runp_Vcond_true: - forall asr0 asa0 asr1 asa1 f c vc stt stf, - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> - valueToBool vc = true -> - stmnt_runp f asr0 asa0 stt asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 -| stmnt_runp_Vcond_false: - 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 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, - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> - mve <> ve -> - stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 -| stmnt_runp_Vcase_match: - forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> - mve = ve -> - stmnt_runp f asr0 asa0 sc asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 -| stmnt_runp_Vcase_default: - forall asr0 asa0 asr1 asa1 f st e ve, - expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> - stmnt_runp f asr0 asa0 st asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 -| stmnt_runp_Vblock_reg: - forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> - expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> - stmnt_runp f asr asa - (Vblock lhs rhs) - (block_reg r asr rhsval) asa -| stmnt_runp_Vnonblock_reg: - forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> - expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> - stmnt_runp f asr asa - (Vnonblock lhs rhs) - (nonblock_reg r asr rhsval) asa -| stmnt_runp_Vblock_arr: - forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> - expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> - stmnt_runp f asr asa - (Vblock lhs rhs) - asr (block_arr r i asa rhsval) -| stmnt_runp_Vnonblock_arr: - forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> - expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> - stmnt_runp f asr asa - (Vnonblock lhs rhs) - asr (nonblock_arr r i asa rhsval). -Hint Constructors stmnt_runp : verilog. - -(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := - let run := fun st ls => - do s' <- stmnt_run s st; - mi_step s' ls - in - match m with - | (Valways _ st)::ls => run st ls - | (Valways_ff _ st)::ls => run st ls - | (Valways_comb _ st)::ls => run st ls - | (Vdecl _ _)::ls => mi_step s ls - | (Vdeclarr _ _ _)::ls => mi_step s ls - | nil => OK s - end.*) - -Inductive mi_stepp : fext -> reg_associations -> arr_associations -> - module_item -> reg_associations -> arr_associations -> Prop := -| mi_stepp_Valways : - forall f sr0 sa0 st sr1 sa1 c, - stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 -| mi_stepp_Valways_ff : - forall f sr0 sa0 st sr1 sa1 c, - stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1 -| mi_stepp_Valways_comb : - forall f sr0 sa0 st sr1 sa1 c, - stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 -| mi_stepp_Vdecl : - forall f sr sa d, - mi_stepp f sr sa (Vdeclaration d) sr sa. -Hint Constructors mi_stepp : verilog. - -Inductive mis_stepp : fext -> reg_associations -> arr_associations -> - list module_item -> reg_associations -> arr_associations -> Prop := -| mis_stepp_Cons : - forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2, - mi_stepp f sr0 sa0 mi sr1 sa1 -> - mis_stepp f sr1 sa1 mis sr2 sa2 -> - mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2 -| mis_stepp_Nil : - forall f sr sa, - mis_stepp f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. - -(*Definition mi_step_commit (s : state) (m : list module_item) : res state := - match mi_step s m with - | OK (State m assoc nbassoc f c) => - OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) - | Error msg => Error msg - | _ => Error (msg "Verilog: Wrong state") - end. - -Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) - {struct n} : res assocmap := - match n with - | S n' => - do assoc' <- mi_run f assoc m n'; - match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with - | OK (State assoc _ _ _) => OK assoc - | Error m => Error m - end - | O => OK assoc - end.*) - -(** Resets the module into a known state, so that it can be executed. This is -assumed to be the starting state of the module, and may have to be changed if -other arguments to the module are also to be supported. *) - -(*Definition initial_fextclk (m : module) : fextclk := - fun x => match x with - | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) - | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) - end.*) - -(*Definition module_run (n : nat) (m : module) : res assocmap := - mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) - -Local Close Scope error_monad_scope. - -(*Theorem value_eq_size_if_eq: - forall lv rv EQ, - vsize lv = vsize rv -> value_eq_size lv rv = left EQ. -Proof. intros. unfold value_eq_size. - -Theorem expr_run_same: - forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. -Proof. - split; generalize dependent v; generalize dependent assoc. - - induction e. - + intros. inversion H. constructor. - + intros. inversion H. constructor. assumption. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. - unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. - constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. - discriminate. - + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. - inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. - eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. - eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. - discriminate. - - induction e. - + intros. inversion H. reflexivity. - + intros. inversion H. subst. simpl. assumption. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. - apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). - apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. - + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. - apply IHe in H3. rewrite Heqo in H3. - inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. - apply IHe2 in H6. rewrite H6. reflexivity. - subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. - assumption. -Qed. - - *) - -Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := - match rl, vl with - | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') - | _, _ => empty_assocmap - end. - -Definition genv := Globalenvs.Genv.t fundef unit. -Definition empty_stack (m : module) : assocmap_arr := - (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty 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 -> - mis_stepp f (mkassociations asr empty_assocmap) - (mkassociations asa (empty_stack m)) - m.(mod_body) - (mkassociations basr1 nasr1) - (mkassociations basa1 nasa1)-> - asr' = merge_regs nasr1 basr1 -> - asa' = merge_arrs nasa1 basa1 -> - asr'!(m.(mod_st)) = Some stval -> - valueToPos stval = pstval -> - step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') -| step_finish : - forall asr asa sf retval m st g, - asr!(m.(mod_finish)) = Some (ZToValue 1) -> - asr!(m.(mod_return)) = Some retval -> - step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) -| step_call : - forall g res m args, - step g (Callstate res m args) Events.E0 - (State res m m.(mod_entrypoint) - (AssocMap.set (mod_reset m) (ZToValue 0) - (AssocMap.set (mod_finish m) (ZToValue 0) - (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) - (init_params args m.(mod_args))))) - (empty_stack m)) -| step_return : - forall g m asr i r sf pc mst asa, - 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) asa). -Hint Constructors step : verilog. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b m0 m, - let ge := Globalenvs.Genv.globalenv p in - Globalenvs.Genv.init_mem p = Some m0 -> - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> - initial_state p (Callstate nil m nil). - -Inductive final_state : state -> Integers.int -> Prop := -| final_state_intro : forall retval retvali, - retvali = valueToInt retval -> - final_state (Returnstate nil retval) retvali. - -Definition semantics (m : program) := - Smallstep.Semantics step (initial_state m) final_state - (Globalenvs.Genv.globalenv m). - -Lemma expr_runp_determinate : - forall f e asr asa v, - expr_runp f asr asa e v -> - forall v', - expr_runp f asr asa e v' -> - v' = v. -Proof. - induction e; intros; - - repeat (try match goal with - | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H - - | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, - H2 : expr_runp _ _ _ ?e _ |- _ ] => - learn (H1 _ _ _ H2) - | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _, - H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => - learn (H1 _ H2) - end; crush). -Qed. -Hint Resolve expr_runp_determinate : verilog. - -Lemma location_is_determinate : - forall f asr asa e l, - location_is f asr asa e l -> - forall l', - location_is f asr asa e l' -> - l' = l. -Proof. - induction 1; intros; - - repeat (try match goal with - | [ H : location_is _ _ _ _ _ |- _ ] => invert H - | [ H1 : expr_runp _ ?asr ?asa ?e _, - H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => - learn (expr_runp_determinate H1 H2) - end; crush). -Qed. - -Lemma stmnt_runp_determinate : - forall f s asr0 asa0 asr1 asa1, - stmnt_runp f asr0 asa0 s asr1 asa1 -> - forall asr1' asa1', - stmnt_runp f asr0 asa0 s asr1' asa1' -> - asr1' = asr1 /\ asa1' = asa1. - induction 1; intros; - - repeat (try match goal with - | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H - - | [ H1 : expr_runp _ ?asr ?asa ?e _, - H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => - learn (expr_runp_determinate H1 H2) - - | [ H1 : location_is _ ?asr ?asa ?e _, - H2 : location_is _ ?asr ?asa ?e _ |- _ ] => - learn (location_is_determinate H1 H2) - - | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _, - H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => - learn (H1 _ _ H2) - end; crush). -Qed. -Hint Resolve stmnt_runp_determinate : verilog. - -Lemma mi_stepp_determinate : - forall f asr0 asa0 m asr1 asa1, - mi_stepp f asr0 asa0 m asr1 asa1 -> - forall asr1' asa1', - mi_stepp f asr0 asa0 m asr1' asa1' -> - asr1' = asr1 /\ asa1' = asa1. -Proof. - intros. destruct m; invert H; invert H0; - - repeat (try match goal with - | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, - H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => - learn (stmnt_runp_determinate H1 H2) - end; crush). -Qed. - -Lemma mis_stepp_determinate : - forall f asr0 asa0 m asr1 asa1, - mis_stepp f asr0 asa0 m asr1 asa1 -> - forall asr1' asa1', - mis_stepp f asr0 asa0 m asr1' asa1' -> - asr1' = asr1 /\ asa1' = asa1. -Proof. - induction 1; intros; - - repeat (try match goal with - | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H - | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H - - | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, - H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => - learn (mi_stepp_determinate H1 H2) - - | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _, - H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] => - learn (H1 _ _ H2) - end; crush). -Qed. - -Lemma semantics_determinate : - forall (p: program), Smallstep.determinate (semantics p). -Proof. - intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. - pose proof (mis_stepp_determinate H5 H15). - crush. - - constructor. invert H; crush. - - invert H; invert H0; unfold ge0, ge1 in *; crush. - - red; simplify; intro; invert H0; invert H; crush. - - invert H; invert H0; crush. -Qed. -- cgit