aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLBlockInstr.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r--src/hls/RTLBlockInstr.v225
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.
generated by cgit (git 2.34.1) at 2024-07-02 18:33:56 +0000