From 5e440ccec06e740c0ee8dc8eb0e54a7284d5aef7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Apr 2020 00:12:07 +0100 Subject: Use State in semantics instead of splitting it up --- src/verilog/Verilog.v | 193 +++++++++++++++++++++++++------------------------- 1 file changed, 98 insertions(+), 95 deletions(-) (limited to 'src') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 61df580..4713c36 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -169,17 +169,17 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Inductive state: Type := -| State: - forall (assoc: assoclist) - (nbassoc: assoclist), - state -| Callstate: state -| Returnstate: state. - -Definition fext := reg -> res value. +Definition fext := PositiveMap.t value. Definition fextclk := nat -> fext. +Inductive state: Type := + State: + forall (assoc : assoclist) + (nbassoc : assoclist) + (f : fextclk) + (cycle : positive), + state. + Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := match op with | Vadd => vplus @@ -212,37 +212,40 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : assoclist -> expr -> value -> Prop := +Inductive expr_runp : state -> expr -> value -> Prop := | erun_Vlit : - forall a v, - expr_runp a (Vlit v) v + forall s v, + expr_runp s (Vlit v) v | erun_Vvar : - forall assoc v r, + forall assoc na f c v r, assoc!r = Some v -> - expr_runp assoc (Vvar r) v + expr_runp (State assoc na f c) (Vvar r) v + | erun_Vinputvar : + forall s r v, + expr_runp s (Vinputvar r) v | erun_Vbinop : - forall a op l r lv rv oper EQ, - expr_runp a l lv -> - expr_runp a r rv -> + forall s op l r lv rv oper EQ, + expr_runp s l lv -> + expr_runp s r rv -> oper = binop_run op -> - expr_runp a (Vbinop op l r) (oper lv rv EQ) + expr_runp s (Vbinop op l r) (oper lv rv EQ) | erun_Vunop : - forall a u vu op oper, - expr_runp a u vu -> + forall s u vu op oper, + expr_runp s u vu -> oper = unop_run op -> - expr_runp a (Vunop op u) (oper vu) + expr_runp s (Vunop op u) (oper vu) | erun_Vternary_true : - forall a c t f vc vt, - expr_runp a c vc -> - expr_runp a t vt -> + forall s c ts fs vc vt, + expr_runp s c vc -> + expr_runp s ts vt -> valueToBool vc = true -> - expr_runp a (Vternary c t f) vt + expr_runp s (Vternary c ts fs) vt | erun_Vternary_false : - forall a c t f vc vf, - expr_runp a c vc -> - expr_runp a f vf -> + forall s c ts fs vc vf, + expr_runp s c vc -> + expr_runp s fs vf -> valueToBool vc = false -> - expr_runp a (Vternary c t f) vf. + expr_runp s (Vternary c ts fs) vf. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -260,16 +263,27 @@ 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 + | State _ _ f c => + match PositiveMap.find r (f (Pos.to_nat c)) with + | Some v => OK v + | _ => OK (ZToValue 1 0) + end + end. + (* TODO FIX Vvar case without default *) -Fixpoint expr_run (f : fext) (assoc : assoclist) (e : expr) - {struct e} : res value := +Fixpoint expr_run (s : state) (e : expr) + {struct e} : res value := match e with | Vlit v => OK v - | Vvar r => handle_def (ZToValue 32 0) assoc!r - | Vinputvar r => f r + | Vvar r => match s with + | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + end + | Vinputvar r => access_fext s r | Vbinop op l r => - let lv := expr_run f assoc l in - let rv := expr_run f assoc r in + let lv := expr_run s l in + let rv := expr_run s r in let oper := binop_run op in do lv' <- lv; do rv' <- rv; @@ -277,11 +291,11 @@ Fixpoint expr_run (f : fext) (assoc : assoclist) (e : expr) (eq_to_opt lv' rv' (oper lv' rv')) | Vunop op e => let oper := unop_run op in - do ev <- expr_run f assoc e; + do ev <- expr_run s e; OK (oper ev) | Vternary c te fe => - do cv <- expr_run f assoc c; - if valueToBool cv then expr_run f assoc te else expr_run f assoc fe + do cv <- expr_run s c; + if valueToBool cv then expr_run s te else expr_run s fe end. (** Return the name of the lhs of an assignment. For now, this function is quite @@ -293,14 +307,14 @@ Definition assign_name (e : expr) : res reg := | _ => Error (msg "Verilog: expression not supported on lhs of assignment") end. -Fixpoint find_case_stmnt (f : fext) (a : assoclist) (v : value) (cl : list (expr * stmnt)) +Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) {struct cl} : option (res stmnt) := match cl with - | (e, s)::xs => - match expr_run f a e with + | (e, st)::xs => + match expr_run s e with | OK v' => match eq_to_opt v v' (veq v v') with - | Some eq => if valueToBool eq then Some (OK s) else find_case_stmnt f a v xs + | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs | None => Some (Error (msg "Verilog: equality check sizes not equal")) end | Error msg => Some (Error msg) @@ -308,50 +322,40 @@ Fixpoint find_case_stmnt (f : fext) (a : assoclist) (v : value) (cl : list (expr | _ => None end. -Fixpoint stmnt_run' (f : fext) (n : nat) (s : state) (st : stmnt) {struct n} : res state := +Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := match n with | S n' => match st with | Vskip => OK s | Vseq s1 s2 => - do s' <- stmnt_run' f n' s s1; - stmnt_run' f n' s' s2 + do s' <- stmnt_run' n' s s1; + stmnt_run' n' s' s2 | Vcond c st sf => - match s with - | State assoc _ => - do cv <- expr_run f assoc c; - if valueToBool cv - then stmnt_run' f n' s st - else stmnt_run' f n' s sf - | _ => Error (msg "Verilog: stmnt execution in wrong state") - end + do cv <- expr_run s c; + if valueToBool cv + then stmnt_run' n' s st + else stmnt_run' n' s sf | Vcase e cl defst => - match s with - | State a _ => - do v <- expr_run f a e; - match find_case_stmnt f a v cl with - | Some (OK st') => stmnt_run' f n' s st' - | Some (Error msg) => Error msg - | None => do s' <- handle_opt (msg "Verilog: no case was matched") - (option_map (stmnt_run' f n' s) defst); s' - end - | _ => Error (msg "Verilog: stmnt execution in wrong state") + do v <- expr_run s e; + match find_case_stmnt s v cl with + | Some (OK st') => stmnt_run' n' s st' + | Some (Error msg) => Error msg + | None => do s' <- handle_opt (msg "Verilog: no case was matched") + (option_map (stmnt_run' n' s) defst); s' end | Vblock lhs rhs => match s with - | State assoc nbassoc => + | State assoc nbassoc f c => do name <- assign_name lhs; - do rhse <- expr_run f assoc rhs; - OK (State (PositiveMap.add name rhse assoc) nbassoc) - | _ => Error (msg "Verilog: stmnt exectution in wrong state") + do rhse <- expr_run s rhs; + OK (State (PositiveMap.add name rhse assoc) nbassoc f c) end | Vnonblock lhs rhs => match s with - | State assoc nbassoc => + | State assoc nbassoc f c => do name <- assign_name lhs; - do rhse <- expr_run f assoc rhs; - OK (State assoc (PositiveMap.add name rhse nbassoc)) - | _ => Error (msg "Verilog: stmnt execution in wrong state") + do rhse <- expr_run s rhs; + OK (State assoc (PositiveMap.add name rhse nbassoc) f c) end end | _ => OK s @@ -359,27 +363,26 @@ Fixpoint stmnt_run' (f : fext) (n : nat) (s : state) (st : stmnt) {struct n} : r Fixpoint stmnt_height (st : stmnt) {struct st} : nat := match st with - | Vskip => 1 - | Vseq s1 s2 => stmnt_height s1 + stmnt_height s2 - | Vcond _ s1 s2 => Nat.max (stmnt_height s1) (stmnt_height s2) + | 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) => - fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls + S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) | _ => 1 end. -Definition stmnt_run (f : fext) (s : state) (st : stmnt) : res state := - stmnt_run' f (stmnt_height st) s st. +Definition stmnt_run (s : state) (st : stmnt) : res state := + stmnt_run' (stmnt_height st) s st. -Fixpoint mi_step (f : fext) (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 f s st; - mi_step f s' ls + do s' <- stmnt_run s st; + mi_step s' ls in match m with | (Valways _ st)::ls => run st ls | (Valways_ff _ st)::ls => run st ls | (Valways_comb _ st)::ls => run st ls - | (Vdecl _ _)::ls => mi_step f s ls + | (Vdecl _ _)::ls => mi_step s ls | nil => OK s end. @@ -391,30 +394,30 @@ Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist := Definition empty_assoclist : assoclist := PositiveMap.empty value. -Definition mi_step_commit (f : fext) (assoc : assoclist) (m : list module_item) : res assoclist := - match mi_step f (State assoc empty_assoclist) m with - | OK (State assoc' nbassoc) => - OK (merge_assoclist nbassoc assoc') +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) | Error msg => Error msg - | _ => Error (msg "Returned in the 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' => - do assoc' <- mi_step_commit (f n') assoc m; - mi_run f assoc' m 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 + | Error m => Error m + end | O => OK assoc end. Definition module_run (n : nat) (m : module) : res assoclist := - let f := - fun n => - match n with - | 1%nat => fun r => if Pos.eqb r (fst (mod_reset m)) then OK (natToValue 1 1) else Error (msg "") - | _ => fun r => if Pos.eqb r (fst (mod_reset m)) then OK (natToValue 1 0) else Error (msg "") - end in + 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. Local Close Scope error_monad_scope. -- cgit