diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 55 |
1 files changed, 25 insertions, 30 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9045499..2cfcba4 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -152,8 +152,8 @@ Lemma add_instr_state_incr : (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n (HTLDataVstmnt st) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt (state_goto s.(st_st) n')) s.(st_controllogic))). + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (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 (HTLDataVstmnt st) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt (state_goto s.(st_st) n')) s.(st_controllogic))) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (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 (HTLDataVstmnt st) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt Vskip) s.(st_controllogic))). + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n 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 (HTLDataVstmnt st) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt Vskip) s.(st_controllogic))) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n 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 (HTLDataVstmnt Vskip) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))). + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n 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 (HTLDataVstmnt Vskip) s.(st_datapath)) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n 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 (HTLDataVstmnt Vskip) (st_datapath s)) - (AssocMap.set n (HTLCtrlVstmnt (state_cond s.(st_st) e n1 n2)) (st_controllogic s))). + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (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 (HTLDataVstmnt Vskip) (st_datapath s)) - (AssocMap.set n (HTLCtrlVstmnt (state_cond s.(st_st) e n1 n2)) (st_controllogic s))) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (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. @@ -564,12 +564,6 @@ 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 @@ -579,8 +573,8 @@ Lemma add_data_instr_state_incr : (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n (HTLDataVstmnt (Vseq (to_stmnt Vskip (AssocMapExt.get_default - _ (HTLDataVstmnt Vskip) n s.(st_datapath))) st)) s.(st_datapath)) + (AssocMap.set n (Vseq (AssocMapExt.get_default + _ Vskip n s.(st_datapath)) st) s.(st_datapath)) s.(st_controllogic)). Proof. constructor; intros; @@ -596,8 +590,8 @@ Definition add_data_instr (n : node) (st : stmnt) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n (HTLDataVstmnt (Vseq (to_stmnt Vskip (AssocMapExt.get_default - _ (HTLDataVstmnt Vskip) n s.(st_datapath))) st)) s.(st_datapath)) + (AssocMap.set n (Vseq (AssocMapExt.get_default + _ Vskip n s.(st_datapath)) st) s.(st_datapath)) s.(st_controllogic)) (add_data_instr_state_incr s n st). @@ -612,7 +606,7 @@ Lemma add_control_instr_state_incr : s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))). + (AssocMap.set n st s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -630,7 +624,7 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))) + (AssocMap.set n 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") @@ -646,7 +640,7 @@ Definition add_control_instr_force_state_incr : s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))). + (AssocMap.set n st s.(st_controllogic))). Admitted. Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := @@ -658,7 +652,7 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n (HTLCtrlVstmnt st) s.(st_controllogic))) + (AssocMap.set n st s.(st_controllogic))) (add_control_instr_force_state_incr s n st). Fixpoint pred_expr (preg: reg) (p: pred_op) := @@ -824,6 +818,7 @@ Definition transf_module (f: function) : mon HTL.module := clk current_state.(st_scldecls) current_state.(st_arrdecls) + (AssocMap.empty (ident * controlsignal)) (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) | _, _ => error (Errors.msg "More than 2^32 states.") end |