aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLPargen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r--src/hls/HTLPargen.v81
1 files changed, 42 insertions, 39 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 9213514..9045499 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -57,8 +57,8 @@ Definition init_state (st : reg) : state :=
1%positive
(AssocMap.empty (option io * scl_decl))
(AssocMap.empty (option io * arr_decl))
- (AssocMap.empty stmnt)
- (AssocMap.empty stmnt).
+ (AssocMap.empty datapath_stmnt)
+ (AssocMap.empty control_stmnt).
Module HTLState <: State.
@@ -152,8 +152,8 @@ Lemma add_instr_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n st s.(st_datapath))
- (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
+ (AssocMap.set n (HTLDataVstmnt st) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt (state_goto s.(st_st) n')) s.(st_controllogic))).
Proof.
constructor; intros;
try (simpl; destruct (peq n n0); subst);
@@ -170,8 +170,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n st s.(st_datapath))
- (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
+ (AssocMap.set n (HTLDataVstmnt st) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt (state_goto s.(st_st) n')) s.(st_controllogic)))
(add_instr_state_incr s n n' st TRANS)
| _ => Error (Errors.msg "HTL.add_instr")
end.
@@ -186,8 +186,8 @@ Lemma add_instr_skip_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n st s.(st_datapath))
- (AssocMap.set n Vskip s.(st_controllogic))).
+ (AssocMap.set n (HTLDataVstmnt st) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt Vskip) s.(st_controllogic))).
Proof.
constructor; intros;
try (simpl; destruct (peq n n0); subst);
@@ -204,8 +204,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n st s.(st_datapath))
- (AssocMap.set n Vskip s.(st_controllogic)))
+ (AssocMap.set n (HTLDataVstmnt st) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt Vskip) s.(st_controllogic)))
(add_instr_skip_state_incr s n st TRANS)
| _ => Error (Errors.msg "HTL.add_instr_skip")
end.
@@ -220,8 +220,8 @@ Lemma add_node_skip_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n Vskip s.(st_datapath))
- (AssocMap.set n st s.(st_controllogic))).
+ (AssocMap.set n (HTLDataVstmnt Vskip) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))).
Proof.
constructor; intros;
try (simpl; destruct (peq n n0); subst);
@@ -238,8 +238,8 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n Vskip s.(st_datapath))
- (AssocMap.set n st s.(st_controllogic)))
+ (AssocMap.set n (HTLDataVstmnt Vskip) s.(st_datapath))
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic)))
(add_node_skip_state_incr s n st TRANS)
| _ => Error (Errors.msg "HTL.add_node_skip")
end.
@@ -407,8 +407,8 @@ Lemma add_branch_instr_state_incr:
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n Vskip (st_datapath s))
- (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+ (AssocMap.set n (HTLDataVstmnt Vskip) (st_datapath s))
+ (AssocMap.set n (HTLCtrlVstmnt (state_cond s.(st_st) e n1 n2)) (st_controllogic s))).
Proof.
intros. apply state_incr_intro; simpl;
try (intros; destruct (peq n0 n); subst);
@@ -425,8 +425,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n Vskip (st_datapath s))
- (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+ (AssocMap.set n (HTLDataVstmnt Vskip) (st_datapath s))
+ (AssocMap.set n (HTLCtrlVstmnt (state_cond s.(st_st) e n1 n2)) (st_controllogic s)))
(add_branch_instr_state_incr s e n n1 n2 NTRANS)
| _ => Error (Errors.msg "Htlgen: add_branch_instr")
end.
@@ -516,13 +516,13 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
(st_controllogic s))
(create_arr_state_incr s sz ln i).
-Definition max_pc_map (m : Maps.PTree.t stmnt) :=
+Definition max_pc_map {A: Type} (m : Maps.PTree.t A) :=
PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
Lemma max_pc_map_sound:
- forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+ forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m).
Proof.
- intros until i.
+ intros until i. unfold max_pc_function.
apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
(* extensionality *)
intros. apply H0. rewrite H; auto.
@@ -530,14 +530,13 @@ Proof.
rewrite PTree.gempty. congruence.
(* inductive case *)
intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
- inv H2. unfold Ple, Plt in *. lia.
- apply Ple_trans with a. auto.
- unfold Ple, Plt in *. lia.
+ inv H2. xomega.
+ apply Ple_trans with a. auto. xomega.
Qed.
Lemma max_pc_wf :
- forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
- map_well_formed m.
+ forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+ @map_well_formed T m.
Proof.
unfold map_well_formed. intros.
exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
@@ -565,6 +564,12 @@ Fixpoint prange {A: Type} (p1 p2: positive) (l: list A) {struct l} :=
| nil => nil
end.
+Definition to_stmnt (s: stmnt) (d: datapath_stmnt) :=
+ match d with
+ | HTLDataVstmnt d' => d'
+ | _ => s
+ end.
+
Lemma add_data_instr_state_incr :
forall s n st,
st_incr s
@@ -574,8 +579,8 @@ Lemma add_data_instr_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n (Vseq (AssocMapExt.get_default
- _ Vskip n s.(st_datapath)) st) s.(st_datapath))
+ (AssocMap.set n (HTLDataVstmnt (Vseq (to_stmnt Vskip (AssocMapExt.get_default
+ _ (HTLDataVstmnt Vskip) n s.(st_datapath))) st)) s.(st_datapath))
s.(st_controllogic)).
Proof.
constructor; intros;
@@ -591,7 +596,8 @@ Definition add_data_instr (n : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath))
+ (AssocMap.set n (HTLDataVstmnt (Vseq (to_stmnt Vskip (AssocMapExt.get_default
+ _ (HTLDataVstmnt Vskip) n s.(st_datapath))) st)) s.(st_datapath))
s.(st_controllogic))
(add_data_instr_state_incr s n st).
@@ -606,7 +612,7 @@ Lemma add_control_instr_state_incr :
s.(st_scldecls)
s.(st_arrdecls)
s.(st_datapath)
- (AssocMap.set n st s.(st_controllogic))).
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))).
Proof.
constructor; intros;
try (simpl; destruct (peq n n0); subst);
@@ -624,7 +630,7 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
s.(st_scldecls)
s.(st_arrdecls)
s.(st_datapath)
- (AssocMap.set n st s.(st_controllogic)))
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic)))
(add_control_instr_state_incr s n st CTRL)
| _ =>
Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
@@ -640,7 +646,7 @@ Definition add_control_instr_force_state_incr :
s.(st_scldecls)
s.(st_arrdecls)
s.(st_datapath)
- (AssocMap.set n st s.(st_controllogic))).
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))).
Admitted.
Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
@@ -652,10 +658,9 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
s.(st_scldecls)
s.(st_arrdecls)
s.(st_datapath)
- (AssocMap.set n st s.(st_controllogic)))
+ (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic)))
(add_control_instr_force_state_incr s n st).
-
Fixpoint pred_expr (preg: reg) (p: pred_op) :=
match p with
| Pvar pred =>
@@ -801,10 +806,8 @@ Definition transf_module (f: function) : mon HTL.module :=
do rst <- create_reg (Some Vinput) 1;
do clk <- create_reg (Some Vinput) 1;
do current_state <- get;
- match zle (Z.pos (max_pc_map current_state.(st_datapath)))
- Integers.Int.max_unsigned,
- zle (Z.pos (max_pc_map current_state.(st_controllogic)))
- Integers.Int.max_unsigned with
+ match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
+ zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
| left LEDATA, left LECTRL =>
ret (HTL.mkmodule
f.(fn_params)
@@ -821,7 +824,7 @@ Definition transf_module (f: function) : mon HTL.module :=
clk
current_state.(st_scldecls)
current_state.(st_arrdecls)
- (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
+ (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
| _, _ => error (Errors.msg "More than 2^32 states.")
end
else error (Errors.msg "Stack size misalignment.").
generated by cgit (git 2.34.1) at 2024-06-30 22:01:02 +0000