diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-02 10:26:23 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-02 10:26:23 +0000 |
| commit | a2199f6bf69ae5cbbdb15227f8828b914baa4348 (patch) | |
| tree | c5e274800ba57fdbe7d88ac9c4418b3046eed8e3 /src/hls/Veriloggenproof.v | |
| parent | a90265c71d6d5c5ec031a8385f977c050bdd7975 (diff) | |
| download | vericert-a2199f6bf69ae5cbbdb15227f8828b914baa4348.tar.gz vericert-a2199f6bf69ae5cbbdb15227f8828b914baa4348.zip | |
Admit Veriloggenproof
Diffstat (limited to 'src/hls/Veriloggenproof.v')
| -rw-r--r-- | src/hls/Veriloggenproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 99828e4..5c484d3 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -277,7 +277,8 @@ Section CORRECTNESS. exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. induction 1; intros R1 MSTATE; inv MSTATE. - - econstructor; split. apply Smallstep.plus_one. econstructor. + Admitted. +(* - econstructor; split. apply Smallstep.plus_one. econstructor. assumption. assumption. eassumption. apply valueToPos_posToValue. split. lia. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. @@ -325,7 +326,7 @@ Section CORRECTNESS. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. apply match_state. assumption. - Qed. + Qed.*) Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : |