From fdf5e7378715ba1bd8552e2f005c4a15c834a038 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Apr 2020 22:43:03 +0100 Subject: Add stmnt_runp inductive --- src/verilog/Verilog.v | 133 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 106 insertions(+), 27 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 4713c36..4ad297b 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -173,7 +173,7 @@ Definition fext := PositiveMap.t value. Definition fextclk := nat -> fext. Inductive state: Type := - State: + Runstate: forall (assoc : assoclist) (nbassoc : assoclist) (f : fextclk) @@ -219,7 +219,7 @@ Inductive expr_runp : state -> expr -> value -> Prop := | erun_Vvar : forall assoc na f c v r, assoc!r = Some v -> - expr_runp (State assoc na f c) (Vvar r) v + expr_runp (Runstate assoc na f c) (Vvar r) v | erun_Vinputvar : forall s r v, expr_runp s (Vinputvar r) v @@ -265,7 +265,7 @@ Local Open Scope error_monad_scope. Definition access_fext (s : state) (r : reg) : res value := match s with - | State _ _ f c => + | Runstate _ _ f c => match PositiveMap.find r (f (Pos.to_nat c)) with | Some v => OK v | _ => OK (ZToValue 1 0) @@ -278,7 +278,7 @@ Fixpoint expr_run (s : state) (e : expr) match e with | Vlit v => OK v | Vvar r => match s with - | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | Runstate assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r end | Vinputvar r => access_fext s r | Vbinop op l r => @@ -307,6 +307,15 @@ Definition assign_name (e : expr) : res reg := | _ => 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 @@ -345,34 +354,83 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := end | Vblock lhs rhs => match s with - | State assoc nbassoc f c => + | Runstate assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (State (PositiveMap.add name rhse assoc) nbassoc f c) + OK (Runstate (PositiveMap.add name rhse assoc) nbassoc f c) end | Vnonblock lhs rhs => match s with - | State assoc nbassoc f c => + | Runstate assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (State assoc (PositiveMap.add name rhse nbassoc) f c) + OK (Runstate assoc (PositiveMap.add name rhse nbassoc) f c) end end | _ => OK s 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. - Definition stmnt_run (s : state) (st : stmnt) : res state := stmnt_run' (stmnt_height st) s st. +Inductive not_matched (s : state) (caseval : value) (curr : expr * stmnt) : Prop := + not_in: + forall currval, + expr_runp s (fst curr) currval -> + caseval <> currval -> + not_matched s caseval curr. + +Inductive stmnt_runp: state -> stmnt -> state -> Prop := +| stmnt_run_Vskip: + forall s, stmnt_runp s Vskip s +| stmnt_run_Vseq: + forall st1 st2 s0 s1 s2, + stmnt_runp s0 st1 s1 -> + stmnt_runp s1 st2 s2 -> + stmnt_runp s0 (Vseq st1 st2) s2 +| stmnt_runp_Vcond_true: + forall s0 s1 c vc stt stf, + expr_runp s0 c vc -> + valueToBool vc = true -> + stmnt_runp s0 stt s1 -> + stmnt_runp s0 (Vcond c stt stf) s1 +| stmnt_runp_Vcond_false: + forall s0 s1 c vc stt stf, + expr_runp s0 c vc -> + valueToBool vc = false -> + stmnt_runp s0 stf s1 -> + stmnt_runp s0 (Vcond c stt stf) s1 +| stmnt_runp_Vcase: + forall e ve s0 s1 me mve sc clst def, + expr_runp s0 e ve -> + expr_runp s0 me mve -> + mve = ve -> + In (me, sc) clst -> + stmnt_runp s0 sc s1 -> + stmnt_runp s0 (Vcase e clst def) s1 +| stmnt_runp_Vcase_default: + forall s0 st s1 e ve clst, + expr_runp s0 e ve -> + Forall (not_matched s0 ve) clst -> + stmnt_runp s0 st s1 -> + stmnt_runp s0 (Vcase e clst (Some st)) s1 +| stmnt_runp_Vblock: + forall lhs name rhs rhsval s assoc assoc' nbassoc f cycle, + assign_name lhs = OK name -> + expr_runp s rhs rhsval -> + assoc' = (PositiveMap.add name rhsval assoc) -> + stmnt_runp (Runstate assoc nbassoc f cycle) + (Vblock lhs rhs) + (Runstate assoc' nbassoc f cycle) +| stmnt_runp_Vnonblock: + forall lhs name rhs rhsval s assoc nbassoc nbassoc' f cycle, + assign_name lhs = OK name -> + expr_runp s rhs rhsval -> + nbassoc' = (PositiveMap.add name rhsval nbassoc) -> + stmnt_runp (Runstate assoc nbassoc f cycle) + (Vblock lhs rhs) + (Runstate assoc nbassoc' f cycle). + Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => do s' <- stmnt_run s st; @@ -396,8 +454,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value. Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with - | OK (State assoc nbassoc f c) => - OK (State (merge_assoclist nbassoc assoc) empty_assoclist f c) + | OK (Runstate assoc nbassoc f c) => + OK (Runstate (merge_assoclist nbassoc assoc) empty_assoclist f c) | Error msg => Error msg end. @@ -406,19 +464,25 @@ Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : na match n with | S n' => do assoc' <- mi_run f assoc m n'; - match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with - | OK (State assoc _ _ _) => OK assoc + match mi_step_commit (Runstate assoc' empty_assoclist f (Pos.of_nat n')) m with + | OK (Runstate 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 => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist) + | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist) + end. + Definition module_run (n : nat) (m : module) : res assoclist := - let f := fun x => match x with - | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist) - | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist) - end in - mi_run f empty_assoclist (mod_body m) n. + mi_run (initial_fextclk m) empty_assoclist (mod_body m) n. Local Close Scope error_monad_scope. @@ -459,4 +523,19 @@ Proof. assumption. Qed. -*) + *) + +Inductive initial_state (m: module): state -> Prop := +| initial_state_intro: + initial_state m (Runstate empty_assoclist empty_assoclist (initial_fextclk m) xH). + +(** A final state is a [Returnstate] with an empty call stack. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate nil (Vint r) m) r. + +(** The small-step semantics for a module. *) + +Definition semantics (p: module) := + Semantics step (initial_state p) final_state (Genv.globalenv p). -- cgit From 57d74093a19569b9dd55520c6a1548e4827f3b1e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Apr 2020 22:16:01 +0100 Subject: Add valueToInt function --- src/verilog/Value.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index fe53dbc..241534c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -78,6 +78,9 @@ Definition uvalueToZ (v : value) : Z := Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). +Definition valueToInt (i : value) : Integers.int := + Int.repr (valueToZ i). + (** 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 -- cgit From eee95c4fe9f8b0e1d24224f9c980c16156d9b80d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Apr 2020 22:16:15 +0100 Subject: Add CompCert semantics for Verilog --- src/verilog/Verilog.v | 233 ++++++++++++++++++++++++++++++++------------------ 1 file changed, 152 insertions(+), 81 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 4ad297b..a4504c2 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -28,9 +28,8 @@ From Coq Require Import Import ListNotations. From coqup Require Import common.Coquplib common.Show verilog.Value. - -From compcert Require Integers. -From compcert Require Import Errors. +From compcert Require Integers Events. +From compcert Require Import Errors Smallstep Globalenvs. Notation "a ! b" := (PositiveMap.find b a) (at level 1). @@ -157,6 +156,7 @@ Record module : Type := mkmodule { mod_clk : szreg; mod_finish : szreg; mod_return : szreg; + mod_state : szreg; (**r Variable that defines the current state, it should be internal. *) mod_args : list szreg; mod_body : list module_item; }. @@ -172,12 +172,40 @@ Coercion Vvar : reg >-> expr. Definition fext := PositiveMap.t value. Definition fextclk := nat -> fext. -Inductive state: Type := - Runstate: - forall (assoc : assoclist) +(** ** State + +The [state] contains the following items: + +- 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 state : Type := +| Runstate: + forall (m : module) + (mi : module_item) + (mis : list module_item) + (assoc : assoclist) (nbassoc : assoclist) (f : fextclk) - (cycle : positive), + (cycle : nat) + (pc : positive), + state +| Finishstate: + forall v : value, state. Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := @@ -212,40 +240,41 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : state -> expr -> value -> Prop := +Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := | erun_Vlit : - forall s v, - expr_runp s (Vlit v) v + forall fext assoc v, + expr_runp fext assoc (Vlit v) v | erun_Vvar : - forall assoc na f c v r, + forall fext assoc v r, assoc!r = Some v -> - expr_runp (Runstate assoc na f c) (Vvar r) v + expr_runp fext assoc (Vvar r) v | erun_Vinputvar : - forall s r v, - expr_runp s (Vinputvar r) v + forall fext assoc r v, + fext!r = Some v -> + expr_runp fext assoc (Vinputvar r) v | erun_Vbinop : - forall s op l r lv rv oper EQ, - expr_runp s l lv -> - expr_runp s r rv -> + forall fext assoc op l r lv rv oper EQ, + expr_runp fext assoc l lv -> + expr_runp fext assoc r rv -> oper = binop_run op -> - expr_runp s (Vbinop op l r) (oper lv rv EQ) + expr_runp fext assoc (Vbinop op l r) (oper lv rv EQ) | erun_Vunop : - forall s u vu op oper, - expr_runp s u vu -> + forall fext assoc u vu op oper, + expr_runp fext assoc u vu -> oper = unop_run op -> - expr_runp s (Vunop op u) (oper vu) + expr_runp fext assoc (Vunop op u) (oper vu) | erun_Vternary_true : - forall s c ts fs vc vt, - expr_runp s c vc -> - expr_runp s ts vt -> + forall fext assoc c ts fs vc vt, + expr_runp fext assoc c vc -> + expr_runp fext assoc ts vt -> valueToBool vc = true -> - expr_runp s (Vternary c ts fs) vt + expr_runp fext assoc (Vternary c ts fs) vt | erun_Vternary_false : - forall s c ts fs vc vf, - expr_runp s c vc -> - expr_runp s fs vf -> + forall fext assoc c ts fs vc vf, + expr_runp fext assoc c vc -> + expr_runp fext assoc fs vf -> valueToBool vc = false -> - expr_runp s (Vternary c ts fs) vf. + expr_runp fext assoc (Vternary c ts fs) vf. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -263,22 +292,20 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. -Definition access_fext (s : state) (r : reg) : res value := - match s with - | Runstate _ _ f c => - match PositiveMap.find r (f (Pos.to_nat c)) with - | Some v => OK v - | _ => OK (ZToValue 1 0) - end +Definition access_fext (f : fext) (r : reg) : res value := + match PositiveMap.find r f with + | Some v => OK v + | _ => OK (ZToValue 1 0) end. (* TODO FIX Vvar case without default *) -Fixpoint expr_run (s : state) (e : expr) +(*Fixpoint expr_run (assoc : assoclist) (e : expr) {struct e} : res value := match e with | Vlit v => OK v | Vvar r => match s with - | Runstate assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | Runstate _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | _ => Error (msg "Verilog: Wrong state") end | Vinputvar r => access_fext s r | Vbinop op l r => @@ -296,7 +323,7 @@ Fixpoint expr_run (s : state) (e : expr) | Vternary c te fe => do cv <- expr_run s c; if valueToBool cv then expr_run s te else expr_run s fe - end. + end.*) (** Return the name of the lhs of an assignment. For now, this function is quite simple because only assignment to normal variables is supported and needed. *) @@ -307,7 +334,7 @@ Definition assign_name (e : expr) : res reg := | _ => Error (msg "Verilog: expression not supported on lhs of assignment") end. -Fixpoint stmnt_height (st : stmnt) {struct st} : nat := +(*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)) @@ -354,31 +381,38 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := end | Vblock lhs rhs => match s with - | Runstate assoc nbassoc f c => + | Runstate m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (Runstate (PositiveMap.add name rhse assoc) nbassoc f c) + OK (Runstate m (PositiveMap.add name rhse assoc) nbassoc f c) + | _ => Error (msg "Verilog: Wrong state") end | Vnonblock lhs rhs => match s with - | Runstate assoc nbassoc f c => + | Runstate m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (Runstate assoc (PositiveMap.add name rhse nbassoc) f c) + OK (Runstate 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. + stmnt_run' (stmnt_height st) s st. *) -Inductive not_matched (s : state) (caseval : value) (curr : expr * stmnt) : Prop := +Inductive not_matched : state -> value -> expr * stmnt -> Prop := not_in: - forall currval, - expr_runp s (fst curr) currval -> + forall caseval curr currval m mi c assoc nbassoc f cycle pc, + expr_runp (f cycle) assoc (fst curr) currval -> caseval <> currval -> - not_matched s caseval curr. + not_matched (Runstate 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 (Runstate m mi c assoc nbassoc f cycle pc) (f cycle, assoc). Inductive stmnt_runp: state -> stmnt -> state -> Prop := | stmnt_run_Vskip: @@ -389,49 +423,53 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := stmnt_runp s1 st2 s2 -> stmnt_runp s0 (Vseq st1 st2) s2 | stmnt_runp_Vcond_true: - forall s0 s1 c vc stt stf, - expr_runp s0 c vc -> + forall s0 f assoc s1 c vc stt stf, + state_fext_assoc s0 (f, assoc) -> + expr_runp f assoc c vc -> valueToBool vc = true -> stmnt_runp s0 stt s1 -> stmnt_runp s0 (Vcond c stt stf) s1 | stmnt_runp_Vcond_false: - forall s0 s1 c vc stt stf, - expr_runp s0 c vc -> + forall s0 f assoc s1 c vc stt stf, + state_fext_assoc s0 (f, assoc) -> + expr_runp f assoc c vc -> valueToBool vc = false -> stmnt_runp s0 stf s1 -> stmnt_runp s0 (Vcond c stt stf) s1 | stmnt_runp_Vcase: - forall e ve s0 s1 me mve sc clst def, - expr_runp s0 e ve -> - expr_runp s0 me mve -> + forall e ve s0 f assoc s1 me mve sc clst 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_Vcase_default: - forall s0 st s1 e ve clst, - expr_runp s0 e ve -> + forall s0 f assoc st s1 e ve clst, + 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_Vblock: - forall lhs name rhs rhsval s assoc assoc' nbassoc f cycle, + forall lhs name rhs rhsval m mi c assoc assoc' nbassoc f cycle pc, assign_name lhs = OK name -> - expr_runp s rhs rhsval -> + expr_runp (f cycle) assoc rhs rhsval -> assoc' = (PositiveMap.add name rhsval assoc) -> - stmnt_runp (Runstate assoc nbassoc f cycle) + stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc) (Vblock lhs rhs) - (Runstate assoc' nbassoc f cycle) + (Runstate m mi c assoc' nbassoc f cycle pc) | stmnt_runp_Vnonblock: - forall lhs name rhs rhsval s assoc nbassoc nbassoc' f cycle, + forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc, assign_name lhs = OK name -> - expr_runp s rhs rhsval -> + expr_runp (f cycle) assoc rhs rhsval -> nbassoc' = (PositiveMap.add name rhsval nbassoc) -> - stmnt_runp (Runstate assoc nbassoc f cycle) + stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc) (Vblock lhs rhs) - (Runstate assoc nbassoc' f cycle). + (Runstate m mi c assoc nbassoc' f cycle pc). -Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := +(*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 @@ -442,7 +480,24 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := | (Valways_comb _ st)::ls => run st ls | (Vdecl _ _)::ls => mi_step s ls | nil => OK s - end. + end.*) + +Inductive mi_stepp : state -> module_item -> state -> Prop := +| mi_stepp_Valways : + forall s0 st s1 c, + stmnt_runp s0 st s1 -> + mi_stepp s0 (Valways c st) s1 +| mi_stepp_Valways_ff : + forall s0 st s1 c, + stmnt_runp s0 st s1 -> + mi_stepp s0 (Valways_ff c st) s1 +| mi_stepp_Valways_comb : + forall s0 st s1 c, + stmnt_runp s0 st s1 -> + mi_stepp s0 (Valways_comb c st) s1 +| mi_stepp_Vdecl : + forall s lhs rhs, + mi_stepp s (Vdecl lhs rhs) s. Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := PositiveMap.add r v assoc. @@ -452,14 +507,15 @@ Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist := Definition empty_assoclist : assoclist := PositiveMap.empty value. -Definition mi_step_commit (s : state) (m : list module_item) : res state := +(*Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with - | OK (Runstate assoc nbassoc f c) => - OK (Runstate (merge_assoclist nbassoc assoc) empty_assoclist f c) + | OK (Runstate m assoc nbassoc f c) => + OK (Runstate m (merge_assoclist nbassoc assoc) empty_assoclist f c) | Error msg => Error msg - end. + | _ => Error (msg "Verilog: Wrong state") + end.*) -Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat) +(*Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat) {struct n} : res assoclist := match n with | S n' => @@ -469,7 +525,7 @@ Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : na | Error m => Error m end | O => OK assoc - end. + 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 @@ -481,8 +537,8 @@ Definition initial_fextclk (m : module) : fextclk := | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist) end. -Definition module_run (n : nat) (m : module) : res assoclist := - mi_run (initial_fextclk m) empty_assoclist (mod_body m) n. +(*Definition module_run (n : nat) (m : module) : res assoclist := + mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.*) Local Close Scope error_monad_scope. @@ -525,17 +581,32 @@ Qed. *) +Definition genv := Genv.t unit unit. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := +| step_module : + forall g m mi hmi tmi assoc nbassoc f cycle pc e, + step g (Runstate m mi (hmi::tmi) assoc nbassoc f cycle pc) e + (Runstate 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 g (Runstate m mi nil assoc nbassoc f cycle pc) e + (Runstate m hmi tmi assoc nbassoc f (S cycle) pc). + Inductive initial_state (m: module): state -> Prop := | initial_state_intro: - initial_state m (Runstate empty_assoclist empty_assoclist (initial_fextclk m) xH). + forall hmi tmi, + hmi::tmi = mod_body m -> + initial_state m (Runstate m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH). (** A final state is a [Returnstate] with an empty call stack. *) -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall r m, - final_state (Returnstate nil (Vint r) m) r. +Inductive final_state: state -> Integers.int -> Prop := + | final_state_intro: forall v, + final_state (Finishstate v) (valueToInt v). (** The small-step semantics for a module. *) Definition semantics (p: module) := - Semantics step (initial_state p) final_state (Genv.globalenv p). + Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil). -- cgit From 8f370a52a5424389d9f0b4b044020932a2febfd4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 3 May 2020 17:12:09 +0100 Subject: Change to State --- src/verilog/Verilog.v | 43 ++++++++++++++++++++++--------------------- 1 file changed, 22 insertions(+), 21 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index a4504c2..7a3982c 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -194,7 +194,7 @@ retrieved and set appropriately. of the Verilog that should match with the RTL. *) Inductive state : Type := -| Runstate: +| State: forall (m : module) (mi : module_item) (mis : list module_item) @@ -304,7 +304,7 @@ Definition access_fext (f : fext) (r : reg) : res value := match e with | Vlit v => OK v | Vvar r => match s with - | Runstate _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r | _ => Error (msg "Verilog: Wrong state") end | Vinputvar r => access_fext s r @@ -381,18 +381,18 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := end | Vblock lhs rhs => match s with - | Runstate m assoc nbassoc f c => + | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (Runstate m (PositiveMap.add name rhse assoc) nbassoc f c) + OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) | _ => Error (msg "Verilog: Wrong state") end | Vnonblock lhs rhs => match s with - | Runstate m assoc nbassoc f c => + | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (Runstate m assoc (PositiveMap.add name rhse nbassoc) f c) + OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) | _ => Error (msg "Verilog: Wrong state") end end @@ -407,12 +407,12 @@ Inductive not_matched : state -> value -> expr * stmnt -> Prop := forall caseval curr currval m mi c assoc nbassoc f cycle pc, expr_runp (f cycle) assoc (fst curr) currval -> caseval <> currval -> - not_matched (Runstate m mi c assoc nbassoc f cycle pc) caseval curr. + 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 (Runstate m mi c assoc nbassoc f cycle pc) (f cycle, assoc). + state_fext_assoc (State m mi c assoc nbassoc f cycle pc) (f cycle, assoc). Inductive stmnt_runp: state -> stmnt -> state -> Prop := | stmnt_run_Vskip: @@ -457,17 +457,17 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := assign_name lhs = OK name -> expr_runp (f cycle) assoc rhs rhsval -> assoc' = (PositiveMap.add name rhsval assoc) -> - stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc) + stmnt_runp (State m mi c assoc nbassoc f cycle pc) (Vblock lhs rhs) - (Runstate m mi c assoc' nbassoc f cycle pc) + (State m mi c assoc' nbassoc f cycle pc) | stmnt_runp_Vnonblock: forall lhs name rhs rhsval m mi 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 (Runstate m mi c assoc nbassoc f cycle pc) + stmnt_runp (State m mi c assoc nbassoc f cycle pc) (Vblock lhs rhs) - (Runstate m mi c assoc nbassoc' f cycle pc). + (State m mi c assoc nbassoc' f cycle pc). (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => @@ -509,8 +509,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value. (*Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with - | OK (Runstate m assoc nbassoc f c) => - OK (Runstate m (merge_assoclist nbassoc assoc) empty_assoclist f c) + | OK (State m assoc nbassoc f c) => + OK (State m (merge_assoclist nbassoc assoc) empty_assoclist f c) | Error msg => Error msg | _ => Error (msg "Verilog: Wrong state") end.*) @@ -520,8 +520,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value. match n with | S n' => do assoc' <- mi_run f assoc m n'; - match mi_step_commit (Runstate assoc' empty_assoclist f (Pos.of_nat n')) m with - | OK (Runstate assoc _ _ _) => OK assoc + match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with + | OK (State assoc _ _ _) => OK assoc | Error m => Error m end | O => OK assoc @@ -583,22 +583,23 @@ Qed. Definition genv := Genv.t unit unit. + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall g m mi hmi tmi assoc nbassoc f cycle pc e, - step g (Runstate m mi (hmi::tmi) assoc nbassoc f cycle pc) e - (Runstate m hmi tmi assoc nbassoc f cycle pc) + 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 g (Runstate m mi nil assoc nbassoc f cycle pc) e - (Runstate m hmi tmi assoc nbassoc f (S cycle) pc). + 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 := | initial_state_intro: forall hmi tmi, hmi::tmi = mod_body m -> - initial_state m (Runstate m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH). + initial_state m (State m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH). (** A final state is a [Returnstate] with an empty call stack. *) -- cgit From 7ee0ca8263632536582646eb83b909f78f9e6fe4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 3 May 2020 17:12:25 +0100 Subject: Add hex notation to values --- src/verilog/Value.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 241534c..1d31110 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -18,6 +18,7 @@ (* begin hide *) From bbv Require Import Word. +From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith. From compcert Require Import lib.Integers. (* end hide *) @@ -211,3 +212,11 @@ Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz 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. -- cgit From 0b118f8dca9068e0075e72f4d0c24cf707df44c7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 3 May 2020 17:13:56 +0100 Subject: Add code to debug execution of HLS --- src/verilog/Test.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 src/verilog/Test.v (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v new file mode 100644 index 0000000..7a31865 --- /dev/null +++ b/src/verilog/Test.v @@ -0,0 +1,73 @@ +From coqup Require Import Verilog Veriloggen Coquplib Value. +From compcert Require Import AST Errors Maps Op Integers. +From compcert Require RTL. +From Coq Require Import FSets.FMapPositive. +Import ListNotations. +Import HexNotationValue. +Local Open Scope word_scope. + +Definition test_module : module := + let mods := [ + Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5))) + (Vnonblock (Vvar 7%positive) + (Vvar 6%positive))) + ] in + mkmodule (1%positive, 1%nat) + (2%positive, 1%nat) + (3%positive, 1%nat) + (4%positive, 1%nat) + (5%positive, 32%nat) + (6%positive, 32%nat) + nil + mods. + +Definition test_input : RTL.function := + let sig := mksignature nil Tvoid cc_default in + let params := nil in + let stacksize := 0 in + let entrypoint := 3%positive in + let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive)) + (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive) + (PTree.empty RTL.instruction)) in + RTL.mkfunction sig params stacksize code entrypoint. + +Definition test_input_program : RTL.program := + mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive. + +Compute transf_program test_input_program. + +Definition test_output_module : module := + {| mod_start := (4%positive, 1%nat); + mod_reset := (5%positive, 1%nat); + mod_clk := (6%positive, 1%nat); + mod_finish := (2%positive, 1%nat); + mod_return := (3%positive, 32%nat); + mod_state := (7%positive, 32%nat); + mod_args := []; + mod_body := + [Valways_ff (Vposedge 6%positive) + (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1")) + (Vnonblock (Vvar 7%positive) (32'h"3")) + (Vcase (Vvar 7%positive) + [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1")); + (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))] + (Some Vskip))); + Valways_ff (Vposedge 6%positive) + (Vcase (Vvar 7%positive) + [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1"))) + (Vblock (Vvar 3%positive) (Vvar 1%positive))); + (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))] + (Some Vskip)); + Vdecl 1%positive 32; Vdecl 7%positive 32] |}. + +Lemma valid_test_output : + transf_program test_input_program = OK test_output_module. +Proof. trivial. Qed. + +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). -- cgit 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 From 5cfa4af9c6e4d9703e3142c24ae78c7da0ac575f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 4 May 2020 16:13:16 +0100 Subject: Add equality check for value --- src/verilog/Value.v | 36 +++++++++++++++++++++--------------- src/verilog/Verilog.v | 2 +- 2 files changed, 22 insertions(+), 16 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 21e59be..4cacab5 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz * @@ -149,24 +149,30 @@ 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. +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. -Definition valueEqCheck (sz : nat) (x y : word sz) : +Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. +Proof. apply nevalue. Qed. + +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 (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 _ + | left eq => left (eqvaluef x y eq) + | right ne => right (nevaluef x y ne) end. (** Arithmetic operations over [value], interpreting them as signed or unsigned diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index a927eac..756dc12 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz * -- cgit From 2df5dc835efa3ac7552363e81ef9af5d3145cc7e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 00:19:27 +0100 Subject: Finish manual simulation --- src/verilog/Test.v | 44 +++++++++++++++++++++++++++++++++++++++++++- src/verilog/Value.v | 29 +++++++++++++++++++++++++---- 2 files changed, 68 insertions(+), 5 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 5c22ef2..5fd6d07 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -1,9 +1,30 @@ +(* + * CoqUp: 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 coqup Require Import Verilog Veriloggen Coquplib Value. From compcert Require Import AST Errors Maps Op Integers. From compcert Require RTL. From Coq Require Import FSets.FMapPositive. +From bbv Require Import Word. Import ListNotations. Import HexNotationValue. +Import WordScope. + Local Open Scope word_scope. Definition test_module : module := @@ -60,6 +81,8 @@ Definition test_output_module : module := (Some Vskip)); Vdecl 1%positive 32; Vdecl 7%positive 32] |}. +Search (_ <> _ -> _ = _). + Lemma valid_test_output : transf_program test_input_program = OK test_output_module. Proof. trivial. Qed. @@ -95,4 +118,23 @@ Proof. apply get_state_fext_assoc. apply erun_Vvar_empty. auto. apply erun_Vlit. - unfold ZToValue. instantiate (1 := 32%nat). simpl. + unfold ZToValue. instantiate (1 := 32%nat). simpl. apply nevalue. simpl. + apply weqb_false. simpl. trivial. + 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. apply nevalue. simpl. + apply weqb_false. simpl. trivial. + eapply stmnt_runp_Vcase_default. + apply get_state_fext_assoc. + apply erun_Vvar_empty. auto. + apply stmnt_run_Vskip. + eapply mis_stepp_Cons. + apply mi_stepp_Vdecl. + eapply mis_stepp_Cons. + apply mi_stepp_Vdecl. + apply mis_stepp_Nil. + Unshelve. + exact 0%nat. +Qed. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 4cacab5..39d1832 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -103,8 +103,8 @@ Definition boolToValue (sz : nat) (b : bool) : value := 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. Defined. +Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +intros; subst; assumption. Defined. Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. @@ -149,7 +149,6 @@ 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. split; intros. @@ -168,13 +167,35 @@ Qed. Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. Proof. apply nevalue. Qed. -Definition valueEq (sz : nat) (x y : word sz) : +(*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. + +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). + Admitted. + (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. -- cgit From 5d4aed9030565349a83f9ede4bd35c020eb416b5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 00:38:19 +0100 Subject: Simplifications to proof --- src/verilog/Test.v | 21 +++++++-------------- src/verilog/Value.v | 2 -- src/verilog/Verilog.v | 10 ++++++++-- 3 files changed, 15 insertions(+), 18 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 5fd6d07..9e13bf6 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -95,20 +95,14 @@ Lemma manual_simulation : (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")). + eapply step_module; auto. + eapply mis_stepp_Cons; auto. apply mi_stepp_Valways_ff. - apply stmnt_runp_Vcond_true with (f := test_fextclk 1%nat) - (assoc := empty_assoclist) - (vc := 1'h"1"); auto. + eapply stmnt_runp_Vcond_true; 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 erun_Vbinop; auto. + apply erun_Vinputvar; simpl. auto. + apply erun_Vlit. simpl. unfold ZToValue. simpl. instantiate (1 := eq_refl (vsize (1'h"1"))). auto. eapply stmnt_runp_Vnonblock. simpl. auto. apply erun_Vlit. auto. @@ -135,6 +129,5 @@ Proof. eapply mis_stepp_Cons. apply mi_stepp_Vdecl. apply mis_stepp_Nil. - Unshelve. - exact 0%nat. + auto. Unshelve. exact 0%nat. Qed. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 39d1832..61f2652 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -101,8 +101,6 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) -Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. - Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. intros; subst; assumption. Defined. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 756dc12..399bff7 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -281,6 +281,7 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := expr_runp fext assoc fs vf -> valueToBool vc = false -> expr_runp fext assoc (Vternary c ts fs) vf. +Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -412,11 +413,12 @@ Inductive state_fext_assoc : state -> fext * assoclist -> Prop := | get_state_fext_assoc : forall c assoc nbassoc f cycle pc, state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc). +Hint Constructors state_fext_assoc : verilog. Inductive stmnt_runp: state -> stmnt -> state -> Prop := -| stmnt_run_Vskip: +| stmnt_runp_Vskip: forall s, stmnt_runp s Vskip s -| stmnt_run_Vseq: +| stmnt_runp_Vseq: forall st1 st2 s0 s1 s2, stmnt_runp s0 st1 s1 -> stmnt_runp s1 st2 s2 -> @@ -473,6 +475,7 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := stmnt_runp (State c assoc nbassoc f cycle pc) (Vnonblock lhs rhs) (State c assoc nbassoc' f cycle pc). +Hint Constructors stmnt_runp : verilog. (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => @@ -503,6 +506,7 @@ Inductive mi_stepp : state -> module_item -> state -> Prop := | mi_stepp_Vdecl : forall s lhs rhs, mi_stepp s (Vdecl lhs rhs) s. +Hint Constructors mi_stepp : verilog. Inductive mis_stepp : state -> list module_item -> state -> Prop := | mis_stepp_Cons : @@ -513,6 +517,7 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop := | mis_stepp_Nil : forall s, mis_stepp s nil s. +Hint Constructors mis_stepp : verilog. Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := PositiveMap.add r v assoc. @@ -614,6 +619,7 @@ Inductive step : state -> state -> Prop := assoc!(fst m.(mod_return)) = Some result -> step (State m assoc empty_assoclist f cycle stvar) (Finishstate result). +Hint Constructors step : verilog. (*Inductive initial_state (m: module): state -> Prop := | initial_state_intro: -- cgit From 4d409fe68c693dd083295f35bd5af8bdec6d2632 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 01:16:03 +0100 Subject: Minimised manual simulation --- src/verilog/Test.v | 39 ++++----------------------------------- src/verilog/Verilog.v | 20 ++++++++++---------- 2 files changed, 14 insertions(+), 45 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 9e13bf6..d94467d 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -95,39 +95,8 @@ Lemma manual_simulation : (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist) empty_assoclist test_fextclk 2 (32'h"3")). Proof. - eapply step_module; auto. - eapply mis_stepp_Cons; auto. - apply mi_stepp_Valways_ff. - eapply stmnt_runp_Vcond_true; auto. - apply get_state_fext_assoc. - eapply erun_Vbinop; auto. - apply erun_Vinputvar; simpl. auto. - apply erun_Vlit. simpl. unfold ZToValue. simpl. instantiate (1 := eq_refl (vsize (1'h"1"))). auto. - 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. apply nevalue. simpl. - apply weqb_false. simpl. trivial. - 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. apply nevalue. simpl. - apply weqb_false. simpl. trivial. - eapply stmnt_runp_Vcase_default. - apply get_state_fext_assoc. - apply erun_Vvar_empty. auto. - apply stmnt_run_Vskip. - eapply mis_stepp_Cons. - apply mi_stepp_Vdecl. - eapply mis_stepp_Cons. - apply mi_stepp_Vdecl. - apply mis_stepp_Nil. - auto. Unshelve. exact 0%nat. + repeat (econstructor; eauto); + try (simpl; unfold ZToValue; simpl; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); + apply nevalue; apply weqb_false; trivial. + Unshelve. exact 0%nat. Qed. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 399bff7..451b452 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v - | erun_Vvar : - 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_Vvar : + forall fext assoc v r, + assoc!r = Some v -> + expr_runp fext assoc (Vvar r) v | erun_Vinputvar : forall fext assoc r v, fext!r = Some v -> @@ -437,21 +437,21 @@ 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_match: +| 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 sc s1 -> + mve <> ve -> + stmnt_runp s0 (Vcase e cs def) s1 -> stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 -| stmnt_runp_Vcase_nomatch: +| 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 -> - stmnt_runp s0 (Vcase e cs def) s1 -> + mve = ve -> + stmnt_runp s0 sc s1 -> stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 | stmnt_runp_Vcase_default: forall s0 f assoc st s1 e ve, -- cgit From d530dc044242efdd4c5fafe13456cd05ac65beee Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 01:20:58 +0100 Subject: Refine test file --- src/verilog/Test.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index d94467d..5cd6ec4 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -81,8 +81,6 @@ Definition test_output_module : module := (Some Vskip)); Vdecl 1%positive 32; Vdecl 7%positive 32] |}. -Search (_ <> _ -> _ = _). - Lemma valid_test_output : transf_program test_input_program = OK test_output_module. Proof. trivial. Qed. @@ -96,7 +94,6 @@ Lemma manual_simulation : empty_assoclist test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); - try (simpl; unfold ZToValue; simpl; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); - apply nevalue; apply weqb_false; trivial. - Unshelve. exact 0%nat. + try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); + apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat. Qed. -- cgit From 74ac24f8dc099cc558d3b03b2f9303c89048f519 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 6 May 2020 11:49:32 +0100 Subject: Add changes to value --- src/verilog/Value.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 61f2652..8a0716d 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -186,13 +186,20 @@ Definition valueeqb (x y : value) : bool := | 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). - Admitted. + unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. + - destruct v1, v2. simpl in H. (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. -- cgit From c8535e1f454c7014c7b794fc8be343e2fda97937 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 17:21:51 +0100 Subject: Rename assoclist to assocset --- src/verilog/Test.v | 6 +++--- src/verilog/Verilog.v | 50 +++++++++++++++++++++++++------------------------- 2 files changed, 28 insertions(+), 28 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 5cd6ec4..f24612e 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -88,10 +88,10 @@ Proof. trivial. Qed. Definition test_fextclk := initial_fextclk test_output_module. Lemma manual_simulation : - step (State test_output_module empty_assoclist empty_assoclist + step (State test_output_module empty_assocset empty_assocset 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")). + (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset) + empty_assocset test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 451b452..a35fb58 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -39,7 +39,7 @@ Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. -Definition assoclist : Type := PositiveMap.t value. +Definition assocset : Type := PositiveMap.t value. (** * Verilog AST @@ -52,7 +52,7 @@ 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. *) -Definition estate : Type := assoclist * assoclist. +Definition estate : Type := assocset * assocset. (** ** Binary Operators @@ -198,8 +198,8 @@ retrieved and set appropriately. Inductive state : Type := | State: forall (m : module) - (assoc : assoclist) - (nbassoc : assoclist) + (assoc : assocset) + (nbassoc : assocset) (f : fextclk) (cycle : nat) (stvar : value), @@ -240,7 +240,7 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := +Inductive expr_runp : fext -> assocset -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v @@ -306,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value := end. (* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assoclist) (e : expr) +(*Fixpoint expr_run (assoc : assocset) (e : expr) {struct e} : res value := match e with | Vlit v => OK v @@ -409,7 +409,7 @@ 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 state_fext_assoc : state -> fext * assoclist -> Prop := +Inductive state_fext_assoc : state -> fext * assocset -> Prop := | get_state_fext_assoc : forall c assoc nbassoc f cycle pc, state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc). @@ -519,28 +519,28 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop := mis_stepp s nil s. Hint Constructors mis_stepp : verilog. -Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := +Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset := PositiveMap.add r v assoc. -Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist := - PositiveMap.fold add_assoclist nbassoc assoc. +Definition merge_assocset (nbassoc assoc : assocset) : assocset := + PositiveMap.fold add_assocset nbassoc assoc. -Definition empty_assoclist : assoclist := PositiveMap.empty value. +Definition empty_assocset : assocset := PositiveMap.empty value. (*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_assoclist nbassoc assoc) empty_assoclist f c) + OK (State m (merge_assocset nbassoc assoc) empty_assocset f c) | Error msg => Error msg | _ => Error (msg "Verilog: Wrong state") end.*) -(*Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat) - {struct n} : res assoclist := +(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat) + {struct n} : res assocset := match n with | S n' => do assoc' <- mi_run f assoc m n'; - match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with + match mi_step_commit (State assoc' empty_assocset f (Pos.of_nat n')) m with | OK (State assoc _ _ _) => OK assoc | Error m => Error m end @@ -553,12 +553,12 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist) - | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist) + | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset) + | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset) end. -(*Definition module_run (n : nat) (m : module) : res assoclist := - mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.*) +(*Definition module_run (n : nat) (m : module) : res assocset := + mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*) Local Close Scope error_monad_scope. @@ -606,18 +606,18 @@ Definition genv := Genv.t unit unit. Inductive step : state -> state -> Prop := | step_module : forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc, - mis_stepp (State m assoc0 empty_assoclist f cycle stvar) + mis_stepp (State m assoc0 empty_assocset f cycle stvar) m.(mod_body) (State m assoc1 nbassoc f cycle stvar) -> - assoc2 = merge_assoclist nbassoc assoc1 -> + assoc2 = merge_assocset 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 (State m assoc0 empty_assocset f cycle stvar) + (State m assoc2 empty_assocset 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) + step (State m assoc empty_assocset f cycle stvar) (Finishstate result). Hint Constructors step : verilog. @@ -625,7 +625,7 @@ Hint Constructors step : verilog. | initial_state_intro: forall hmi tmi, hmi::tmi = mod_body m -> - initial_state m (State m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH). + initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH). (** A final state is a [Returnstate] with an empty call stack. *) -- cgit From fa39e09d403cfba1b1e6c359362e54600dfc28b0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 23:12:59 +0100 Subject: Use associations instead of state --- src/verilog/Value.v | 4 ++ src/verilog/Verilog.v | 135 ++++++++++++++++++++++++-------------------------- 2 files changed, 69 insertions(+), 70 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 8a0716d..a96d67c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -200,6 +200,10 @@ 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. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index a35fb58..ba7e83d 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -41,6 +41,12 @@ Definition szreg : Type := reg * nat. Definition assocset : Type := PositiveMap.t value. +Record associations : Type := + mkassociations { + assoc_blocking : assocset; + assoc_nonblocking : assocset + }. + (** * Verilog AST The Verilog AST is defined here, which is the target language of the @@ -409,72 +415,61 @@ 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 state_fext_assoc : state -> fext * assocset -> Prop := -| get_state_fext_assoc : - forall c assoc nbassoc f cycle pc, - state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc). -Hint Constructors state_fext_assoc : verilog. - -Inductive stmnt_runp: state -> stmnt -> state -> Prop := +Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := | stmnt_runp_Vskip: - forall s, stmnt_runp s Vskip s + forall f a, stmnt_runp f a Vskip a | stmnt_runp_Vseq: - forall st1 st2 s0 s1 s2, - stmnt_runp s0 st1 s1 -> - stmnt_runp s1 st2 s2 -> - stmnt_runp s0 (Vseq st1 st2) s2 + forall f st1 st2 as0 as1 as2, + stmnt_runp f as0 st1 as1 -> + stmnt_runp f as1 st2 as2 -> + stmnt_runp f as0 (Vseq st1 st2) as2 | stmnt_runp_Vcond_true: - forall s0 f assoc s1 c vc stt stf, - state_fext_assoc s0 (f, assoc) -> - expr_runp f assoc c vc -> + forall as0 as1 f c vc stt stf, + expr_runp f as0.(assoc_blocking) c vc -> valueToBool vc = true -> - stmnt_runp s0 stt s1 -> - stmnt_runp s0 (Vcond c stt stf) s1 + stmnt_runp f as0 stt as1 -> + stmnt_runp f as0 (Vcond c stt stf) as1 | stmnt_runp_Vcond_false: - forall s0 f assoc s1 c vc stt stf, - state_fext_assoc s0 (f, assoc) -> - expr_runp f assoc c vc -> + forall as0 as1 f c vc stt stf, + expr_runp f as0.(assoc_blocking) c vc -> valueToBool vc = false -> - stmnt_runp s0 stf s1 -> - stmnt_runp s0 (Vcond c stt stf) s1 + stmnt_runp f as0 stf as1 -> + stmnt_runp f as0 (Vcond c stt stf) as1 | 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 -> + forall e ve as0 f as1 me mve sc cs def, + expr_runp f as0.(assoc_blocking) e ve -> + expr_runp f as0.(assoc_blocking) me mve -> mve <> ve -> - stmnt_runp s0 (Vcase e cs def) s1 -> - stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 + stmnt_runp f as0 (Vcase e cs def) as1 -> + stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1 | 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 -> + forall e ve as0 f as1 me mve sc cs def, + expr_runp f as0.(assoc_blocking) e ve -> + expr_runp f as0.(assoc_blocking) me mve -> mve = ve -> - stmnt_runp s0 sc s1 -> - stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 + stmnt_runp f as0 sc as1 -> + stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1 | stmnt_runp_Vcase_default: - forall s0 f assoc st s1 e ve, - state_fext_assoc s0 (f, assoc) -> - expr_runp f assoc e ve -> - stmnt_runp s0 st s1 -> - stmnt_runp s0 (Vcase e nil (Some st)) s1 + forall as0 as1 f st e ve, + expr_runp f as0.(assoc_blocking) e ve -> + stmnt_runp f as0 st as1 -> + stmnt_runp f as0 (Vcase e nil (Some st)) as1 | stmnt_runp_Vblock: - forall lhs name rhs rhsval c assoc assoc' nbassoc f cycle pc, + forall lhs name rhs rhsval assoc assoc' nbassoc f, assign_name lhs = OK name -> - expr_runp (f cycle) assoc rhs rhsval -> + expr_runp f assoc rhs rhsval -> assoc' = (PositiveMap.add name rhsval assoc) -> - stmnt_runp (State c assoc nbassoc f cycle pc) - (Vblock lhs rhs) - (State c assoc' nbassoc f cycle pc) + stmnt_runp f (mkassociations assoc nbassoc) + (Vblock lhs rhs) + (mkassociations assoc nbassoc) | stmnt_runp_Vnonblock: - forall lhs name rhs rhsval c assoc nbassoc nbassoc' f cycle pc, + forall lhs name rhs rhsval assoc nbassoc nbassoc' f, assign_name lhs = OK name -> - expr_runp (f cycle) assoc rhs rhsval -> + expr_runp f assoc rhs rhsval -> nbassoc' = (PositiveMap.add name rhsval nbassoc) -> - stmnt_runp (State c assoc nbassoc f cycle pc) - (Vnonblock lhs rhs) - (State c assoc nbassoc' f cycle pc). + stmnt_runp f (mkassociations assoc nbassoc) + (Vnonblock lhs rhs) + (mkassociations assoc nbassoc'). Hint Constructors stmnt_runp : verilog. (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := @@ -490,33 +485,33 @@ Hint Constructors stmnt_runp : verilog. | nil => OK s end.*) -Inductive mi_stepp : state -> module_item -> state -> Prop := +Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop := | mi_stepp_Valways : - forall s0 st s1 c, - stmnt_runp s0 st s1 -> - mi_stepp s0 (Valways c st) s1 + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways c st) s1 | mi_stepp_Valways_ff : - forall s0 st s1 c, - stmnt_runp s0 st s1 -> - mi_stepp s0 (Valways_ff c st) s1 + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways_ff c st) s1 | mi_stepp_Valways_comb : - forall s0 st s1 c, - stmnt_runp s0 st s1 -> - mi_stepp s0 (Valways_comb c st) s1 + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways_comb c st) s1 | mi_stepp_Vdecl : - forall s lhs rhs, - mi_stepp s (Vdecl lhs rhs) s. + forall f s lhs rhs, + mi_stepp f s (Vdecl lhs rhs) s. Hint Constructors mi_stepp : verilog. -Inductive mis_stepp : state -> list module_item -> state -> Prop := +Inductive mis_stepp : fext -> associations -> list module_item -> associations -> 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 + forall f mi mis s0 s1 s2, + mi_stepp f s0 mi s1 -> + mis_stepp f s1 mis s2 -> + mis_stepp f s0 (mi :: mis) s2 | mis_stepp_Nil : - forall s, - mis_stepp s nil s. + forall f s, + mis_stepp f s nil s. Hint Constructors mis_stepp : verilog. Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset := @@ -606,9 +601,9 @@ Definition genv := Genv.t unit unit. Inductive step : state -> state -> Prop := | step_module : forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc, - mis_stepp (State m assoc0 empty_assocset f cycle stvar) + mis_stepp (f cycle) (mkassociations assoc0 empty_assocset) m.(mod_body) - (State m assoc1 nbassoc f cycle stvar) -> + (mkassociations assoc1 nbassoc) -> assoc2 = merge_assocset nbassoc assoc1 -> Some stvar' = assoc2!(fst m.(mod_state)) -> step (State m assoc0 empty_assocset f cycle stvar) -- cgit From 4bdabd1828c48e74c6b1f701f57a1b3c421a95fb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 23:13:25 +0100 Subject: Redefine HTL for intermediate Verilog language --- src/verilog/HTL.v | 145 ++++++++++++++++++++++++++---------------------------- 1 file changed, 69 insertions(+), 76 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 1d156ad..3d863b2 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -16,89 +16,82 @@ * along with this program. If not, see . *) -(** 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. - *) - -From coqup.common Require Import Coquplib. - -From compcert Require Import Maps. -From compcert Require Op AST Memory Registers. - -Definition node := positive. - -Definition reg := Registers.reg. +From Coq Require Import FSets.FMapPositive. +From coqup Require Import Coquplib Value. +From coqup Require Verilog. +From compcert Require Events Globalenvs Smallstep Integers. -Definition ident := AST.ident. +Import HexNotationValue. -Inductive instruction : Type := -| Hnop : node -> instruction -| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction - (** [Hnonblock op args res next] Defines a nonblocking assignment to a - register, using the operation defined in Op.v. *) -| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hinst : AST.signature -> ident -> reg -> node -> instruction - (** [Hinst sig fun args rst strt end res next] Defines the start of a - module instantiation, meaning the function will run until the result is - returned. *) -| Htailcall : AST.signature -> ident -> list reg -> instruction -| Hcond : Op.condition -> list reg -> node -> node -> instruction -| Hjumptable : reg -> list node -> instruction -| Hfinish : option reg -> instruction. - -Record inst : Type := - mkinst { - inst_moddecl : ident; - inst_args : list reg - }. +(** 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. *) -Definition code : Type := PTree.t instruction. +Notation "a ! b" := (PositiveMap.find b a) (at level 1). -Definition instances : Type := PTree.t inst. +Definition reg := positive. +Definition node := positive. -Definition empty_instances : instances := PTree.empty inst. +Definition datapath := PositiveMap.t Verilog.stmnt. +Definition controllogic := PositiveMap.t Verilog.stmnt. -(** Function declaration for VTL also contain a construction which describes the - functions that are called in the current function. This information is used - to print out *) -Record module : Type := +Record module: Type := mkmodule { - mod_sig : AST.signature; mod_params : list reg; - mod_stacksize : Z; - mod_code : code; - mod_insts : instances; - mod_entrypoint : node + mod_datapath : datapath; + mod_controllogic : controllogic; + mod_entrypoint : node; + mod_st : reg; + mod_finish : reg; + mod_return : reg }. -Definition moddecl := AST.fundef module. - -Definition design := AST.program moddecl unit. - -Definition modsig (md : moddecl) := - match md with - | AST.Internal m => mod_sig m - | AST.External ef => AST.ef_sig ef - end. - -(** Describes various transformations that can be applied to HTL. This applies - the transformation to each instruction in the function and returns the new - function with the modified instructions. *) -Section TRANSF. - - Variable transf_instr : node -> instruction -> instruction. - - Definition transf_module (m : module) : module := - mkmodule - m.(mod_sig) - m.(mod_params) - m.(mod_stacksize) - (PTree.map transf_instr m.(mod_code)) - m.(mod_insts) - m.(mod_entrypoint). - -End TRANSF. +(** * Operational Semantics *) + +Definition genv := Globalenvs.Genv.t unit unit. +Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil. + +Inductive state : Type := +| State : + forall (m : module) + (st : node) + (assoc : Verilog.assocset), + state +| Returnstate : forall v : value, state. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := +| step_module : + forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f, + m.(mod_controllogic)!st = Some ctrl -> + m.(mod_datapath)!st = Some data -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc0 Verilog.empty_assocset) + ctrl + (Verilog.mkassociations assoc1 nbassoc0) -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc1 nbassoc0) + data + (Verilog.mkassociations assoc2 nbassoc1) -> + assoc3 = Verilog.merge_assocset nbassoc1 assoc2 -> + step g (State m st assoc0) t (State m st assoc3) +| step_finish : + forall g t m st assoc retval, + assoc!(m.(mod_finish)) = Some (1'h"1") -> + assoc!(m.(mod_return)) = Some retval -> + step g (State m st assoc) t (Returnstate retval). +Hint Constructors step : htl. + +Inductive initial_state (m : module) : state -> Prop := +| initial_state_intro : forall st, + st = m.(mod_entrypoint) -> + initial_state m (State m st Verilog.empty_assocset). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + value_int_eqb retval retvali = true -> + final_state (Returnstate retval) retvali. + +Definition semantics (m : module) := + Smallstep.Semantics step (initial_state m) final_state genv_empty. -- cgit From 32990af23915c15e5cfd4cfe32c47cafa508f11d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 May 2020 23:34:15 +0100 Subject: Add AssocMap --- src/verilog/AssocMap.v | 60 ++++++++++++++++++++++++++++++++++++++++++++++ src/verilog/HTL.v | 10 ++++---- src/verilog/Test.v | 6 ++--- src/verilog/Verilog.v | 64 ++++++++++++++++++++------------------------------ 4 files changed, 93 insertions(+), 47 deletions(-) create mode 100644 src/verilog/AssocMap.v (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v new file mode 100644 index 0000000..e550072 --- /dev/null +++ b/src/verilog/AssocMap.v @@ -0,0 +1,60 @@ +(* + * CoqUp: 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 coqup Require Import Coquplib Value. +From Coq Require Import FSets.FMapPositive. + +Definition reg := positive. + +Module AssocMap := PositiveMap. + +Module AssocMapExt. + Import AssocMap. + + Section Operations. + + Variable elt : Type. + + Definition merge : t elt -> t elt -> t elt := fold (@add elt). + + Definition find_default (a : elt) (k : reg) (m : t elt) : elt := + match find k m with + | None => a + | Some v => v + end. + + End Operations. + +End AssocMapExt. +Import AssocMapExt. + +Definition assocmap := AssocMap.t value. + +Definition find_assocmap (n : nat) : reg -> assocmap -> value := + find_default value (ZToValue n 0). + +Definition empty_assocmap : assocmap := AssocMap.empty value. + +Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. + +Module AssocMapNotation. + Notation "a ! b" := (AssocMap.find b a) (at level 1). + Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). + Notation "a # b" := (find_assocmap 32 b a) (at level 1). + Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). +End AssocMapNotation. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 3d863b2..147d24b 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. +From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers. @@ -57,7 +57,7 @@ Inductive state : Type := | State : forall (m : module) (st : node) - (assoc : Verilog.assocset), + (assoc : assocmap), state | Returnstate : forall v : value, state. @@ -67,14 +67,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f - (Verilog.mkassociations assoc0 Verilog.empty_assocset) + (Verilog.mkassociations assoc0 empty_assocmap) ctrl (Verilog.mkassociations assoc1 nbassoc0) -> Verilog.stmnt_runp f (Verilog.mkassociations assoc1 nbassoc0) data (Verilog.mkassociations assoc2 nbassoc1) -> - assoc3 = Verilog.merge_assocset nbassoc1 assoc2 -> + assoc3 = merge_assocmap nbassoc1 assoc2 -> step g (State m st assoc0) t (State m st assoc3) | step_finish : forall g t m st assoc retval, @@ -86,7 +86,7 @@ Hint Constructors step : htl. Inductive initial_state (m : module) : state -> Prop := | initial_state_intro : forall st, st = m.(mod_entrypoint) -> - initial_state m (State m st Verilog.empty_assocset). + initial_state m (State m st empty_assocmap). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, diff --git a/src/verilog/Test.v b/src/verilog/Test.v index f24612e..90c5312 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -88,10 +88,10 @@ Proof. trivial. Qed. Definition test_fextclk := initial_fextclk test_output_module. Lemma manual_simulation : - step (State test_output_module empty_assocset empty_assocset + step (State test_output_module empty_assocmap empty_assocmap test_fextclk 1 (32'h"1")) - (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset) - empty_assocset test_fextclk 2 (32'h"3")). + (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap) + empty_assocmap test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index ba7e83d..c0bce25 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -27,24 +27,21 @@ From Coq Require Import Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value. +From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. Import HexNotationValue. - -Notation "a ! b" := (PositiveMap.find b a) (at level 1). +Import AssocMapNotation. Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. -Definition assocset : Type := PositiveMap.t value. - Record associations : Type := mkassociations { - assoc_blocking : assocset; - assoc_nonblocking : assocset + assoc_blocking : assocmap; + assoc_nonblocking : assocmap }. (** * Verilog AST @@ -58,8 +55,6 @@ 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. *) -Definition estate : Type := assocset * assocset. - (** ** Binary Operators These are the binary operations that can be represented in Verilog. Ideally, @@ -167,8 +162,7 @@ Record module : Type := mkmodule { mod_state : szreg; (**r Variable that defines the current state, it should be internal. *) mod_args : list szreg; mod_body : list module_item; -}. - + }. (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := @@ -204,8 +198,8 @@ retrieved and set appropriately. Inductive state : Type := | State: forall (m : module) - (assoc : assocset) - (nbassoc : assocset) + (assoc : assocmap) + (nbassoc : assocmap) (f : fextclk) (cycle : nat) (stvar : value), @@ -246,7 +240,7 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : fext -> assocset -> expr -> value -> Prop := +Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v @@ -312,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value := end. (* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assocset) (e : expr) +(*Fixpoint expr_run (assoc : assocmap) (e : expr) {struct e} : res value := match e with | Vlit v => OK v @@ -461,7 +455,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := assoc' = (PositiveMap.add name rhsval assoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vblock lhs rhs) - (mkassociations assoc nbassoc) + (mkassociations assoc' nbassoc) | stmnt_runp_Vnonblock: forall lhs name rhs rhsval assoc nbassoc nbassoc' f, assign_name lhs = OK name -> @@ -514,28 +508,20 @@ Inductive mis_stepp : fext -> associations -> list module_item -> associations - mis_stepp f s nil s. Hint Constructors mis_stepp : verilog. -Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset := - PositiveMap.add r v assoc. - -Definition merge_assocset (nbassoc assoc : assocset) : assocset := - PositiveMap.fold add_assocset nbassoc assoc. - -Definition empty_assocset : assocset := PositiveMap.empty value. - (*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_assocset nbassoc assoc) empty_assocset f c) + OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) | Error msg => Error msg | _ => Error (msg "Verilog: Wrong state") - end.*) + end. -(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat) - {struct n} : res assocset := +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_assocset f (Pos.of_nat n')) m with + 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 @@ -548,12 +534,12 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset) - | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset) + | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) end. -(*Definition module_run (n : nat) (m : module) : res assocset := - mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*) +(*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. @@ -601,18 +587,18 @@ Definition genv := Genv.t unit unit. Inductive step : state -> state -> Prop := | step_module : forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc, - mis_stepp (f cycle) (mkassociations assoc0 empty_assocset) + mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap) m.(mod_body) (mkassociations assoc1 nbassoc) -> - assoc2 = merge_assocset nbassoc assoc1 -> + assoc2 = merge_assocmap nbassoc assoc1 -> Some stvar' = assoc2!(fst m.(mod_state)) -> - step (State m assoc0 empty_assocset f cycle stvar) - (State m assoc2 empty_assocset f (S cycle) stvar') + step (State m assoc0 empty_assocmap f cycle stvar) + (State m assoc2 empty_assocmap 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_assocset f cycle stvar) + step (State m assoc empty_assocmap f cycle stvar) (Finishstate result). Hint Constructors step : verilog. @@ -620,7 +606,7 @@ Hint Constructors step : verilog. | initial_state_intro: forall hmi tmi, hmi::tmi = mod_body m -> - initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH). + initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH). (** A final state is a [Returnstate] with an empty call stack. *) -- cgit From 7dbed3811e57479c78e4e82806d343d9285576c1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 May 2020 23:34:36 +0100 Subject: Add lessdef for values --- src/verilog/Value.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index a96d67c..cde98d4 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,8 +19,8 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith. -From compcert Require Import lib.Integers. +From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From compcert Require Import lib.Integers common.Values. (* end hide *) (** * Value @@ -48,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. Definition valueToWord : forall v : value, word (vsize v) := vword. -Definition valueToNat (v : value) : nat := +Definition valueToNat (v :value) : nat := wordToNat (vword v). Definition natToValue sz (n : nat) : value := @@ -284,3 +284,10 @@ Module HexNotationValue. 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', + Integers.Int.unsigned i = valueToZ v' -> + val_value_lessdef (Vint i) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. -- cgit From 333b306421d204e69deb1308352e31ffe53d2287 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:50:37 +0100 Subject: Add theorems about merge --- src/verilog/AssocMap.v | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index e550072..bd61c8e 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -30,14 +30,24 @@ Module AssocMapExt. Variable elt : Type. - Definition merge : t elt -> t elt -> t elt := fold (@add elt). - Definition find_default (a : elt) (k : reg) (m : t elt) : elt := match find k m with | None => a | Some v => v end. + Definition merge : t elt -> t elt -> t elt := fold (@add elt). + + Lemma merge_add_assoc : + forall am am' r v x, + find x (merge (add r v am) am') = find x (add r v (merge am am')). + Admitted. + + Lemma merge_base : + forall am, + merge (empty elt) am = am. + Proof. intros. unfold merge. apply fold_1. Qed. + End Operations. End AssocMapExt. -- cgit From 75c4a7bcad1ffd3ba69a3b514fb71590c7a523c9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:50:58 +0100 Subject: Fix definitions in Value and add lemmas --- src/verilog/Value.v | 42 +++++++++++++++++++++++++++++++++++------- 1 file changed, 35 insertions(+), 7 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index cde98d4..0ce0bc5 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -70,17 +70,14 @@ Definition uvalueToZ (v : value) : Z := uwordToZ (vword v). Definition posToValue sz (p : positive) : value := - mkvalue sz (posToWord sz p). + ZToValue sz (Zpos p). Definition posToValueAuto (p : positive) : value := - let size := Z.to_nat (Z.succ (log_inf p)) in - mkvalue size (Word.posToWord size p). + let size := Pos.to_nat (Pos.size p) in + ZToValue size (Zpos p). Definition valueToPos (v : value) : positive := - match valueToZ v with - | Zpos p => p - | _ => 1 - end. + Z.to_pos (uvalueToZ v). Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). @@ -88,6 +85,12 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (valueToZ i). +Definition valToValue (v : Values.val) := + match v with + | Values.Vint i => intToValue i + | _ => ZToValue 32 0%Z + 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 @@ -291,3 +294,28 @@ Inductive val_value_lessdef: val -> value -> Prop := Integers.Int.unsigned i = valueToZ v' -> val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. + +Search Z positive. + +Search "wordToZ". + +Lemma uvalueToZ_ZToValue : + forall n z, + (0 <= z < 2 ^ Z.of_nat n)%Z -> + uvalueToZ (ZToValue n z) = z. +Proof. + intros. unfold uvalueToZ, ZToValue. simpl. + apply uwordToZ_ZToWord. apply H. +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. apply Pos.size_gt. + inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. + simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. +Qed. -- cgit From 43f766ea8aff8309d94173cc1e2670eb8ddce68f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:51:14 +0100 Subject: Switch position of empty rule --- src/verilog/Verilog.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index c0bce25..c1e0a79 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v - | erun_Vvar_empty : - forall fext assoc r sz, - assoc!r = None -> - expr_runp fext assoc (Vvar r) (ZToValue sz 0) | erun_Vvar : 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 -> -- cgit From d76ea8e7a52f01a1be2f5b2ec1c5367a42aa0f65 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:51:33 +0100 Subject: Fix the semantics to properly evaluate the state --- src/verilog/HTL.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 147d24b..36e4434 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -63,7 +63,7 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f, + forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval, m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -75,7 +75,9 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations assoc2 nbassoc1) -> assoc3 = merge_assocmap nbassoc1 assoc2 -> - step g (State m st assoc0) t (State m st assoc3) + assoc3!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State m st assoc0) t (State m pstval assoc3) | step_finish : forall g t m st assoc retval, assoc!(m.(mod_finish)) = Some (1'h"1") -> -- cgit From 39a4348657c2f3efb3feafe9cf65b0f2a1a263c2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 21 May 2020 23:10:45 +0100 Subject: Finish the proof with most assumptions --- src/verilog/AssocMap.v | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index bd61c8e..9caa2d1 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -36,12 +36,17 @@ Module AssocMapExt. | Some v => v end. - Definition merge : t elt -> t elt -> t elt := fold (@add elt). - - Lemma merge_add_assoc : - forall am am' r v x, - find x (merge (add r v am) am') = find x (add r v (merge am am')). - Admitted. + Definition merge (m1 m2 : t elt) : t elt := + fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1). + + Lemma merge_add_assoc2 : + forall am am' r v, + merge (add r v am) am' = add r v (merge am am'). + Proof. + intros. + unfold merge. + Search fold_right. + apply SetoidList.fold_right_add2. Lemma merge_base : forall am, -- cgit From bb8a935f9143e65102a3a498a96dd13a3b8a4801 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 24 May 2020 13:36:53 +0100 Subject: Add HTLgen --- src/verilog/AssocMap.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 9caa2d1..cac2c02 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -43,15 +43,14 @@ Module AssocMapExt. forall am am' r v, merge (add r v am) am' = add r v (merge am am'). Proof. - intros. - unfold merge. - Search fold_right. - apply SetoidList.fold_right_add2. + induction am; intros. + unfold merge. simpl. unfold fold_right. simpl. Search MapsTo. + Abort. Lemma merge_base : forall am, merge (empty elt) am = am. - Proof. intros. unfold merge. apply fold_1. Qed. + Proof. auto. Qed. End Operations. -- cgit From 213267be33d714dabd19ca09210b5dc1ad4f6254 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 27 May 2020 23:38:40 +0100 Subject: Add more proofs and remove Admitted --- src/verilog/AssocMap.v | 45 +++++++++++++++++++++++++++++++++++++-------- src/verilog/Value.v | 22 ++++++++++++++-------- 2 files changed, 51 insertions(+), 16 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index cac2c02..7db800b 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -26,6 +26,11 @@ Module AssocMap := PositiveMap. Module AssocMapExt. Import AssocMap. + Hint Resolve elements_3w : assocmap. + Hint Resolve elements_correct : assocmap. + Hint Resolve gss : assocmap. + Hint Resolve gso : assocmap. + Section Operations. Variable elt : Type. @@ -36,16 +41,40 @@ Module AssocMapExt. | Some v => v end. - Definition merge (m1 m2 : t elt) : t elt := - fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1). + Definition merge (am bm : t elt) : t elt := + fold_right (fun p a => add (fst p) (snd p) a) bm (elements am). - Lemma merge_add_assoc2 : - forall am am' r v, - merge (add r v am) am' = add r v (merge am am'). + Lemma add_assoc : + forall k v l bm, + List.In (k, v) l -> + SetoidList.NoDupA (@eq_key elt) l -> + @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v. Proof. - induction am; intros. - unfold merge. simpl. unfold fold_right. simpl. Search MapsTo. - Abort. + Hint Resolve SetoidList.InA_alt : assocmap. + Hint Extern 1 (exists _, _) => apply list_in_map_inv : assocmap. + + induction l; intros. + - contradiction. + - destruct a as [k' v']. + destruct (peq k k'). + + inversion H. inversion H1. inversion H0. subst. + simpl. auto with assocmap. + + subst. inversion H0. subst. apply in_map with (f := fst) in H1. simpl in *. + unfold not in H4. exfalso. apply H4. apply SetoidList.InA_alt. + auto with assocmap. + + + 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 merge_add : + forall k v am bm, + find k am = Some v -> + find k (merge am bm) = Some v. + Proof. unfold merge. auto with assocmap. Qed. Lemma merge_base : forall am, diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 0ce0bc5..34cb0d2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -85,10 +85,11 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (valueToZ i). -Definition valToValue (v : Values.val) := +Definition valToValue (v : Values.val) : option value := match v with - | Values.Vint i => intToValue i - | _ => ZToValue 32 0%Z + | Values.Vint i => Some (intToValue i) + | Values.Vundef => Some (ZToValue 32 0%Z) + | _ => None end. (** Convert a [value] to a [bool], so that choices can be made based on the @@ -295,17 +296,22 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. -Search Z positive. - -Search "wordToZ". +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. - intros. unfold uvalueToZ, ZToValue. simpl. - apply uwordToZ_ZToWord. apply H. + unfold uvalueToZ, ZToValue. simpl. + auto using uwordToZ_ZToWord. Qed. Lemma valueToPos_posToValueAuto : -- cgit From 3ee0bfa7367fde5f9ec0dfd77f921f22f9e64563 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 28 May 2020 21:32:11 +0100 Subject: Finish Assocmap proofs --- src/verilog/AssocMap.v | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 7db800b..39fe3d2 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -19,6 +19,10 @@ From coqup Require Import Coquplib Value. From Coq Require Import FSets.FMapPositive. +From compcert Require Import Maps. + +Search Maps.PTree.get not List.In. + Definition reg := positive. Module AssocMap := PositiveMap. @@ -70,16 +74,71 @@ Module AssocMapExt. Qed. Hint Resolve add_assoc : assocmap. + Lemma not_in_assoc : + forall k v l bm, + ~ List.In k (List.map (@fst key elt) l) -> + @find elt k bm = Some v -> + @find elt k (fold_right (fun p a => add (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, find k am = Some v) <-> + List.In k (List.map (@fst _ elt) (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, find k am = Some v) <-> + ~ List.In k (List.map (@fst _ elt) (elements am)). + Proof. auto using not_iff_compat with assocmap. Qed. + Hint Resolve elements_correct' : assocmap. + + Lemma elements_correct_none : + forall am k, + find k am = None -> + ~ List.In k (List.map (@fst _ elt) (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_add : forall k v am bm, find k am = Some v -> find k (merge am bm) = Some v. Proof. unfold merge. auto with assocmap. Qed. + Hint Resolve merge_add : assocmap. + + Lemma merge_not_in : + forall k v am bm, + find k am = None -> + find k bm = Some v -> + find k (merge am bm) = Some v. + Proof. intros. apply not_in_assoc; auto with assocmap. Qed. + Hint Resolve merge_not_in : assocmap. Lemma merge_base : forall am, merge (empty elt) am = am. Proof. auto. Qed. + Hint Resolve merge_base : assocmap. End Operations. -- cgit From 3beb6e00213c5e7409d4574b663e5c6bf7490d66 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 14:42:09 +0100 Subject: Change AssocMap to Maps.PTree --- src/verilog/AssocMap.v | 113 +++++++++++++++++++++++++++++-------------------- 1 file changed, 66 insertions(+), 47 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 39fe3d2..e3b8159 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -17,46 +17,67 @@ *) From coqup Require Import Coquplib Value. -From Coq Require Import FSets.FMapPositive. - From compcert Require Import Maps. -Search Maps.PTree.get not List.In. - Definition reg := positive. -Module AssocMap := PositiveMap. +Module AssocMap := Maps.PTree. Module AssocMapExt. Import AssocMap. - Hint Resolve elements_3w : assocmap. - Hint Resolve elements_correct : assocmap. - Hint Resolve gss : assocmap. - Hint Resolve gso : assocmap. + Hint Resolve elements_correct elements_complete + elements_keys_norepet : assocmap. + Hint Resolve gso gss : assocmap. Section Operations. - Variable elt : Type. + Variable A : Type. - Definition find_default (a : elt) (k : reg) (m : t elt) : elt := - match find k m with + Definition get_default (a : A) (k : reg) (m : t A) : A := + match get k m with | None => a | Some v => v end. - Definition merge (am bm : t elt) : t elt := - fold_right (fun p a => add (fst p) (snd p) a) bm (elements am). + 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 : + forall am, + merge (empty A) am = am. + Proof. auto. Qed. + Hint Resolve merge_base : assocmap. + + Lemma merge_base2 : + forall am, + merge am (empty A) = am. + Proof. + unfold merge. + destruct am; trivial. + destruct o; trivial. + Qed. + Hint Resolve merge_base2 : assocmap. + + Lemma merge_assoc : + forall am bm k v, + (merge (set k v am) bm) = (set k v (merge am bm)). + Proof. Admitted. + + 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 v l bm, + forall (k : elt) (v : A) l bm, List.In (k, v) l -> - SetoidList.NoDupA (@eq_key elt) l -> - @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v. + 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. - Hint Resolve SetoidList.InA_alt : assocmap. - Hint Extern 1 (exists _, _) => apply list_in_map_inv : assocmap. - induction l; intros. - contradiction. - destruct a as [k' v']. @@ -64,9 +85,7 @@ Module AssocMapExt. + inversion H. inversion H1. inversion H0. subst. simpl. auto with assocmap. - subst. inversion H0. subst. apply in_map with (f := fst) in H1. simpl in *. - unfold not in H4. exfalso. apply H4. apply SetoidList.InA_alt. - 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. @@ -76,9 +95,9 @@ Module AssocMapExt. Lemma not_in_assoc : forall k v l bm, - ~ List.In k (List.map (@fst key elt) l) -> - @find elt k bm = Some v -> - @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v. + ~ 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. @@ -91,8 +110,8 @@ Module AssocMapExt. Lemma elements_iff : forall am k, - (exists v, find k am = Some v) <-> - List.In k (List.map (@fst _ elt) (elements am)). + (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. @@ -104,41 +123,41 @@ Module AssocMapExt. Lemma elements_correct' : forall am k, - ~ (exists v, find k am = Some v) <-> - ~ List.In k (List.map (@fst _ elt) (elements am)). + ~ (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, - find k am = None -> - ~ List.In k (List.map (@fst _ elt) (elements am)). + 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_add : + Lemma merge_fold_add : forall k v am bm, - find k am = Some v -> - find k (merge am bm) = Some v. - Proof. unfold merge. auto with assocmap. Qed. - Hint Resolve merge_add : assocmap. + 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_not_in : + Lemma merge_fold_not_in : forall k v am bm, - find k am = None -> - find k bm = Some v -> - find k (merge am bm) = Some v. + 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_not_in : assocmap. + Hint Resolve merge_fold_not_in : assocmap. - Lemma merge_base : + Lemma merge_fold_base : forall am, - merge (empty elt) am = am. + merge_fold (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_base : assocmap. + Hint Resolve merge_fold_base : assocmap. End Operations. @@ -148,14 +167,14 @@ Import AssocMapExt. Definition assocmap := AssocMap.t value. Definition find_assocmap (n : nat) : reg -> assocmap -> value := - find_default value (ZToValue n 0). + get_default value (ZToValue n 0). Definition empty_assocmap : assocmap := AssocMap.empty value. Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. Module AssocMapNotation. - Notation "a ! b" := (AssocMap.find b a) (at level 1). + Notation "a ! b" := (AssocMap.get b a) (at level 1). Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). Notation "a # b" := (find_assocmap 32 b a) (at level 1). Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). -- cgit From d7ff396015312585336d80c7b4608ac136b7aa0c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 15:35:26 +0100 Subject: New and improved Assocmap --- src/verilog/AssocMap.v | 39 ++++++++++++++++++++++++++++++++------- 1 file changed, 32 insertions(+), 7 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index e3b8159..88ad504 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -48,13 +48,13 @@ Module AssocMapExt. | _, _ => m1 end. - Lemma merge_base : + Lemma merge_base_1 : forall am, merge (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_base : assocmap. + Hint Resolve merge_base_1 : assocmap. - Lemma merge_base2 : + Lemma merge_base_2 : forall am, merge am (empty A) = am. Proof. @@ -62,12 +62,37 @@ Module AssocMapExt. destruct am; trivial. destruct o; trivial. Qed. - Hint Resolve merge_base2 : assocmap. + Hint Resolve merge_base_2 : assocmap. - Lemma merge_assoc : + 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, - (merge (set k v am) bm) = (set k v (merge am bm)). - Proof. Admitted. + 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). -- cgit From 3f3623f533033aca29fc7c5a05d2dad716133811 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 15:40:05 +0100 Subject: Fix indentation --- src/verilog/AssocMap.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 88ad504..43f9065 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -50,23 +50,23 @@ Module AssocMapExt. Lemma merge_base_1 : forall am, - merge (empty A) am = 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. + merge am (empty A) = am. Proof. unfold merge. destruct am; trivial. destruct o; trivial. - Qed. + 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'). + 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. @@ -128,7 +128,7 @@ Module AssocMapExt. - assumption. - destruct a as [k' v']. destruct (peq k k'); subst; - simpl in *; apply Decidable.not_or in H; destruct H. contradiction. + simpl in *; apply Decidable.not_or in H; destruct H. contradiction. rewrite AssocMap.gso; auto. Qed. Hint Resolve not_in_assoc : assocmap. @@ -180,7 +180,7 @@ Module AssocMapExt. Lemma merge_fold_base : forall am, - merge_fold (empty A) am = am. + merge_fold (empty A) am = am. Proof. auto. Qed. Hint Resolve merge_fold_base : assocmap. -- cgit From e06577fe952a3c268520b280b020bb2bff252529 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 18:14:59 +0100 Subject: Fix compilation moving to PTree --- src/verilog/AssocMap.v | 4 ++++ src/verilog/HTL.v | 7 +++---- src/verilog/Verilog.v | 14 +++++++------- 3 files changed, 14 insertions(+), 11 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 43f9065..88b13a6 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -198,6 +198,10 @@ 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. + Module AssocMapNotation. Notation "a ! b" := (AssocMap.get b a) (at level 1). Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 36e4434..a21064c 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -20,6 +20,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers. +From compcert Require Import Maps. Import HexNotationValue. @@ -29,13 +30,11 @@ hardware-like layout that is still similar to the register transfer language instantiations and that we now describe a state machine instead of a control-flow graph. *) -Notation "a ! b" := (PositiveMap.find b a) (at level 1). - Definition reg := positive. Definition node := positive. -Definition datapath := PositiveMap.t Verilog.stmnt. -Definition controllogic := PositiveMap.t Verilog.stmnt. +Definition datapath := PTree.t Verilog.stmnt. +Definition controllogic := PTree.t Verilog.stmnt. Record module: Type := mkmodule { diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index c1e0a79..ce7ddd9 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -171,13 +171,13 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := PositiveMap.t value. +Definition fext := AssocMap.t value. 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. @@ -300,7 +300,7 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. Definition access_fext (f : fext) (r : reg) : res value := - match PositiveMap.find r f with + match AssocMap.get r f with | Some v => OK v | _ => OK (ZToValue 1 0) end. @@ -452,7 +452,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := forall lhs name rhs rhsval assoc assoc' nbassoc f, assign_name lhs = OK name -> expr_runp f assoc rhs rhsval -> - assoc' = (PositiveMap.add name rhsval assoc) -> + assoc' = (AssocMap.set name rhsval assoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vblock lhs rhs) (mkassociations assoc' nbassoc) @@ -460,7 +460,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := forall lhs name rhs rhsval assoc nbassoc nbassoc' f, assign_name lhs = OK name -> expr_runp f assoc rhs rhsval -> - nbassoc' = (PositiveMap.add name rhsval nbassoc) -> + nbassoc' = (AssocMap.set name rhsval nbassoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vnonblock lhs rhs) (mkassociations assoc nbassoc'). @@ -534,8 +534,8 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) - | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) + | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) end. (*Definition module_run (n : nat) (m : module) : res assocmap := -- cgit