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 | |
| parent | cf9949a5151aa9ed86554fb31c2a56fad0614a10 (diff) | |
| download | vericert-50ec2fb12454c2bc1f902c955f0b81df71b58c39.tar.gz vericert-50ec2fb12454c2bc1f902c955f0b81df71b58c39.zip | |
Fix Verilog semantics and fix order of always blocks
| -rw-r--r-- | src/translation/Veriloggen.v | 4 | ||||
| -rw-r--r-- | src/translation/Veriloggenproof.v | 7 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 2 |
3 files changed, 5 insertions, 8 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 2b9974b..b550ff9 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -43,10 +43,10 @@ Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in let body := - Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) - :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) 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). diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index d476710..555ddbd 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -712,7 +712,7 @@ Definition empty_stack (m : module) : assocmap_arr := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g, + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) |