diff options
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r-- | src/hls/RTLBlockInstr.v | 225 |
1 files changed, 3 insertions, 222 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 8353452..51beedc 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -28,228 +28,10 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. -Require Import vericert.common.Vericertlib. -Require Import vericert.hls.Sat. - -Local Open Scope rtl. +Require Import Predicate. +Require Import Vericertlib. Definition node := positive. -Definition predicate := positive. - -Inductive pred_op : Type := -| Pvar: predicate -> pred_op -| Ptrue: pred_op -| Pfalse: pred_op -| Pnot: pred_op -> pred_op -| Pand: pred_op -> pred_op -> pred_op -| Por: pred_op -> pred_op -> pred_op. - -Declare Scope pred_op. - -Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op. -Notation "A ∨ B" := (Por A B) (at level 25) : pred_op. -Notation "⟂" := (Pfalse) : pred_op. -Notation "'T'" := (Ptrue) : pred_op. -Notation "¬ A" := (Pnot A) (at level 15) : pred_op. - -Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := - match p with - | Pvar p' => a (Pos.to_nat p') - | Ptrue => true - | Pfalse => false - | Pnot p' => negb (sat_predicate p' a) - | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a - | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a - end. - -Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := - match a with - | nil => nil - | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) - end. - -Lemma satFormula_concat: - forall a b agn, - satFormula a agn -> - satFormula b agn -> - satFormula (a ++ b) agn. -Proof. induction a; crush. Qed. - -Lemma satFormula_concat2: - forall a b agn, - satFormula (a ++ b) agn -> - satFormula a agn /\ satFormula b agn. -Proof. - induction a; simplify; - try apply IHa in H1; crush. -Qed. - -Lemma satClause_concat: - forall a a1 a0, - satClause a a1 -> - satClause (a0 ++ a) a1. -Proof. induction a0; crush. Qed. - -Lemma satClause_concat2: - forall a a1 a0, - satClause a0 a1 -> - satClause (a0 ++ a) a1. -Proof. - induction a0; crush. - inv H; crush. -Qed. - -Lemma satClause_concat3: - forall a b c, - satClause (a ++ b) c -> - satClause a c \/ satClause b c. -Proof. - induction a; crush. - inv H; crush. - apply IHa in H0; crush. - inv H0; crush. -Qed. - -Lemma satFormula_mult': - forall p2 a a0, - satFormula p2 a0 \/ satClause a a0 -> - satFormula (map (fun x : list lit => a ++ x) p2) a0. -Proof. - induction p2; crush. - - inv H. inv H0. apply satClause_concat. auto. - apply satClause_concat2; auto. - - apply IHp2. - inv H; crush; inv H0; crush. -Qed. - -Lemma satFormula_mult2': - forall p2 a a0, - satFormula (map (fun x : list lit => a ++ x) p2) a0 -> - satClause a a0 \/ satFormula p2 a0. -Proof. - induction p2; crush. - apply IHp2 in H1. inv H1; crush. - apply satClause_concat3 in H0. - inv H0; crush. -Qed. - -Lemma satFormula_mult: - forall p1 p2 a, - satFormula p1 a \/ satFormula p2 a -> - satFormula (mult p1 p2) a. -Proof. - induction p1; crush. - apply satFormula_concat; crush. - inv H. inv H0. - apply IHp1. auto. - apply IHp1. auto. - apply satFormula_mult'; - inv H; crush. -Qed. - -Lemma satFormula_mult2: - forall p1 p2 a, - satFormula (mult p1 p2) a -> - satFormula p1 a \/ satFormula p2 a. -Proof. - induction p1; crush. - apply satFormula_concat2 in H; crush. - apply IHp1 in H0. - inv H0; crush. - apply satFormula_mult2' in H1. inv H1; crush. -Qed. - -Fixpoint trans_pred (bound: nat) (p: pred_op) : - option {fm: formula | forall a, - sat_predicate p a = true <-> satFormula fm a}. - refine - (match bound with - | O => None - | S n => - match p with - | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) - | Ptrue => Some (exist _ nil _) - | Pfalse => Some (exist _ (nil::nil) _) - | Pand p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist _ p1' _), Some (exist _ p2' _) => - Some (exist _ (p1' ++ p2') _) - | _, _ => None - end - | Por p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist _ p1' _), Some (exist _ p2' _) => - Some (exist _ (mult p1' p2') _) - | _, _ => None - end - | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) - | Pnot Ptrue => Some (exist _ (nil::nil) _) - | Pnot Pfalse => Some (exist _ nil _) - | Pnot (Pnot p') => - match trans_pred n p' with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - | Pnot (Pand p1 p2) => - match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - | Pnot (Por p1 p2) => - match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - end - end); split; intros; simpl in *; auto; try solve [crush]. - - inv H. inv H0; auto. - - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. - crush. - - rewrite negb_involutive in H. apply i in H. auto. - - rewrite negb_involutive. apply i; auto. - - rewrite negb_andb in H. apply i. auto. - - rewrite negb_andb. apply i. auto. - - rewrite negb_orb in H. apply i. auto. - - rewrite negb_orb. apply i. auto. - - apply satFormula_concat. - apply andb_prop in H. inv H. apply i in H0. auto. - apply andb_prop in H. inv H. apply i0 in H1. auto. - - apply satFormula_concat2 in H. simplify. apply andb_true_intro. - split. apply i in H0. auto. - apply i0 in H1. auto. - - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto. - apply i0 in H0. auto. - - apply orb_true_intro. - apply satFormula_mult2 in H. inv H. apply i in H0. auto. - apply i0 in H0. auto. -Defined. - -Definition sat_pred (bound: nat) (p: pred_op) : - option ({al : alist | sat_predicate p (interp_alist al) = true} - + {forall a : asgn, sat_predicate p a = false}). - refine - ( match trans_pred bound p with - | Some (exist _ fm _) => - match boundedSat bound fm with - | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) - | Some (inright _) => Some (inright _) - | None => None - end - | None => None - end ). - - apply i in s2. auto. - - intros. specialize (n a). specialize (i a). - destruct (sat_predicate p a). exfalso. - apply n. apply i. auto. auto. -Defined. - -Definition sat_pred_simple (bound: nat) (p: pred_op) := - match sat_pred bound p with - | Some (inleft (exist _ al _)) => Some (Some al) - | Some (inright _) => Some None - | None => None - end. Inductive instr : Type := | RBnop : instr @@ -320,10 +102,9 @@ Definition predset := PMap.t bool. Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := match p with - | Pvar p' => PMap.get p' pr + | Pvar (b, p') => if b then PMap.get p' pr else negb (PMap.get p' pr) | Ptrue => true | Pfalse => false - | Pnot p' => negb (eval_predf pr p') | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') end. |