diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-06 23:08:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-06 23:08:03 +0100 |
| commit | 23a2a2fb2916a7ecb240aa51686bbe049f8418e4 (patch) | |
| tree | f5f9cf0001bbd44cfaab7d70f3c169b8275be15d /src/hls/HTLgenspec.v | |
| parent | 873162771e87c6c358dc07e58bc0bd3a08f9a00e (diff) | |
| download | vericert-23a2a2fb2916a7ecb240aa51686bbe049f8418e4.tar.gz vericert-23a2a2fb2916a7ecb240aa51686bbe049f8418e4.zip | |
Finish load and store proof, but broke top-level
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 7cb6d8c..6a10fa2 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -178,12 +178,12 @@ Hint Constructors tr_code : htlspec. 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 wf, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3) -> (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) -> @@ -648,5 +648,9 @@ Proof. 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. + rewrite H5. rewrite H7. apply EQ2. apply PTree.elements_complete. + eauto with htlspec. + erewrite <- collect_declare_freshreg_trans; try eassumption. + lia. Qed. |