diff options
| -rw-r--r-- | src/translation/Veriloggenproof.v | 33 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 4 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 2 |
3 files changed, 24 insertions, 15 deletions
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 825cb7e..e556c69 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,8 +17,8 @@ *) From compcert Require Import Smallstep Linking. -From coqup Require Import Veriloggen. -From coqup Require HTL Verilog. +From coqup Require HTL. +From coqup Require Import Coquplib Veriloggen Verilog. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. @@ -29,47 +29,52 @@ Proof. intros. eapply match_transform_program_contextual. auto. Qed. -Inductive match_stacks : list HTL.stackframe -> list Verilog.stackframe -> Prop := +Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := | match_stack : forall res m pc reg_assoc arr_assoc hstk vstk, match_stacks hstk vstk -> match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) - (Verilog.Stackframe res (transl_module m) pc + (Stackframe res (transl_module m) pc reg_assoc arr_assoc :: vstk) | match_stack_nil : match_stacks nil nil. -Inductive match_states : HTL.state -> Verilog.state -> Prop := +Inductive match_states : HTL.state -> state -> Prop := | match_state : forall m st reg_assoc arr_assoc hstk vstk, match_stacks hstk vstk -> match_states (HTL.State hstk m st reg_assoc arr_assoc) - (Verilog.State vstk (transl_module m) st reg_assoc arr_assoc) + (State vstk (transl_module m) st reg_assoc arr_assoc) | match_returnstate : forall v hstk vstk, match_stacks hstk vstk -> - match_states (HTL.Returnstate hstk v) (Verilog.Returnstate vstk v) + match_states (HTL.Returnstate hstk v) (Returnstate vstk v) | match_initial_call : forall m, - match_states (HTL.Callstate nil m nil) (Verilog.Callstate nil (transl_module m) nil). + match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). Section CORRECTNESS. Variable prog: HTL.program. - Variable tprog: Verilog.program. + Variable tprog: program. Hypothesis TRANSL : match_prog prog tprog. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : Verilog.genv := Globalenvs.Genv.globalenv tprog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. - Theorem transl_step_correct: + Lemma stmnt_in_case : + exists e st, + + Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> - forall (R1 : Verilog.state), + forall (R1 : state), match_states S1 R1 -> - exists R2, Smallstep.plus Verilog.step tge R1 t R2 /\ match_states S2 R2. + exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE. + induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. + - apply Smallstep.plus_one. econstructor. econstructor. + * econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 0bf5072..a3623f0 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -99,12 +99,14 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data + forall g m st sf ctrl data ist asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 asr' asa' f stval pstval, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 9c05fc9..d476710 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -713,6 +713,8 @@ 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, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) (mkassociations asa (empty_stack m)) m.(mod_body) |