diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-26 09:40:16 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-26 09:40:31 +0100 |
| commit | 50ec2fb12454c2bc1f902c955f0b81df71b58c39 (patch) | |
| tree | 8ffd09be682442cedddc6106c242962e614e236c /src/translation/Veriloggenproof.v | |
| parent | cf9949a5151aa9ed86554fb31c2a56fad0614a10 (diff) | |
| download | vericert-kvx-50ec2fb12454c2bc1f902c955f0b81df71b58c39.tar.gz vericert-kvx-50ec2fb12454c2bc1f902c955f0b81df71b58c39.zip | |
Fix Verilog semantics and fix order of always blocks
Diffstat (limited to 'src/translation/Veriloggenproof.v')
| -rw-r--r-- | src/translation/Veriloggenproof.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index e556c69..db96949 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -62,9 +62,6 @@ Section CORRECTNESS. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog. - Lemma stmnt_in_case : - exists e st, - Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> @@ -73,8 +70,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. econstructor. - * econstructor. + - apply Smallstep.plus_one. econstructor. eassumption. trivial. + * econstructor. econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). |