diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 75d5321..c7dbe72 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -179,12 +179,13 @@ 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 wf1 wf2 wf3 wf4, + 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, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) -> + 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)) -> (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) -> @@ -197,6 +198,12 @@ 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. @@ -645,7 +652,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. @@ -655,3 +662,4 @@ Proof. erewrite <- collect_declare_freshreg_trans; try eassumption. lia. Qed. +*)Admitted. |