diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 42 |
1 files changed, 13 insertions, 29 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 7abdf82..5b179e1 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -31,7 +31,6 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. -Require Import vericert.hls.FunctionalUnits. #[local] Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. #[local] Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -71,8 +70,6 @@ Ltac monadInv1 H := discriminate | (ret _ _ = OK _ _ _) => inversion H; clear H; try subst - | (mret _ _ = OK _ _ _) => - inversion H; clear H; try subst | (error _ _ = OK _ _ _) => discriminate | (bind ?G ?F ?S = OK ?X ?S' ?I) => @@ -101,10 +98,9 @@ Ltac monadInv1 H := Ltac monadInv H := match type of H with | (ret _ _ = OK _ _ _) => monadInv1 H - | (mret _ _ = OK _ _ _) => monadInv1 H | (error _ _ = OK _ _ _) => monadInv1 H - | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H - | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H + | (bind ?G ?F ?S = OK ?X ?S' ?I) => monadInv1 H + | (bind2 ?G ?F ?S = OK ?X ?S' ?I) => monadInv1 H | (?F _ _ _ _ _ _ _ _ = OK _ _ _) => ((progress simpl in H) || unfold F in H); monadInv1 H | (?F _ _ _ _ _ _ _ = OK _ _ _) => @@ -123,15 +119,11 @@ Ltac monadInv H := ((progress simpl in H) || unfold F in H); monadInv1 H end. -(*| -=========================================== -Relational specification of the translation -=========================================== +(** * Relational specification of the translation *) -We now define inductive predicates that characterise the fact that the +(** We now define inductive predicates that characterise the fact that the statemachine that is created by the translation contains the correct -translations for each of the elements. -|*) +translations for each of the elements *) Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : @@ -142,7 +134,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall n op args dst s s' e i, Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vblock (Vvar dst) e) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, Z.pos n1 <= Int.max_unsigned -> @@ -160,14 +152,14 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c dst n, Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src)) + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) (state_goto st n). -(* tr_instr_Ijumptable : +(*| tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) @@ -186,13 +178,12 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts t Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls r_en r_u_en r_addr r_wr_en r_d_in r_d_out, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3 wf4, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st fin rtrn start rst clk scldecls arrdecls - (mk_ram stk_len stk r_en r_u_en r_addr r_wr_en r_d_in r_d_out)) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> @@ -205,12 +196,6 @@ Inductive tr_module (f : RTL.function) : module -> Prop := start = ((RTL.max_reg_function f) + 5)%positive -> rst = ((RTL.max_reg_function f) + 6)%positive -> clk = ((RTL.max_reg_function f) + 7)%positive -> - r_en = ((RTL.max_reg_function f) + 8)%positive -> - r_u_en = ((RTL.max_reg_function f) + 9)%positive -> - r_addr = ((RTL.max_reg_function f) + 10)%positive -> - r_wr_en = ((RTL.max_reg_function f) + 11)%positive -> - r_d_in = ((RTL.max_reg_function f) + 12)%positive -> - r_d_out = ((RTL.max_reg_function f) + 13)%positive -> tr_module f m. #[local] Hint Constructors tr_module : htlspec. @@ -549,7 +534,7 @@ Proof. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold block. replace (st_st s4) with (st_st s2) by congruence. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. econstructor. apply Z.leb_le; assumption. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. @@ -659,7 +644,7 @@ Proof. assert (EQ3D := EQ3). apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. - (*replace (st_controllogic s10) with (st_controllogic s3) by congruence. + replace (st_controllogic s10) with (st_controllogic s3) by congruence. replace (st_datapath s10) with (st_datapath s3) by congruence. replace (st_st s10) with (st_st s3) by congruence. eapply iter_expand_instr_spec; eauto with htlspec. @@ -669,4 +654,3 @@ Proof. erewrite <- collect_declare_freshreg_trans; try eassumption. lia. Qed. -*)Admitted. |