aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/translation/HTLgenproof.v43
-rw-r--r--src/translation/Veriloggen.v4
-rw-r--r--src/translation/Veriloggenproof.v58
-rw-r--r--src/verilog/HTL.v4
-rw-r--r--src/verilog/Verilog.v11
5 files changed, 95 insertions, 25 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 08b1216..753dccf 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -2106,16 +2106,29 @@ Section CORRECTNESS.
Admitted.
Hint Resolve transl_step_correct : htlproof.
- Lemma main_tprog_internal :
- forall b f,
- Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
- Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
- Admitted.
Lemma option_inv :
forall A x y,
@Some A x = Some y -> x = y.
- Proof. intros. inversion H. trivial. Qed.
+ Proof. intros. inversion H. trivial. Qed.
+
+ Lemma main_tprog_internal :
+ forall b,
+ Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
+ exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
+ Proof.
+ intros.
+ destruct TRANSL. unfold main_is_internal in H1.
+ repeat (unfold_match H1). replace b with b0.
+ exploit function_ptr_translated; eauto. intros [tf [A B]].
+ unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B.
+ unfold_match B. inv B. econstructor. apply A.
+
+ apply option_inv. rewrite <- Heqo. rewrite <- H.
+ rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+ trivial. symmetry; eapply Linking.match_program_main; eauto.
+ Qed.
+
(* Had to admit proof because currently there is no way to force main to be Internal. *)
Lemma transl_initial_states :
@@ -2136,21 +2149,23 @@ Section CORRECTNESS.
unfold transl_fundef, Errors.bind in B.
unfold AST.transf_partial_fundef, Errors.bind in B.
repeat (unfold_match B). inversion B. subst.
+ exploit main_tprog_internal; eauto; intros.
+ rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+ apply Heqo. symmetry; eapply Linking.match_program_main; eauto.
+ inversion H5.
econstructor; split. econstructor.
apply (Genv.init_mem_transf_partial TRANSL'); eauto.
replace (AST.prog_main tprog) with (AST.prog_main prog).
rewrite symbols_preserved; eauto.
symmetry; eapply Linking.match_program_main; eauto.
- apply main_tprog_internal. replace ge0 with ge in * by auto.
- replace b0 with b in *. rewrite symbols_preserved.
- replace (AST.prog_main tprog) with (AST.prog_main prog).
- assumption.
- symmetry; eapply Linking.match_program_main; eauto.
- apply option_inv. rewrite <- H0. rewrite <- Heqo.
- trivial.
+ apply H6.
constructor.
- apply transl_module_correct. eassumption.
+ apply transl_module_correct.
+ assert (Some (AST.Internal x) = Some (AST.Internal m)).
+ replace (AST.fundef HTL.module) with (HTL.fundef).
+ rewrite <- H6. setoid_rewrite <- A. trivial.
+ trivial. inv H7. assumption.
Qed.
Hint Resolve transl_initial_states : htlproof.
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 6c58c56..db96949 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -16,16 +16,66 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-From compcert Require Import Smallstep.
-From coqup Require HTL Verilog.
+From compcert Require Import Smallstep Linking.
+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.
+
+Lemma transf_program_match:
+ forall prog, match_prog prog (transl_program prog).
+Proof.
+ intros. eapply match_transform_program_contextual. auto.
+Qed.
+
+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)
+ (Stackframe res (transl_module m) pc
+ reg_assoc arr_assoc :: vstk)
+| match_stack_nil : match_stacks nil nil.
+
+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)
+ (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) (Returnstate vstk v)
+| match_initial_call :
+ forall m,
+ 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 : genv := Globalenvs.Genv.globalenv tprog.
+
+ Theorem transl_step_correct :
+ forall (S1 : HTL.state) t S2,
+ HTL.step ge S1 t S2 ->
+ forall (R1 : state),
+ match_states S1 R1 ->
+ 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. eassumption. trivial.
+ * econstructor. econstructor.
Theorem transf_program_correct:
forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
- Admitted.
+
End CORRECTNESS.
+
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 7d5e3c0..555ddbd 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -279,7 +279,8 @@ Inductive stackframe : Type :=
forall (res : reg)
(m : module)
(pc : node)
- (assoc : assocmap),
+ (reg_assoc : assocmap_reg)
+ (arr_assoc : assocmap_arr),
stackframe.
Inductive state : Type :=
@@ -711,7 +712,9 @@ 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)
(mkassociations asa (empty_stack m))
m.(mod_body)
@@ -735,9 +738,9 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
(init_params args m.(mod_args)))
(empty_stack m))
| step_return :
- forall g m asr i r sf pc mst,
+ forall g m asr i r sf pc mst asa,
mst = mod_st m ->
- step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
+ step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
(State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
(empty_stack m)).
Hint Constructors step : verilog.
generated by cgit (git 2.34.1) at 2024-07-07 16:58:15 +0000