diff options
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/Array.v | 337 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 32 | ||||
| -rw-r--r-- | src/verilog/PrintHTL.ml | 81 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 12 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
| -rw-r--r-- | src/verilog/Value.v | 111 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 84 |
7 files changed, 610 insertions, 49 deletions
diff --git a/src/verilog/Array.v b/src/verilog/Array.v new file mode 100644 index 0000000..be06541 --- /dev/null +++ b/src/verilog/Array.v @@ -0,0 +1,337 @@ +Set Implicit Arguments. + +Require Import Lia. +Require Import Coquplib. +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. + info_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/HTL.v b/src/verilog/HTL.v index c07d672..a3623f0 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,7 +17,7 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value AssocMap. +From coqup Require Import Coquplib Value AssocMap Array. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. @@ -46,6 +46,7 @@ Record module: Type := mod_entrypoint : node; mod_st : reg; mod_stk : reg; + mod_stk_len : nat; mod_finish : reg; mod_return : reg; mod_start : reg; @@ -65,6 +66,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct 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. @@ -74,7 +78,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), stackframe. Inductive state : Type := @@ -82,8 +87,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -94,17 +99,19 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data + forall g m st sf ctrl data ist asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 asr' asa' f stval pstval, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = 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 (AssocMap.empty (list value))) + (Verilog.mkassociations asa (empty_stack m)) ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> @@ -114,8 +121,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> - asr' = merge_assocmap nasr2 basr2 -> - asa' = AssocMapExt.merge (list value) nasa2 basa2 -> + asr' = Verilog.merge_regs nasr2 basr2 -> + asa' = Verilog.merge_arrs nasa2 basa2 -> 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') @@ -130,13 +137,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.empty (list value))) + (empty_stack m)) | step_return : - forall g m asr i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml new file mode 100644 index 0000000..0bdba51 --- /dev/null +++ b/src/verilog/PrintHTL.ml @@ -0,0 +1,81 @@ +(* -*- mode: tuareg -*- + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +open Value +open Datatypes +open Camlcoq +open AST +open Clflags +open Printf +open Maps +open AST +open HTL +open PrintAST +open PrintVerilog +open CoqupClflags + +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 index 5dc0386..5265c97 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -22,9 +22,12 @@ open Datatypes open Camlcoq open AST +open Clflags open Printf +open CoqupClflags + let concat = String.concat "" let indent i = String.make (2 * i) ' ' @@ -75,7 +78,7 @@ let rec pprint_expr = function | 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; ")"] + | 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 = @@ -187,6 +190,12 @@ let debug_always i clk state = concat [ 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 @@ -194,6 +203,7 @@ let pprint_module debug i n m = 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" ] diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 6544e52..62bf63f 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -16,6 +16,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +val pprint_stmnt : int -> Verilog.stmnt -> string + val print_value : out_channel -> Value.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..8ba5138 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,7 +19,7 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. (* end hide *) @@ -108,6 +108,11 @@ Definition boolToValue (sz : nat) (b : bool) : value := 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. @@ -294,8 +299,18 @@ Inductive val_value_lessdef: val -> value -> Prop := forall i v', i = valueToInt v' -> val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = Ptrofs.repr (valueToZ v') -> + (Z.modulo (valueToZ 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 -> @@ -314,6 +329,12 @@ Proof. 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. @@ -330,7 +351,19 @@ Proof. rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. split. apply Zle_0_pos. - assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt. + 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. @@ -360,4 +393,76 @@ Qed. Lemma boolToValue_ValueToBool : forall b, valueToBool (boolToValue 32 b) = b. -Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. +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 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 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 -> + (x < 2^(Z.of_nat sz))%Z -> + valueToNat (ZToValue sz x) = Z.to_nat x. +Proof. + destruct x; intros; unfold ZToValue, valueToNat; simpl. + - rewrite wzero'_def. apply wordToNat_wzero. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. + unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. + rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. + Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) + Search "inj" positive nat. +*) diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b80678e..555ddbd 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -25,9 +25,11 @@ From Coq Require Import Lists.List Program. +Require Import Lia. + Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap. +From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. @@ -47,39 +49,51 @@ Record associations (A : Type) : Type := assoc_nonblocking : AssocMap.t A }. +Definition arr := (Array (option value)). + Definition reg_associations := associations value. -Definition arr_associations := associations (list value). +Definition arr_associations := associations arr. -Definition assocmap_arr := AssocMap.t (list value). +Definition assocmap_reg := AssocMap.t value. +Definition assocmap_arr := AssocMap.t arr. -Definition merge_associations {A : Type} (assoc : associations A) := - mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) - (AssocMap.empty A). +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 => nth_error arr i - end. - -Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := - match i, l with - | _, nil => nil - | S n, h :: t => h :: list_set n x t - | O, h :: t => x :: t + | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr))) end. -Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := +Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := match a ! r with | None => a - | Some arr => AssocMap.set r (list_set i v arr) 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 (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). + 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) (assocmap_l_set r i v asa.(assoc_nonblocking)). + 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). @@ -87,8 +101,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := 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 := Scalar (sz : nat). -Inductive arr_decl : Type := Array (sz : nat) (ln : nat). +Inductive scl_decl : Type := VScalar (sz : nat). +Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST @@ -218,6 +232,7 @@ Record module : Type := mkmodule { 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; @@ -235,7 +250,7 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := AssocMap.t value. +Definition fext := assocmap. Definition fextclk := nat -> fext. (** ** State @@ -264,7 +279,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), stackframe. Inductive state : Type := @@ -272,8 +288,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -691,17 +707,21 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := 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, + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) - (mkassociations asa (AssocMap.empty (list value))) + (mkassociations asa (empty_stack m)) m.(mod_body) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1)-> - asr' = merge_assocmap nasr1 basr1 -> - asa' = AssocMapExt.merge (list value) nasa1 basa1 -> + 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') @@ -716,13 +736,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint)) (init_params args m.(mod_args))) - (AssocMap.empty (list value))) + (empty_stack m)) | step_return : - forall g m asr i r sf pc mst, + forall g m asr i r sf pc mst asa, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + (empty_stack m)). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := |