diff options
-rw-r--r-- | src/translation/Veriloggen.v | 6 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 8 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 7 |
3 files changed, 12 insertions, 9 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f0ec576..f5d5fa7 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -28,12 +28,12 @@ Definition transl_list_fun (a : node * Verilog.stmnt) := Definition transl_list st := map transl_list_fun st. Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := - match a with (r, (io, VScalar sz)) => Vdeclaration (Vdecl io r sz) end. + match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := - match a with (r, (io, VArray sz l)) => Vdeclaration (Vdeclarr io r sz l) end. + match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. @@ -45,7 +45,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue 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)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) m.(mod_reset) diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 3052d03..ee0aa64 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -195,8 +195,12 @@ Section CORRECTNESS. Lemma mis_stepp_decl : forall l asr asa f, - mis_stepp f asr asa l asr asa. - Admitted. + mis_stepp f asr asa (map Vdeclaration l) asr asa. + Proof. + induction l. + - intros. constructor. + - intros. simplify. econstructor. constructor. auto. + Qed. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 1513330..064474a 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -610,8 +610,8 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 | mi_stepp_Vdecl : - forall f sr sa lhs rhs io, - mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa. + forall f sr sa d, + mi_stepp f sr sa (Vdeclaration d) sr sa. Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> @@ -743,8 +743,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m asr i r sf pc mst asa, mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) - asa). + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := |