aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Verilog.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/Verilog.v')
-rw-r--r--src/hls/Verilog.v231
1 files changed, 191 insertions, 40 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 779b05c..3a2c81d 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -21,23 +21,24 @@ Set Implicit Arguments.
Require Import Coq.Structures.OrderedTypeEx.
Require Import Coq.FSets.FMapPositive.
+Require Import Coq.Program.Basics.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
+Require Import Coq.Program.Program.
Require Import Coq.micromega.Lia.
+Require compcert.common.Events.
+Require Import compcert.lib.Integers.
Require Import compcert.common.Errors.
-Require Import compcert.common.Globalenvs.
Require Import compcert.common.Smallstep.
-Require Import compcert.lib.Integers.
-Require compcert.common.Events.
+Require Import compcert.common.Globalenvs.
-Require Import vericert.common.Show.
Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.Array.
-Require Import vericert.hls.AssocMap.
-Require Import vericert.hls.FunctionalUnits.
+Require Import vericert.common.Show.
Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
Import ListNotations.
@@ -81,6 +82,39 @@ Definition merge_arr (new : option arr) (old : option arr) : option arr :=
Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
AssocMap.combine merge_arr new old.
+Lemma merge_arr_empty':
+ forall l,
+ merge_arr (Some (arr_repeat None (length l))) (Some (make_array l)) = Some (make_array l).
+Proof.
+ induction l; auto.
+ unfold merge_arr.
+ unfold combine, make_array. simplify. rewrite H0.
+ rewrite list_repeat_cons. simplify.
+ rewrite H0; auto.
+Qed.
+
+Lemma merge_arr_empty:
+ forall v l,
+ v = Some (make_array l) ->
+ merge_arr (Some (arr_repeat None (length l))) v = v.
+Proof. intros. rewrite H. apply merge_arr_empty'. Qed.
+
+Lemma merge_arr_empty2:
+ forall v l v',
+ v = Some v' ->
+ l = arr_length v' ->
+ merge_arr (Some (arr_repeat None l)) v = v.
+Proof.
+ intros. subst. destruct v'. simplify.
+ generalize dependent arr_wf. generalize dependent arr_length.
+ induction arr_contents.
+ - simplify; subst; auto.
+ - unfold combine, make_array in *; simplify; subst.
+ rewrite list_repeat_cons; simplify.
+ specialize (IHarr_contents (Datatypes.length arr_contents) eq_refl).
+ inv IHarr_contents. rewrite H0. rewrite H0. auto.
+Qed.
+
Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
match a ! r with
| None => None
@@ -195,9 +229,12 @@ Inductive stmnt : Type :=
| Vskip : stmnt
| Vseq : stmnt -> stmnt -> stmnt
| Vcond : expr -> stmnt -> stmnt -> stmnt
-| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt
+| Vcase : expr -> stmnt_expr_list -> option stmnt -> stmnt
| Vblock : expr -> expr -> stmnt
-| Vnonblock : expr -> expr -> stmnt.
+| Vnonblock : expr -> expr -> stmnt
+with stmnt_expr_list : Type :=
+| Stmntnil : stmnt_expr_list
+| Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list.
(*|
Edges
@@ -263,7 +300,6 @@ Record module : Type := mkmodule {
mod_stk : reg;
mod_stk_len : nat;
mod_args : list reg;
- mod_funct_units: funct_units;
mod_body : list module_item;
mod_entrypoint : node;
}.
@@ -405,7 +441,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
expr_runp fext reg stack fs vf ->
valueToBool vc = false ->
expr_runp fext reg stack (Vternary c ts fs) vf.
-Hint Constructors expr_runp : verilog.
+#[export] Hint Constructors expr_runp : verilog.
Definition handle_opt {A : Type} (err : errmsg) (val : option A)
: res A :=
@@ -464,19 +500,19 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
mve <> ve ->
stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 ->
- stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
+ stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1
| stmnt_runp_Vcase_match:
forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
mve = ve ->
stmnt_runp f asr0 asa0 sc asr1 asa1 ->
- stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
+ stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1
| stmnt_runp_Vcase_default:
forall asr0 asa0 asr1 asa1 f st e ve,
expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
stmnt_runp f asr0 asa0 st asr1 asa1 ->
- stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
+ stmnt_runp f asr0 asa0 (Vcase e Stmntnil (Some st)) asr1 asa1
| stmnt_runp_Vblock_reg:
forall lhs r rhs rhsval asr asa f,
location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
@@ -505,26 +541,35 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
stmnt_runp f asr asa
(Vnonblock lhs rhs)
asr (nonblock_arr r i asa rhsval).
-Hint Constructors stmnt_runp : verilog.
+#[export] Hint Constructors stmnt_runp : verilog.
Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
module_item -> reg_associations -> arr_associations -> Prop :=
| mi_stepp_Valways :
forall f sr0 sa0 st sr1 sa1 c,
stmnt_runp f sr0 sa0 st sr1 sa1 ->
- mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
-| mi_stepp_Valways_ff :
- forall f sr0 sa0 st sr1 sa1 c,
- stmnt_runp f sr0 sa0 st sr1 sa1 ->
- mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
-| mi_stepp_Valways_comb :
+ mi_stepp f sr0 sa0 (Valways (Vposedge c) st) sr1 sa1
+| mi_stepp_Valways_ne :
+ forall f sr0 sa0 c st,
+ mi_stepp f sr0 sa0 (Valways (Vnegedge c) st) sr0 sa0
+| mi_stepp_Vdecl :
+ forall f sr0 sa0 d,
+ mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0.
+#[export] Hint Constructors mi_stepp : verilog.
+
+Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations ->
+ module_item -> reg_associations -> arr_associations -> Prop :=
+| mi_stepp_negedge_Valways :
forall f sr0 sa0 st sr1 sa1 c,
stmnt_runp f sr0 sa0 st sr1 sa1 ->
- mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
-| mi_stepp_Vdecl :
- forall f sr sa d,
- mi_stepp f sr sa (Vdeclaration d) sr sa.
-Hint Constructors mi_stepp : verilog.
+ mi_stepp_negedge f sr0 sa0 (Valways (Vnegedge c) st) sr1 sa1
+| mi_stepp_negedge_Valways_ne :
+ forall f sr0 sa0 c st,
+ mi_stepp_negedge f sr0 sa0 (Valways (Vposedge c) st) sr0 sa0
+| mi_stepp_negedge_Vdecl :
+ forall f sr0 sa0 d,
+ mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0.
+#[export] Hint Constructors mi_stepp : verilog.
Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
list module_item -> reg_associations -> arr_associations -> Prop :=
@@ -536,7 +581,19 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
| mis_stepp_Nil :
forall f sr sa,
mis_stepp f sr sa nil sr sa.
-Hint Constructors mis_stepp : verilog.
+#[export] Hint Constructors mis_stepp : verilog.
+
+Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations ->
+ list module_item -> reg_associations -> arr_associations -> Prop :=
+| mis_stepp_negedge_Cons :
+ forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
+ mi_stepp_negedge f sr0 sa0 mi sr1 sa1 ->
+ mis_stepp_negedge f sr1 sa1 mis sr2 sa2 ->
+ mis_stepp_negedge f sr0 sa0 (mi :: mis) sr2 sa2
+| mis_stepp_negedge_Nil :
+ forall f sr sa,
+ mis_stepp_negedge f sr sa nil sr sa.
+#[export] Hint Constructors mis_stepp : verilog.
Local Close Scope error_monad_scope.
@@ -552,18 +609,24 @@ Definition empty_stack (m : module) : assocmap_arr :=
Inductive step : genv -> state -> Events.trace -> state -> Prop :=
| step_module :
- forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
+ forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 basr2 nasr2
+ basa2 nasa2 f stval pstval m sf st g ist,
asr!(m.(mod_reset)) = Some (ZToValue 0) ->
asr!(m.(mod_finish)) = Some (ZToValue 0) ->
asr!(m.(mod_st)) = Some ist ->
valueToPos ist = st ->
mis_stepp f (mkassociations asr empty_assocmap)
(mkassociations asa (empty_stack m))
- m.(mod_body)
+ (mod_body m)
(mkassociations basr1 nasr1)
- (mkassociations basa1 nasa1)->
- asr' = merge_regs nasr1 basr1 ->
- asa' = merge_arrs nasa1 basa1 ->
+ (mkassociations basa1 nasa1) ->
+ mis_stepp_negedge f (mkassociations (merge_regs nasr1 basr1) empty_assocmap)
+ (mkassociations (merge_arrs nasa1 basa1) (empty_stack m))
+ (mod_body m)
+ (mkassociations basr2 nasr2)
+ (mkassociations basa2 nasa2) ->
+ asr' = merge_regs nasr2 basr2 ->
+ asa' = merge_arrs nasa2 basa2 ->
asr'!(m.(mod_st)) = Some stval ->
valueToPos stval = pstval ->
step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -586,7 +649,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
mst = mod_st m ->
step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
(State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
-Hint Constructors step : verilog.
+#[export] Hint Constructors step : verilog.
Inductive initial_state (p: program): state -> Prop :=
| initial_state_intro: forall b m0 m,
@@ -605,6 +668,18 @@ Definition semantics (m : program) :=
Smallstep.Semantics step (initial_state m) final_state
(Globalenvs.Genv.globalenv m).
+Fixpoint list_to_stmnt st :=
+ match st with
+ | (e, s) :: r => Stmntcons e s (list_to_stmnt r)
+ | nil => Stmntnil
+ end.
+
+Fixpoint stmnt_to_list st :=
+ match st with
+ | Stmntcons e s r => (e, s) :: stmnt_to_list r
+ | Stmntnil => nil
+ end.
+
Lemma expr_runp_determinate :
forall f e asr asa v,
expr_runp f asr asa e v ->
@@ -632,7 +707,7 @@ Proof.
learn (H1 _ H2)
end; crush).
Qed.
-Hint Resolve expr_runp_determinate : verilog.
+#[export] Hint Resolve expr_runp_determinate : verilog.
Lemma location_is_determinate :
forall f asr asa e l,
@@ -665,8 +740,8 @@ Lemma stmnt_runp_determinate :
| [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H
| [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H
| [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H
- | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H
- | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H
+ | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => invert H
+ | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil _) _ _ |- _ ] => invert H
| [ H1 : expr_runp _ ?asr ?asa ?e _,
H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
@@ -681,7 +756,7 @@ Lemma stmnt_runp_determinate :
learn (H1 _ _ H2)
end; crush).
Qed.
-Hint Resolve stmnt_runp_determinate : verilog.
+#[export] Hint Resolve stmnt_runp_determinate : verilog.
Lemma mi_stepp_determinate :
forall f asr0 asa0 m asr1 asa1,
@@ -699,6 +774,22 @@ Proof.
end; crush).
Qed.
+Lemma mi_stepp_negedge_determinate :
+ forall f asr0 asa0 m asr1 asa1,
+ mi_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+ forall asr1' asa1',
+ mi_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+ asr1' = asr1 /\ asa1' = asa1.
+Proof.
+ intros. destruct m; invert H; invert H0;
+
+ repeat (try match goal with
+ | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
+ H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+ learn (stmnt_runp_determinate H1 H2)
+ end; crush).
+Qed.
+
Lemma mis_stepp_determinate :
forall f asr0 asa0 m asr1 asa1,
mis_stepp f asr0 asa0 m asr1 asa1 ->
@@ -722,17 +813,77 @@ Proof.
end; crush).
Qed.
+Lemma mis_stepp_negedge_determinate :
+ forall f asr0 asa0 m asr1 asa1,
+ mis_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+ forall asr1' asa1',
+ mis_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+ asr1' = asr1 /\ asa1' = asa1.
+Proof.
+ induction 1; intros;
+
+ repeat (try match goal with
+ | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H
+ | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
+
+ | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _,
+ H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+ learn (mi_stepp_negedge_determinate H1 H2)
+
+ | [ H1 : forall asr1 asa1, mis_stepp_negedge _ ?asr0 ?asa0 ?m asr1 asa1 -> _,
+ H2 : mis_stepp_negedge _ ?asr0 ?asa0 ?m _ _ |- _ ] =>
+ learn (H1 _ _ H2)
+ end; crush).
+Qed.
+
Lemma semantics_determinate :
forall (p: program), Smallstep.determinate (semantics p).
Proof.
intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
- invert H; invert H0; constructor. (* Traces are always empty *)
- - invert H; invert H0; crush.
- assert (f = f0) by (destruct f; destruct f0; auto); subst.
- pose proof (mis_stepp_determinate H5 H15).
+ - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
+ pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4.
+ pose proof (mis_stepp_negedge_determinate H6 H17).
crush.
- constructor. invert H; crush.
- invert H; invert H0; unfold ge0, ge1 in *; crush.
- red; simplify; intro; invert H0; invert H; crush.
- invert H; invert H0; crush.
Qed.
+
+Local Open Scope positive.
+
+Fixpoint max_reg_expr (e: expr) :=
+ match e with
+ | Vlit _ => 1
+ | Vvar r => r
+ | Vvari r e => Pos.max r (max_reg_expr e)
+ | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2))
+ | Vinputvar r => r
+ | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+ | Vunop _ e => max_reg_expr e
+ | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3))
+ end.
+
+Fixpoint max_reg_stmnt (st: stmnt) :=
+ match st with
+ | Vskip => 1
+ | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)
+ | Vcond e s1 s2 =>
+ Pos.max (max_reg_expr e)
+ (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2))
+ | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)
+ | Vcase e stl (Some s) =>
+ Pos.max (max_reg_stmnt s)
+ (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl))
+ | Vblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+ | Vnonblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+ end
+with max_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
+ match stl with
+ | Stmntnil => 1
+ | Stmntcons e s stl' =>
+ Pos.max (max_reg_expr e)
+ (Pos.max (max_reg_stmnt s)
+ (max_reg_stmnt_expr_list stl'))
+ end.
generated by cgit (git 2.34.1) at 2024-07-18 08:02:07 +0000