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') 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