diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
commit | b32e7574864cde80f8f5283431c21a6803a89108 (patch) | |
tree | f30babb0db7e5797cb77f6ac44a682cb9b8b105b /src/hls/DMemorygen.v | |
parent | c321e39de166308d8db2f6ebe577edb3297b507c (diff) | |
download | vericert-b32e7574864cde80f8f5283431c21a6803a89108.tar.gz vericert-b32e7574864cde80f8f5283431c21a6803a89108.zip |
Fix backend hardware generation and scheduling
Diffstat (limited to 'src/hls/DMemorygen.v')
-rw-r--r-- | src/hls/DMemorygen.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index 0ac0ff0..bef9f3d 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -298,7 +298,7 @@ Proof. lia. Qed. Lemma module_ram_wf' : forall m addr, addr = max_reg_module m + 1 -> - mod_clk m < addr. + mod_preg m < addr. Proof. unfold max_reg_module; lia. Qed. Definition transf_module (m: module): module. @@ -326,6 +326,7 @@ Definition transf_module (m: module): module. (mod_start m) (mod_reset m) (mod_clk m) + (mod_preg m) (AssocMap.set u_en (None, VScalar 1) (AssocMap.set en (None, VScalar 1) (AssocMap.set wr_en (None, VScalar 1) @@ -3374,7 +3375,7 @@ Section CORRECTNESS. { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. + unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H15. auto. - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). replace (mod_reset (transf_module m)) with (mod_reset m). |