From c106b109fa0d469568c4841f07f7243a4f7813a4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 4 May 2020 12:08:04 +0100 Subject: Refine the semantics --- src/verilog/Test.v | 37 +++++++++++++++--- src/verilog/Value.v | 44 +++++++++++++++++---- src/verilog/Verilog.v | 105 ++++++++++++++++++++++++++++++-------------------- 3 files changed, 130 insertions(+), 56 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 7a31865..5c22ef2 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -64,10 +64,35 @@ Lemma valid_test_output : transf_program test_input_program = OK test_output_module. Proof. trivial. Qed. +Definition test_fextclk := initial_fextclk test_output_module. + Lemma manual_simulation : - forall f, - step (State test_output_module empty_assoclist - (initial_fextclk test_output_module) - 1%nat 1%positive) - (State test_output_module test_output_module (add_assoclist 7 (32'h"3") empty_assoclist) - 2%nat 3%positive). + step (State test_output_module empty_assoclist empty_assoclist + test_fextclk 1 (32'h"1")) + (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist) + empty_assoclist test_fextclk 2 (32'h"3")). +Proof. + apply step_module with (assoc1 := empty_assoclist) + (nbassoc := (add_assoclist 7%positive (32'h"3") empty_assoclist)); auto. + apply mis_stepp_Cons with (s1 := State test_output_module empty_assoclist (add_assoclist 7%positive (32'h"3") empty_assoclist) test_fextclk 1%nat (32'h"1")). + apply mi_stepp_Valways_ff. + apply stmnt_runp_Vcond_true with (f := test_fextclk 1%nat) + (assoc := empty_assoclist) + (vc := 1'h"1"); auto. + apply get_state_fext_assoc. + apply erun_Vbinop with (lv := 1'h"1") + (rv := 1'h"1") + (oper := veq) + (EQ := EQ_trivial (1'h"1")); auto. + apply erun_Vinputvar; auto. + apply erun_Vlit. + eapply stmnt_runp_Vnonblock. simpl. auto. + apply erun_Vlit. + auto. + eapply mis_stepp_Cons. + apply mi_stepp_Valways_ff. + eapply stmnt_runp_Vcase_nomatch. + apply get_state_fext_assoc. + apply erun_Vvar_empty. auto. + apply erun_Vlit. + unfold ZToValue. instantiate (1 := 32%nat). simpl. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 1d31110..21e59be 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -60,13 +60,6 @@ Definition valueToN (v : value) : N := Definition NToValue sz (n : N) : value := mkvalue sz (NToWord sz n). -Definition posToValue sz (p : positive) : value := - mkvalue sz (posToWord sz p). - -Definition posToValueAuto (p : positive) : value := - let size := Z.to_nat (Z.succ (log_inf p)) in - mkvalue size (Word.posToWord size p). - Definition ZToValue (s : nat) (z : Z) : value := mkvalue s (ZToWord s z). @@ -76,6 +69,19 @@ Definition valueToZ (v : value) : Z := Definition uvalueToZ (v : value) : Z := uwordToZ (vword v). +Definition posToValue sz (p : positive) : value := + mkvalue sz (posToWord sz p). + +Definition posToValueAuto (p : positive) : value := + let size := Z.to_nat (Z.succ (log_inf p)) in + mkvalue size (Word.posToWord size p). + +Definition valueToPos (v : value) : positive := + match valueToZ v with + | Zpos p => p + | _ => 1 + end. + Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). @@ -95,8 +101,10 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) +Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. + Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -Proof. intros; subst; assumption. Qed. +Proof. intros; subst; assumption. Defined. Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. @@ -141,6 +149,26 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) | _ => None end. +Lemma eqvalue {sz : nat} (x y : word sz) : x = y -> (mkvalue sz x = mkvalue sz y). +Proof. intros. subst. reflexivity. Qed. + +Lemma nevalue {sz : nat} (x y : word sz) : x <> y -> (mkvalue sz x <> mkvalue sz y). +Proof. Admitted. + +Definition valueEqCheck (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 (eqvalue x y eq) + | right ne => right (nevalue x y ne) + end. + +Definition valueEq (x y : value) (EQ : vsize x = vsize y): {x = y} + {x <> y} := + let unif_y := unify_word (vsize x) (vsize y) (vword y) EQ in + match weq (vword x) unif_y with + | left _ => left _ + | right _ => right _ + end. + (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 7a3982c..a927eac 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -31,6 +31,8 @@ From coqup Require Import common.Coquplib common.Show verilog.Value. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. +Import HexNotationValue. + Notation "a ! b" := (PositiveMap.find b a) (at level 1). Definition reg : Type := positive. @@ -196,13 +198,11 @@ retrieved and set appropriately. Inductive state : Type := | State: forall (m : module) - (mi : module_item) - (mis : list module_item) (assoc : assoclist) (nbassoc : assoclist) (f : fextclk) (cycle : nat) - (pc : positive), + (stvar : value), state | Finishstate: forall v : value, @@ -248,21 +248,27 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := forall fext assoc v r, assoc!r = Some v -> expr_runp fext assoc (Vvar r) v + | erun_Vvar_empty : + forall fext assoc r sz, + assoc!r = None -> + expr_runp fext assoc (Vvar r) (ZToValue sz 0) | erun_Vinputvar : forall fext assoc r v, fext!r = Some v -> expr_runp fext assoc (Vinputvar r) v | erun_Vbinop : - forall fext assoc op l r lv rv oper EQ, + forall fext assoc op l r lv rv oper EQ resv, expr_runp fext assoc l lv -> expr_runp fext assoc r rv -> oper = binop_run op -> - expr_runp fext assoc (Vbinop op l r) (oper lv rv EQ) + resv = oper lv rv EQ -> + expr_runp fext assoc (Vbinop op l r) resv | erun_Vunop : - forall fext assoc u vu op oper, + forall fext assoc u vu op oper resv, expr_runp fext assoc u vu -> oper = unop_run op -> - expr_runp fext assoc (Vunop op u) (oper vu) + resv = oper vu -> + expr_runp fext assoc (Vunop op u) resv | erun_Vternary_true : forall fext assoc c ts fs vc vt, expr_runp fext assoc c vc -> @@ -402,17 +408,10 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := Definition stmnt_run (s : state) (st : stmnt) : res state := stmnt_run' (stmnt_height st) s st. *) -Inductive not_matched : state -> value -> expr * stmnt -> Prop := - not_in: - forall caseval curr currval m mi c assoc nbassoc f cycle pc, - expr_runp (f cycle) assoc (fst curr) currval -> - caseval <> currval -> - not_matched (State m mi c assoc nbassoc f cycle pc) caseval curr. - Inductive state_fext_assoc : state -> fext * assoclist -> Prop := | get_state_fext_assoc : - forall m mi c assoc nbassoc f cycle pc, - state_fext_assoc (State m mi c assoc nbassoc f cycle pc) (f cycle, assoc). + forall c assoc nbassoc f cycle pc, + state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc). Inductive stmnt_runp: state -> stmnt -> state -> Prop := | stmnt_run_Vskip: @@ -436,38 +435,44 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := valueToBool vc = false -> stmnt_runp s0 stf s1 -> stmnt_runp s0 (Vcond c stt stf) s1 -| stmnt_runp_Vcase: - forall e ve s0 f assoc s1 me mve sc clst def, +| stmnt_runp_Vcase_match: + forall e ve s0 f assoc s1 me mve sc cs def, state_fext_assoc s0 (f, assoc) -> expr_runp f assoc e ve -> expr_runp f assoc me mve -> mve = ve -> - In (me, sc) clst -> stmnt_runp s0 sc s1 -> - stmnt_runp s0 (Vcase e clst def) s1 + stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 +| stmnt_runp_Vcase_nomatch: + forall e ve s0 f assoc s1 me mve sc cs def, + state_fext_assoc s0 (f, assoc) -> + expr_runp f assoc e ve -> + expr_runp f assoc me mve -> + mve <> ve -> + stmnt_runp s0 (Vcase e cs def) s1 -> + stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 | stmnt_runp_Vcase_default: - forall s0 f assoc st s1 e ve clst, + forall s0 f assoc st s1 e ve, state_fext_assoc s0 (f, assoc) -> expr_runp f assoc e ve -> - Forall (not_matched s0 ve) clst -> stmnt_runp s0 st s1 -> - stmnt_runp s0 (Vcase e clst (Some st)) s1 + stmnt_runp s0 (Vcase e nil (Some st)) s1 | stmnt_runp_Vblock: - forall lhs name rhs rhsval m mi c assoc assoc' nbassoc f cycle pc, + forall lhs name rhs rhsval c assoc assoc' nbassoc f cycle pc, assign_name lhs = OK name -> expr_runp (f cycle) assoc rhs rhsval -> assoc' = (PositiveMap.add name rhsval assoc) -> - stmnt_runp (State m mi c assoc nbassoc f cycle pc) + stmnt_runp (State c assoc nbassoc f cycle pc) (Vblock lhs rhs) - (State m mi c assoc' nbassoc f cycle pc) + (State c assoc' nbassoc f cycle pc) | stmnt_runp_Vnonblock: - forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc, + forall lhs name rhs rhsval c assoc nbassoc nbassoc' f cycle pc, assign_name lhs = OK name -> expr_runp (f cycle) assoc rhs rhsval -> nbassoc' = (PositiveMap.add name rhsval nbassoc) -> - stmnt_runp (State m mi c assoc nbassoc f cycle pc) - (Vblock lhs rhs) - (State m mi c assoc nbassoc' f cycle pc). + stmnt_runp (State c assoc nbassoc f cycle pc) + (Vnonblock lhs rhs) + (State c assoc nbassoc' f cycle pc). (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => @@ -499,6 +504,16 @@ Inductive mi_stepp : state -> module_item -> state -> Prop := forall s lhs rhs, mi_stepp s (Vdecl lhs rhs) s. +Inductive mis_stepp : state -> list module_item -> state -> Prop := +| mis_stepp_Cons : + forall mi mis s0 s1 s2, + mi_stepp s0 mi s1 -> + mis_stepp s1 mis s2 -> + mis_stepp s0 (mi :: mis) s2 +| mis_stepp_Nil : + forall s, + mis_stepp s nil s. + Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := PositiveMap.add r v assoc. @@ -583,19 +598,24 @@ Qed. Definition genv := Genv.t unit unit. - -Inductive step : genv -> state -> Events.trace -> state -> Prop := +Inductive step : state -> state -> Prop := | step_module : - forall g m mi hmi tmi assoc nbassoc f cycle pc e, - step_cc g (State m mi (hmi::tmi) assoc nbassoc f cycle pc) e - (State m hmi tmi assoc nbassoc f cycle pc) -| step_module_empty : - forall g tmi hmi m mi assoc nbassoc f cycle pc e, - hmi::tmi = mod_body m -> - step_cc g (State m mi nil assoc nbassoc f cycle pc) e - (State m hmi tmi assoc nbassoc f (S cycle) pc). - -Inductive initial_state (m: module): state -> Prop := + forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc, + mis_stepp (State m assoc0 empty_assoclist f cycle stvar) + m.(mod_body) + (State m assoc1 nbassoc f cycle stvar) -> + assoc2 = merge_assoclist nbassoc assoc1 -> + Some stvar' = assoc2!(fst m.(mod_state)) -> + step (State m assoc0 empty_assoclist f cycle stvar) + (State m assoc2 empty_assoclist f (S cycle) stvar') +| step_finish : + forall m assoc f cycle stvar result, + assoc!(fst m.(mod_finish)) = Some (1'h"1") -> + assoc!(fst m.(mod_return)) = Some result -> + step (State m assoc empty_assoclist f cycle stvar) + (Finishstate result). + +(*Inductive initial_state (m: module): state -> Prop := | initial_state_intro: forall hmi tmi, hmi::tmi = mod_body m -> @@ -611,3 +631,4 @@ Inductive final_state: state -> Integers.int -> Prop := Definition semantics (p: module) := Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil). +*) -- cgit