From fd05b7155ce5ebd2d4ce665f3b30e2aca391dafe Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 Mar 2021 11:27:28 +0000 Subject: Remove comments in Verilog.v --- src/hls/Verilog.v | 194 ------------------------------------------------------ 1 file changed, 194 deletions(-) (limited to 'src/hls/Verilog.v') diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 48f3084..ec1d307 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -426,40 +426,6 @@ 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 AssocMap.get r f with - | Some v => OK v - | _ => OK (ZToValue 0) - end.*) - -(* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assocmap) (e : expr) - {struct e} : res value := - match e with - | Vlit v => OK v - | Vvar r => match s with - | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r - | _ => Error (msg "Verilog: Wrong state") - end - | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") - | Vinputvar r => access_fext s r - | Vbinop op l r => - 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; - handle_opt (msg "Verilog: sizes are not equal") - (eq_to_opt lv' rv' (oper lv' rv')) - | Vunop op e => - let oper := unop_run op in - do ev <- expr_run s e; - OK (oper ev) - | Vternary c te fe => - do cv <- expr_run s c; - if valueToBool cv then expr_run s te else expr_run s fe - end.*) - (** Return the location of the lhs of an assignment. *) Inductive location : Type := @@ -472,80 +438,6 @@ Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> expr_runp f asr asa iexp iv -> location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). -(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) -(* match e with *) -(* | Vvar r => OK r *) -(* | _ => 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 - | (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 st) else find_case_stmnt s v xs - | None => Some (Error (msg "Verilog: equality check sizes not equal")) - end - | Error msg => Some (Error msg) - end - | _ => None - end. - -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' n' s s1; - stmnt_run' n' s' s2 - | Vcond c st sf => - 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 => - 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 m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) - | _ => Error (msg "Verilog: Wrong state") - end - | Vnonblock lhs rhs => - match s with - | State m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State 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. *) - Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt -> reg_associations -> arr_associations -> Prop := | stmnt_runp_Vskip: @@ -616,20 +508,6 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> asr (nonblock_arr r i asa rhsval). Hint Constructors stmnt_runp : verilog. -(*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 - 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 s ls - | (Vdeclarr _ _ _)::ls => mi_step s ls - | nil => OK s - end.*) - Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := | mi_stepp_Valways : @@ -661,80 +539,8 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> mis_stepp f sr sa nil sr sa. Hint Constructors mis_stepp : verilog. -(*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_assocmap nbassoc assoc) empty_assocmap f c) - | Error msg => Error msg - | _ => Error (msg "Verilog: Wrong state") - end. - -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_assocmap f (Pos.of_nat n')) m with - | OK (State 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 => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) - | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) - end.*) - -(*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. -(*Theorem value_eq_size_if_eq: - forall lv rv EQ, - vsize lv = vsize rv -> value_eq_size lv rv = left EQ. -Proof. intros. unfold value_eq_size. - -Theorem expr_run_same: - forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. -Proof. - split; generalize dependent v; generalize dependent assoc. - - induction e. - + intros. inversion H. constructor. - + intros. inversion H. constructor. assumption. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. - unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. - constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. - discriminate. - + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. - inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. - eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. - eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. - discriminate. - - induction e. - + intros. inversion H. reflexivity. - + intros. inversion H. subst. simpl. assumption. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. - apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). - apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. - + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. - apply IHe in H3. rewrite Heqo in H3. - inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. - apply IHe2 in H6. rewrite H6. reflexivity. - subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. - assumption. -Qed. - - *) - Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := match rl, vl with | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') -- cgit