diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-11 17:15:39 +0100 |
| commit | 6ad3f69cf04d0055b7987e6e4c858a64d3b1693c (patch) | |
| tree | c686b80ee30c1280f005c27d60a6344bbee8d646 /src/hls/DMemorygen.v | |
| parent | 05afcff334725e885522e9859b9ab735a404014c (diff) | |
| download | vericert-6ad3f69cf04d0055b7987e6e4c858a64d3b1693c.tar.gz vericert-6ad3f69cf04d0055b7987e6e4c858a64d3b1693c.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). |