diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-03-09 22:19:40 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-09 22:19:40 +0000 |
commit | b9b21b639f4604b7ff0f0ccefa70f4bbde706d54 (patch) | |
tree | 39a471c26f933df72dc5002d6346648562f2470a /src/hls/Verilog.v | |
parent | 57350a8ca5579b65978d7a723a20915e763a2d0b (diff) | |
download | vericert-b9b21b639f4604b7ff0f0ccefa70f4bbde706d54.tar.gz vericert-b9b21b639f4604b7ff0f0ccefa70f4bbde706d54.zip |
Add negative edge reasoning to HTLgenproof
Diffstat (limited to 'src/hls/Verilog.v')
-rw-r--r-- | src/hls/Verilog.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 8e14267..48f3084 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -76,6 +76,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 |