diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:19:02 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:19:13 +0000 |
commit | 5baf15eafe42571210249a4863b0aff0d3490565 (patch) | |
tree | 39b0a3f722f5b27c1902d24fa9554d6701d0a40b /src/hls/RTLPargen.v | |
parent | 3addff470c8faeb6876c63575184caa0aa829e28 (diff) | |
download | vericert-5baf15eafe42571210249a4863b0aff0d3490565.tar.gz vericert-5baf15eafe42571210249a4863b0aff0d3490565.zip |
Share code between RTLBlock and Par
Diffstat (limited to 'src/hls/RTLPargen.v')
-rw-r--r-- | src/hls/RTLPargen.v | 51 |
1 files changed, 7 insertions, 44 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 836ceac..55bf71c 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -16,56 +16,19 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import AST Maps. -From vericert Require Import Vericertlib RTLBlock RTLPar Scheduleoracle. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. -Fixpoint beq {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := - match m1, m2 with - | PTree.Leaf, _ => PTree.bempty m2 - | _, PTree.Leaf => PTree.bempty m1 - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq beqA l1 l2 && beq beqA r1 r2 - end. - -Lemma beq_correct: - forall A B beqA m1 m2, - @beq A B beqA m1 m2 = true <-> - (forall (x: PTree.elt), - match PTree.get x m1, PTree.get x m2 with - | None, None => True - | Some y1, Some y2 => beqA y1 y2 = true - | _, _ => False - end). -Proof. - induction m1; intros. - - simpl. rewrite PTree.bempty_correct. split; intros. - rewrite PTree.gleaf. rewrite H. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. - - destruct m2. - + unfold beq. rewrite PTree.bempty_correct. split; intros. - rewrite H. rewrite PTree.gleaf. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). -Qed. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.Scheduleoracle. Parameter schedule : RTLBlock.function -> RTLPar.function. Definition transl_function (f : RTLBlock.function) : Errors.res RTLPar.function := let tf := schedule f in - if beq schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then + if beq2 schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then Errors.OK tf else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). |