diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 9 | ||||
-rw-r--r-- | src/Simulator.v | 3 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 4 | ||||
-rw-r--r-- | src/translation/HTLgen.v | 108 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 6 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 105 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 684 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 23 | ||||
-rw-r--r-- | src/translation/Veriloggenspec.v | 113 | ||||
-rw-r--r-- | src/verilog/HTL.v | 7 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.ml | 46 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
-rw-r--r-- | src/verilog/Test.v | 99 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 183 |
14 files changed, 364 insertions, 1028 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index e998521..98ef429 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -74,9 +74,12 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. -Definition transf_backend (r : RTL.program) : res Verilog.module := +Definition transf_backend (r : RTL.program) : res Verilog.program := OK r - @@@ Veriloggen.transf_program. + @@@ Inlining.transf_program + @@ print (print_RTL 1) + @@@ HTLgen.transl_program + @@ Veriloggen.transl_program. Definition transf_frontend (p: Csyntax.program) : res RTL.program := OK p @@ -88,7 +91,7 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program := @@@ RTLgen.transl_program @@ print (print_RTL 0). -Definition transf_hls (p : Csyntax.program) : res Verilog.module := +Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ transf_frontend @@@ transf_backend. diff --git a/src/Simulator.v b/src/Simulator.v index 930971b..83d3e96 100644 --- a/src/Simulator.v +++ b/src/Simulator.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Import FSets.FMapPositive. +(*From Coq Require Import FSets.FMapPositive. From compcert Require Import Errors. @@ -33,3 +33,4 @@ Definition simulate (n : nat) (m : Verilog.module) : res (Value.value * list (po end. Local Close Scope error_monad_scope. +*) diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 0028fcb..ba87af6 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Verilog Value Compiler Simulator. +From coqup Require Verilog Value Compiler. From Coq Require DecidableClass. @@ -166,7 +166,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls Simulator.simulate + Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index cba2940..c73aaa7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,7 +17,7 @@ *) From compcert Require Import Maps. -From compcert Require Errors. +From compcert Require Errors Globalenvs. From compcert Require Import AST RTL. From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. @@ -27,15 +27,12 @@ Hint Resolve AssocMap.gss : htlh. Hint Resolve Ple_refl : htlh. Hint Resolve Ple_succ : htlh. -Inductive scl_decl : Type := Scalar (sz : nat). -Inductive arr_decl : Type := Array (sz : nat) (ln : nat). - Record state: Type := mkstate { st_st : reg; st_freshreg: reg; st_freshstate: node; - st_scldecls: AssocMap.t scl_decl; - st_arrdecls: AssocMap.t arr_decl; + st_scldecls: AssocMap.t (option io * scl_decl); + st_arrdecls: AssocMap.t (option io * arr_decl); st_datapath: datapath; st_controllogic: controllogic; }. @@ -44,8 +41,8 @@ Definition init_state (st : reg) : state := mkstate st 1%positive 1%positive - (AssocMap.empty scl_decl) - (AssocMap.empty arr_decl) + (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty (option io * arr_decl)) (AssocMap.empty stmnt) (AssocMap.empty stmnt). @@ -127,6 +124,30 @@ Proof. auto with htlh. Qed. +Lemma declare_reg_state_incr : + forall i s r sz, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Proof. auto with htlh. Qed. + +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := + fun s => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr i s r sz). + Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with @@ -338,9 +359,11 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Inop n' => add_instr n n' Vskip | Iop op args dst n' => do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; add_instr n n' (nonblock dst instr) | Iload mem addr args dst n' => do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; add_instr n n' (block dst src) | Istore mem addr args src n' => do dst <- translate_arr_access mem addr args stack; @@ -363,61 +386,62 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni end. Lemma create_reg_state_incr: - forall s sz, + forall s sz i, st_incr s (mkstate s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) s.(st_arrdecls) (st_datapath s) (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. -Definition create_reg (sz : nat) : mon reg := +Definition create_reg (i : option io) (sz : nat) : mon reg := fun s => let r := s.(st_freshreg) in OK r (mkstate s.(st_st) (Pos.succ r) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) (st_controllogic s)) - (create_reg_state_incr s sz). + (create_reg_state_incr s sz i). Lemma create_arr_state_incr: - forall s sz ln, + forall s sz ln i, st_incr s (mkstate s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. -Definition create_arr (sz : nat) (ln : nat) : mon (reg * nat) := +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := fun s => let r := s.(st_freshreg) in OK (r, ln) (mkstate s.(st_st) (Pos.succ r) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)) - (create_arr_state_incr s sz ln). + (create_arr_state_incr s sz ln i). Definition transf_module (f: function) : mon module := - do fin <- create_reg 1; - do rtrn <- create_reg 32; - do (stack, stack_len) <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do start <- create_reg 1; - do rst <- create_reg 1; - do clk <- create_reg 1; + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; do current_state <- get; ret (mkmodule f.(RTL.fn_params) @@ -428,14 +452,19 @@ Definition transf_module (f: function) : mon module := stack stack_len fin - rtrn). + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls)). Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) - (st_scldecls (init_state st)) + (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). @@ -443,15 +472,30 @@ Definition max_state (f: function) : state := Definition transl_module (f : function) : Errors.res module := run_mon (max_state f) (transf_module f). -Definition transl_fundef (f : RTL.fundef) : Errors.res HTL.fundef := +Definition transl_fundef := transf_partial_fundef transl_module. + +Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. + +(*Definition transl_main_fundef f : Errors.res HTL.fundef := match f with - | Internal f' => - Errors.bind (transl_module f') - (fun f'' => Errors.OK (Internal f'')) - | _ => Errors.Error (Errors.msg "External function could not be translated.") + | Internal f => transl_fundef (Internal f) + | External f => Errors.Error (Errors.msg "Could not find internal main function") end. (** Translation of a whole program. *) Definition transl_program (p: RTL.program) : Errors.res HTL.program := - transform_partial_program transl_fundef p. + transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i + then transl_fundef f + else transl_main_fundef f) + (fun i v => Errors.OK v) p. +*) + +(*Definition main_is_internal (p : RTL.program): Prop := + let ge := Globalenvs.Genv.globalenv p in + forall b m, + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m). + +Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }. +*) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 6dc4c21..773497b 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -724,6 +724,7 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_step_correct : htlproof. + (* Had to admit proof because currently there is no way to force main to be Internal. *) Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> @@ -740,10 +741,11 @@ Section CORRECTNESS. replace (AST.prog_main tprog) with (AST.prog_main prog). rewrite symbols_preserved; eauto. symmetry; eapply Linking.match_program_main; eauto. - eexact A. trivial. + Admitted. + (*eexact A. trivial. constructor. apply transl_module_correct. auto. - Qed. + Qed.*) Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 89b79ac..57d2d87 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,7 +184,7 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> @@ -192,34 +192,48 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> tr_module f m. Hint Constructors tr_module : htlspec. Lemma create_reg_datapath_trans : - forall sz s s' x i, - create_reg sz s = OK x s' i -> + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_datapath_trans : htlspec. Lemma create_reg_controllogic_trans : - forall sz s s' x i, - create_reg sz s = OK x s' i -> + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_datapath_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma declare_reg_controllogic_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_controllogic_trans : htlspec. Lemma create_arr_datapath_trans : - forall sz ln s s' x i, - create_arr sz ln s = OK x s' i -> + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_arr_datapath_trans : htlspec. Lemma create_arr_controllogic_trans : - forall sz ln s s' x i, - create_arr sz ln s = OK x s' i -> + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_arr_controllogic_trans : htlspec. @@ -240,11 +254,11 @@ Hint Resolve get_refl_s : htlspec. Ltac inv_incr := repeat match goal with - | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] => + | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => let H1 := fresh "H" in assert (H1 := H); eapply create_reg_datapath_trans in H; eapply create_reg_controllogic_trans in H1 - | [ H: create_arr _ _ ?s = OK _ ?s' _ |- _ ] => + | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => let H1 := fresh "H" in assert (H1 := H); eapply create_arr_datapath_trans in H; eapply create_arr_controllogic_trans in H1 @@ -256,6 +270,44 @@ Ltac inv_incr := | [ H: st_incr _ _ |- _ ] => destruct st_incr end. +Lemma collect_controllogic_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_datapath_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_declare_controllogic_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. eapply collect_controllogic_trans; try eassumption. + intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_datapath_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. eapply collect_datapath_trans; try eassumption. + intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. +Qed. + Ltac rewrite_states := match goal with | [ H: ?x ?s = ?x ?s' |- _ ] => @@ -330,16 +382,17 @@ Proof. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. eapply in_map with (f := fst) in H9. contradiction. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor. - eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H9. contradiction. + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. unfold nonblock. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST. + constructor. eapply translate_instr_tr_op. apply EQ1. + eapply in_map with (f := fst) in H14. contradiction. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1. - eapply in_map with (f := fst) in H9. contradiction. + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence. + rewrite HST. econstructor. apply EQ1. + eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. @@ -407,9 +460,13 @@ Proof. econstructor; simpl; trivial. intros. inv_incr. - assert (STC: st_controllogic s9 = st_controllogic s3) by congruence. - assert (STD: st_datapath s9 = st_datapath s3) by congruence. - assert (STST: st_st s9 = st_st s3) by congruence. + assert (EQ3D := EQ3). + destruct x3. + apply collect_declare_datapath_trans in EQ3. + apply collect_declare_controllogic_trans in EQ3D. + assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. + assert (STD: st_datapath s10 = st_datapath s3) by congruence. + assert (STST: st_st s10 = st_st s3) by congruence. rewrite STC. rewrite STD. rewrite STST. eapply iter_expand_instr_spec; eauto with htlspec. apply PTree.elements_complete. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 4a6f23e..efe3565 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -16,655 +16,51 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Import FSets.FMapPositive. +From compcert Require Import Maps. +From compcert Require Errors. +From compcert Require Import AST. +From coqup Require Import Verilog HTL Coquplib AssocMap Value. -From coqup Require Import Verilog Coquplib Value. - -From compcert Require Errors Op AST Integers Maps. -From compcert Require Import RTL. - -Notation "a ! b" := (PositiveMap.find b a) (at level 1). - -Definition node : Type := positive. -Definition reg : Type := positive. -Definition ident : Type := positive. - -Hint Resolve PositiveMap.gempty : verilog_state. -Hint Resolve PositiveMap.gso : verilog_state. -Hint Resolve PositiveMap.gss : verilog_state. -Hint Resolve Ple_refl : verilog_state. - -Inductive statetrans : Type := -| StateGoto (p : node) -| StateCond (c : expr) (t f : node). - -Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue 32 n)). - -Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). - -Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt := +Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) := match st with - | StateGoto p => state_goto stvar p - | StateCond c t f => state_cond stvar c t f + | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls + | nil => nil end. -Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) := - forall (n: node), - Plt n fs \/ stm!n = None. -Hint Unfold valid_freshstate : verilog_state. - -Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t statetrans) := - forall (n: node), - (forall x, stm!n = Some x -> exists y, st!n = Some y) - /\ (forall x, st!n = Some x -> exists y, stm!n = Some y). -Hint Unfold states_have_transitions : verilog_state. - -Record decl : Type := mkdecl { - width: nat; - length: nat -}. - -Record state: Type := mkstate { - st_freshreg: reg; - st_freshstate: node; - st_stm: PositiveMap.t stmnt; - st_statetrans: PositiveMap.t statetrans; - st_decl: PositiveMap.t decl; - st_wf: valid_freshstate st_stm st_freshstate - /\ states_have_transitions st_stm st_statetrans; -}. - -Remark init_state_valid_freshstate: - valid_freshstate (PositiveMap.empty stmnt) 1%positive. -Proof. auto with verilog_state. Qed. -Hint Resolve init_state_valid_freshstate : verilog_state. - -Remark init_state_states_have_transitions: - states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). -Proof. - unfold states_have_transitions. - split; intros; rewrite PositiveMap.gempty in H; discriminate. -Qed. -Hint Resolve init_state_states_have_transitions : verilog_state. - -Remark init_state_wf: - valid_freshstate (PositiveMap.empty stmnt) 1%positive - /\ states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). -Proof. auto with verilog_state. Qed. - -Definition init_state : state := - mkstate 1%positive - 1%positive - (PositiveMap.empty stmnt) - (PositiveMap.empty statetrans) - (PositiveMap.empty decl) - init_state_wf. - -Inductive state_incr: state -> state -> Prop := - state_incr_intro: - forall (s1 s2: state), - Ple s1.(st_freshreg) s2.(st_freshreg) -> - Ple s1.(st_freshstate) s2.(st_freshstate) -> - (forall n, - s1.(st_stm)!n = None \/ s2.(st_stm)!n = s1.(st_stm)!n) -> - (forall n, - s1.(st_statetrans)!n = None - \/ s2.(st_statetrans)!n = s1.(st_statetrans)!n) -> - state_incr s1 s2. -Hint Constructors state_incr : verilog_state. - -Lemma state_incr_refl: - forall s, state_incr s s. -Proof. auto with verilog_state. Qed. - -Lemma state_incr_trans: - forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. -Proof. - intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans. - - intros. destruct H3 with n. - + left; assumption. - + destruct H6 with n; - [ rewrite <- H0; left; assumption - | right; rewrite <- H0; apply H8 - ]. - - intros. destruct H4 with n. - + left; assumption. - + destruct H7 with n. - * rewrite <- H0. left. assumption. - * right. rewrite <- H0. apply H8. -Qed. - -Inductive res (A: Type) (s: state): Type := -| Error : Errors.errmsg -> res A s -| OK : A -> forall (s' : state), state_incr s s' -> res A s. - -Arguments OK [A s]. -Arguments Error [A s]. - -Definition mon (A: Type) : Type := forall (s: state), res A s. - -Definition ret {A: Type} (x: A) : mon A := - fun (s : state) => OK x s (state_incr_refl s). - -Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := - fun (s : state) => - match f s with - | Error msg => Error msg - | OK a s' i => - match g a s' with - | Error msg => Error msg - | OK b s'' i' => OK b s'' (state_incr_trans s s' s'' i i') - end - end. - -Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := - bind f (fun xy => g (fst xy) (snd xy)). - -Notation "'do' X <- A ; B" := (bind A (fun X => B)) -(at level 200, X ident, A at level 100, B at level 200). -Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) -(at level 200, X ident, Y ident, A at level 100, B at level 200). - -Definition handle_error {A: Type} (f g: mon A) : mon A := - fun (s : state) => - match f s with - | OK a s' i => OK a s' i - | Error _ => g s - end. - -Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: state) => Error err. - -Definition get : mon state := fun s => OK s s (state_incr_refl s). - -Definition set (s: state) (i: forall s', state_incr s' s) : mon unit := - fun s' => OK tt s (i s'). - -Definition run_mon {A: Type} (s: state) (m: mon A): Errors.res A := - match m s with - | OK a s' i => Errors.OK a - | Error err => Errors.Error err - end. - -Definition map_state (f: state -> state) (i: forall s, state_incr s (f s)): mon state := - fun s => let s' := f s in OK s' s' (i s). - -Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := - match l with - | nil => ret nil - | x::xs => - do r <- f x; - do rs <- traverselist f xs; - ret (r::rs) +Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := + match scldecl with + | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' + | nil => nil end. -Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. -Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. - -Definition bop (op : binop) (r1 r2 : reg) : expr := - Vbinop op (Vvar r1) (Vvar r2). - -Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := - Vbinop op (Vvar r) (Vlit (intToValue l)). - -Definition boplitz (op: binop) (r: reg) (l: Z) : expr := - Vbinop op (Vvar r) (Vlit (ZToValue 32 l)). - -Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := - match c, args with - | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) - | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) - | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) - | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) - | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) - | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) - | _, _ => error (Errors.msg "Veriloggen: comparison instruction not implemented: other") +Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := + match arrdecl with + | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' + | nil => nil end. -Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) - : mon expr := - match c, args with - | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) - | Integers.Cne, r1::nil => ret (boplit Vne r1 i) - | Integers.Clt, r1::nil => ret (boplit Vlt r1 i) - | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) - | Integers.Cle, r1::nil => ret (boplit Vle r1 i) - | Integers.Cge, r1::nil => ret (boplit Vge r1 i) - | _, _ => error (Errors.msg "Veriloggen: comparison_imm instruction not implemented: other") - end. - -Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := - match c, args with - | Op.Ccomp c, _ => translate_comparison c args - | Op.Ccompu c, _ => translate_comparison c args - | Op.Ccompimm c i, _ => translate_comparison_imm c args i - | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero") - | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero") - | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other") - end. - -Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := - match a, args with - | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) - | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) - | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - | Op.Aindexed2scaled scale offset, r1::r2::nil => - ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (* Stack arrays/referenced variables *) - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vlit (ZToValue 32 (a / 4))) - else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other") - end. - -(** Translate an instruction to a statement. *) -Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := - match op, args with - | Op.Omove, r::nil => ret (Vvar r) - | Op.Ointconst n, _ => ret (Vlit (intToValue n)) - | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r)) - | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) - | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) - | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs") - | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu") - | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) - | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) - | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) - | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) - | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) - | Op.Oandimm n, r::nil => ret (boplit Vand r n) - | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) - | Op.Oorimm n, r::nil => ret (boplit Vor r n) - | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2) - | Op.Oxorimm n, r::nil => ret (boplit Vxor r n) - | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r)) - | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2) - | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) - | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) - | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm") - | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru") - | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm") - | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm") - | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm") - | Op.Ocmp c, _ => translate_condition c args - | Op.Olea a, _ => translate_eff_addressing a args - | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *) - | Op.Ocast32signed, r::nill => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *) - | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other") - end. - -Remark add_instr_valid_freshstate: - forall (s: state) (n: node) (st: stmnt), - Plt n (st_freshstate s) -> - valid_freshstate (PositiveMap.add n st s.(st_stm)) (st_freshstate s). -Proof. - unfold valid_freshstate. intros. - case (peq n0 n); intro. - subst n0. left. assumption. - rewrite PositiveMap.gso. - apply (st_wf s). assumption. -Qed. -Hint Resolve add_instr_valid_freshstate : verilog_state. - -Remark add_instr_states_have_transitions: - forall (s: state) (n n': node) (st: stmnt), - states_have_transitions - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans)). -Proof. - unfold states_have_transitions. split; intros. - - case (peq n0 n); intro. - subst. exists (StateGoto n'). apply PositiveMap.gss. - rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. - assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1. - destruct H1 with n0. apply H2 with x. assumption. assumption. assumption. - - case (peq n0 n); intro. - subst. exists st. apply PositiveMap.gss. - rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. - assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1. - destruct H1 with n0. apply H3 with x. assumption. assumption. assumption. -Qed. -Hint Resolve add_instr_states_have_transitions : verilog_state. - -Remark add_instr_state_wf: - forall (s: state) (n n': node) (st: stmnt) (LT: Plt n (st_freshstate s)), - valid_freshstate (PositiveMap.add n st (st_stm s)) (st_freshstate s) - /\ states_have_transitions - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans)). -Proof. auto with verilog_state. Qed. - -Lemma add_instr_state_incr : - forall s n n' st LT, - (st_stm s)!n = None -> - (st_statetrans s)!n = None -> - state_incr s - (mkstate s.(st_freshreg) - (st_freshstate s) - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans)) - s.(st_decl) - (add_instr_state_wf s n n' st LT)). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with verilog_state. -Qed. - -Definition check_empty_node_stm: - forall (s: state) (n: node), { s.(st_stm)!n = None } + { True }. -Proof. - intros. case (s.(st_stm)!n); intros. right; auto. left; auto. -Defined. - -Definition check_empty_node_statetrans: - forall (s: state) (n: node), { s.(st_statetrans)!n = None } + { True }. -Proof. - intros. case (s.(st_statetrans)!n); intros. right; auto. left; auto. -Defined. - -Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := - fun s => - match plt n (st_freshstate s), check_empty_node_stm s n, check_empty_node_statetrans s n with - | left LT, left STM, left TRANS => - OK tt (mkstate s.(st_freshreg) - (st_freshstate s) - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans)) - s.(st_decl) - (add_instr_state_wf s n n' st LT)) - (add_instr_state_incr s n n' st LT STM TRANS) - | _, _, _ => Error (Errors.msg "Veriloggen.add_instr") - end. - -(** Add a register to the state without changing the [st_freshreg], as this -should already be the right value. This can be assumed because the max register -is taken from the RTL code. *) - -Definition add_reg (r: reg) (s: state) : state := - mkstate (st_freshreg s) - (st_freshstate s) - (st_stm s) - (st_statetrans s) - (PositiveMap.add r (mkdecl 32 0) (st_decl s)) - (st_wf s). - -Lemma add_reg_state_incr: - forall r s, - state_incr s (add_reg r s). -Proof. auto with verilog_state. Qed. - -Definition add_instr_reg (r: reg) (n: node) (n': node) (st: stmnt) : mon unit := - do _ <- map_state (add_reg r) (add_reg_state_incr r); - add_instr n n' st. - -Lemma change_decl_state_incr: - forall s decl', - state_incr s (mkstate - (st_freshreg s) - (st_freshstate s) - (st_stm s) - (st_statetrans s) - decl' - (st_wf s)). -Proof. auto with verilog_state. Qed. - -Lemma decl_io_state_incr: - forall s, - state_incr s (mkstate - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (st_stm s) - (st_statetrans s) - (st_decl s) - (st_wf s)). -Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed. - -(** Declare a new register by incrementing the [st_freshreg] by one and -returning the old [st_freshreg]. *) - -Definition decl_io (d: decl) : mon (reg * decl) := - fun s => let r := s.(st_freshreg) in - OK (r, d) (mkstate - (Pos.succ r) - (st_freshstate s) - (st_stm s) - (st_statetrans s) - (st_decl s) - (st_wf s)) - (decl_io_state_incr s). - -(** Declare a new register which is given, by changing [st_decl] and without -affecting anything else. *) - -Definition declare_reg (r: reg) (d: decl): mon (reg * decl) := - fun s => OK (r, d) (mkstate - (st_freshreg s) - (st_freshstate s) - (st_stm s) - (st_statetrans s) - (PositiveMap.add r d s.(st_decl)) - (st_wf s)) - (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))). - -(** Declare a new fresh register by first getting a valid register to increment, -and then adding it to the declaration list. *) - -Definition decl_fresh_reg (d: decl) : mon (reg * decl) := - do (r, d) <- decl_io d; - declare_reg r d. - -Lemma add_branch_instr_states_have_transitions: - forall s e n n1 n2, - states_have_transitions (PositiveMap.add n Vskip (st_stm s)) - (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)). -Proof. - split; intros; destruct (peq n0 n); subst; eauto with verilog_state; - rewrite PositiveMap.gso in *; - assert (H1 := (st_wf s)); inv H1; unfold states_have_transitions in H2; - destruct H2 with n0; try (apply H1 with x); try (apply H3 with x); assumption. -Qed. - -Lemma add_branch_valid_freshstate: - forall s n, - Plt n (st_freshstate s) -> - valid_freshstate (PositiveMap.add n Vskip (st_stm s)) (st_freshstate s). -Proof. - unfold valid_freshstate; intros; destruct (peq n0 n). - - subst; auto. - - assert (H1 := st_wf s); destruct H1; - unfold valid_freshstate in H0; rewrite PositiveMap.gso; auto. -Qed. - -Lemma add_branch_instr_st_wf: - forall s e n n1 n2, - Plt n (st_freshstate s) -> - valid_freshstate (PositiveMap.add n Vskip (st_stm s)) (st_freshstate s) - /\ states_have_transitions (PositiveMap.add n Vskip (st_stm s)) - (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)). -Proof. - auto using add_branch_valid_freshstate, add_branch_instr_states_have_transitions. -Qed. - -Lemma add_branch_instr_state_incr: - forall s e n n1 n2 LT, - (st_stm s) ! n = None -> - (st_statetrans s) ! n = None -> - state_incr s (mkstate - (st_freshreg s) - (st_freshstate s) - (PositiveMap.add n Vskip (st_stm s)) - (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)) - (st_decl s) - (add_branch_instr_st_wf s e n n1 n2 LT)). -Proof. - intros. apply state_incr_intro; simpl; - try (intros; destruct (peq n0 n); subst); - auto with verilog_state. -Qed. - -Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := - fun s => - match plt n (st_freshstate s), check_empty_node_stm s n, check_empty_node_statetrans s n with - | left LT, left NSTM, left NTRANS => - OK tt (mkstate - (st_freshreg s) - (st_freshstate s) - (PositiveMap.add n Vskip (st_stm s)) - (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)) - (st_decl s) - (add_branch_instr_st_wf s e n n1 n2 LT)) - (add_branch_instr_state_incr s e n n1 n2 LT NSTM NTRANS) - | _, _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") - end. - -Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) - (args : list reg) (stack : reg) : mon expr := - match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *) - | Op.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) - then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) - else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) - then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4)))) - else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") - end. - -Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := - match ni with - (n, i) => - match i with - | Inop n' => add_instr n n' Vskip - | Iop op args dst n' => - do instr <- translate_instr op args; - add_instr_reg dst n n' (block dst instr) - | Iload mem addr args dst n' => - do src <- translate_arr_access mem addr args stack; - add_instr_reg dst n n' (block dst src) - | Istore mem addr args src n' => - do dst <- translate_arr_access mem addr args stack; - add_instr_reg src n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) - | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") - | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") - | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") - | Icond cond args n1 n2 => - do e <- translate_condition cond args; - add_branch_instr e n n1 n2 - | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented") - | Ireturn r => - match r with - | Some r' => - add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) - | None => - add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z))) - end - end - end. - -Definition make_stm_cases (s : positive * stmnt) : expr * stmnt := - match s with (a, b) => (posToExpr 32 a, b) end. - -Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt := - Vcase (Vvar r) (map make_stm_cases (PositiveMap.elements s)) (Some Vskip). - -Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt := - match st with - | (n, StateGoto n') => (posToExpr 32 n, state_goto r n') - | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2) - end. - -Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt := - Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip). - -Definition allocate_reg (e : reg * decl) : module_item := - match e with - | (r, (mkdecl n 0)) => Vdecl r n - | (r, (mkdecl n l)) => Vdeclarr r n l - end. - -Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item := - (Valways_ff (Vposedge clk) - (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1))) - (nonblock st (posToExpr 32 entry)) - (make_statetrans st s.(st_statetrans)))) - :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm))) - :: (map allocate_reg (PositiveMap.elements s.(st_decl))). - -(** To start out with, the assumption is made that there is only one - function/module in the original code. *) - -Definition set_int_size (r: reg) : reg * nat := (r, 32%nat). - -(*FIXME: This shouldn't be necessary; needs alterations in Verilog.v *) -Definition get_sz (rg : reg * decl) : szreg := match rg with (r, d) => (r, d.(width)) end. - -Definition transf_module (f: function) : mon module := - do fin <- decl_io (mkdecl 1 0); - do rtrn <- decl_io (mkdecl 32 0); - do stack <- decl_fresh_reg (mkdecl 32%nat (Z.to_nat (f.(fn_stacksize) / 4))); - do _ <- traverselist (transf_instr (fst fin) (fst rtrn) (fst stack)) (Maps.PTree.elements f.(fn_code)); - do start <- decl_io (mkdecl 1 0); - do rst <- decl_io (mkdecl 1 0); - do clk <- decl_io (mkdecl 1 0); - do st <- decl_fresh_reg (mkdecl 32 0); - do current_state <- get; - let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in - ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st) - (map set_int_size f.(fn_params)) mi). - -Lemma max_state_valid_freshstate: - forall f, - valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)). -Proof. unfold valid_freshstate; simpl; auto with verilog_state. Qed. -Hint Resolve max_state_valid_freshstate : verilog_state. - -Lemma max_state_st_wf: - forall f, - valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)) - /\ states_have_transitions (st_stm init_state) (st_statetrans init_state). -Proof. auto with verilog_state. Qed. - -Definition max_state (f: function) : state := - mkstate (Pos.succ (max_reg_function f)) - (Pos.succ (max_pc_function f)) - (st_stm init_state) - (st_statetrans init_state) - (st_decl init_state) - (max_state_st_wf f). - -Definition transl_module (f : function) : Errors.res module := - run_mon (max_state f) (transf_module f). - -(** Retrieve the main function from the RTL, this should probably be replaced by -retrieving a designated function instead. This could be passed on the -commandline and be assumed as a [Parameter] in this code. *) - -Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) -{struct flist} : option function := - match flist with - | (i, AST.Gfun (AST.Internal f)) :: xs => - if Pos.eqb i main - then Some f - else main_function main xs - | _ :: xs => main_function main xs - | nil => None - end. - -Definition transf_program (d : program) : Errors.res module := - match main_function d.(AST.prog_main) d.(AST.prog_defs) with - | Some f => run_mon (max_state f) (transf_module f) - | _ => Errors.Error (Errors.msg "Veriloggen: could not find main function") - end. +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)) + (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint))) + (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) + :: (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) + m.(mod_clk) + m.(mod_finish) + m.(mod_return) + m.(mod_st) + m.(mod_stk) + m.(mod_params) + body + m.(mod_entrypoint). + +Definition transl_fundef := transf_fundef transl_module. + +Definition transl_program (p: HTL.program) : Verilog.program := + transform_program transl_fundef p. diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 942a83a..6c58c56 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,30 +17,15 @@ *) From compcert Require Import Smallstep. -From compcert Require RTL. -From coqup Require Verilog. +From coqup Require HTL Verilog. Section CORRECTNESS. - Variable prog: RTL.program. - Variable tprog: Verilog.module. - - Inductive match_states: RTL.state -> Verilog.state -> Prop := - | match_state: - forall, - - match_states (RTL.State f s k sp e m) - (Verilog.State m mi mis assoc nbassoc f cycle pc) - | match_returnstate: - forall v tv k m tm cs - (MS: match_stacks k cs) - (LD: Val.lessdef v tv) - (MEXT: Mem.extends m tm), - match_states (CminorSel.Returnstate v k m) - (RTL.Returnstate cs tv tm). + Variable prog: HTL.program. + Variable tprog: Verilog.program. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (Verilog.semantics tprog). + forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). Admitted. End CORRECTNESS. diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v index 09d08ed..7dc632c 100644 --- a/src/translation/Veriloggenspec.v +++ b/src/translation/Veriloggenspec.v @@ -15,116 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see <https://www.gnu.org/licenses/>. *) - -From Coq Require Import FSets.FMapPositive. -From compcert Require RTL Op Maps. -From coqup Require Import Coquplib Verilog Veriloggen Value. - -(** * Relational specification of the translation *) - -(** We now define inductive predicates that characterise the fact that the -statemachine that is created by the translation contains the correct -translations for each of the elements *) - -Inductive tr_op : Op.operation -> list reg -> expr -> Prop := -| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r) -| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n)) -| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r)) -| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2) -| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2) -| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n) -| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2) -| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2) -| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2) -| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2) -| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2) -| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n) -| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2) -| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n) -| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2) -| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n) -| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r)) -| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2) -| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n) -| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2) -| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n) -| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e -| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e. - -Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := -| tr_instr_Inop : - forall n, - tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n) -| tr_instr_Iop : - forall n op args e dst, - tr_op op args e -> - tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) -| tr_instr_Icond : - forall n1 n2 cond args s s' i c, - translate_condition cond args s = OK c s' i -> - tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) -| tr_instr_Ireturn_None : - tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip -| tr_instr_Ireturn_Some : - forall r, - tr_instr fin rtrn st (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. - -Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt) - (fin rtrn st : reg) : Prop := -| tr_code_intro : - forall i s t n, - Maps.PTree.get n c = Some i -> - stmnts!n = Some s -> - trans!n = Some t -> - tr_instr fin rtrn st i s t -> - tr_code c stmnts trans fin rtrn st. - -(** [tr_module_items start clk st rst s mis] holds if the state is correctly -translated to actual Verilog, meaning it is correctly implemented as a state -machine in Verilog. Currently it does not seem that useful because it models -the [make_module_items] nearly exactly. Therefore it might have to be changed -to make up for that. *) - -Inductive tr_module_items : node -> reg -> reg -> reg -> state -> list module_item -> Prop := - tr_module_items_intro : - forall start clk st rst s mis, - Valways_ff (Vposedge clk) - (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1))) - (nonblock st (posToExpr 32 start)) - (make_statetrans st s.(st_statetrans))) - :: Valways_ff (Vposedge clk) (make_stm st s.(st_stm)) - :: List.map allocate_reg (PositiveMap.elements s.(st_decl)) = mis -> - tr_module_items start clk st rst s mis. - -(** [tr_module function module] Holds if the [module] is the correct translation -of the [function] that it was given. *) - -Inductive tr_module : RTL.function -> module -> Prop := - tr_module_intro : - forall f mi st rtrn fin clk rst start s0 s1 s2 s3 s4 s5 s6 i1 i2 i3 i4 i5 i6, - decl_io 1 s0 = OK fin s1 i1 -> - decl_io 32 s1 = OK rtrn s2 i2 -> - decl_io 1 s2 = OK start s3 i3 -> - decl_io 1 s3 = OK rst s4 i4 -> - decl_io 1 s4 = OK clk s5 i5 -> - decl_fresh_reg 32 s5 = OK st s6 i6 -> - tr_code f.(RTL.fn_code) s6.(st_stm) - (PositiveMap.map (statetrans_transl (fst st)) s6.(st_statetrans)) - (fst fin) (fst rtrn) (fst st) -> - tr_module_items f.(RTL.fn_entrypoint) (fst clk) (fst st) (fst rst) s6 mi -> - tr_module f (mkmodule - start - rst - clk - fin - rtrn - st - (List.map set_int_size f.(RTL.fn_params)) - mi). - -Lemma tr_module_correct: - forall f m, - transl_module f = Errors.OK m -> - tr_module f m. -Admitted. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 82aac41..c509248 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -48,7 +48,12 @@ Record module: Type := mod_stk : reg; mod_stk_len : nat; mod_finish : reg; - mod_return : reg + mod_return : reg; + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); + mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); }. Definition fundef := AST.fundef module. diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index bdd8581..700b8e3 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -21,6 +21,7 @@ open Value open Datatypes open Camlcoq +open AST open Printf @@ -107,21 +108,30 @@ let pprint_edge_top i = function | Valledge -> "@*" | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] -let declare i t = +let declare t = function (r, sz) -> - concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; ";\n" ] -let declarearr i t = +let declarearr t = function (r, sz, ln) -> - concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] +let print_io = function + | Some Vinput -> "input" + | Some Voutput -> "output reg" + | Some Vinout -> "inout" + | None -> "reg" + +let decl i = function + | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] + | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] + (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function - | Vdecl (r, sz) -> declare i "reg" (r, sz) - | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln) + | Vdeclaration d -> decl i d | Valways (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] | Valways_ff (e, s) -> @@ -138,10 +148,6 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"] let compose f g x = g x |> f -let init_inputs i r = declare i "input" r - -let init_outputs i r = declare i "output reg" r - let testbench = "module testbench; reg start, reset, clk; wire finish; @@ -171,17 +177,12 @@ endmodule let pprint_module i n m = let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in let outputs = [m.mod_finish; m.mod_return] in - concat [ indent i; "module "; n; - "("; concat (intersperse ", " (List.map (compose register fst) (inputs @ outputs))); ");\n"; - fold_map (init_inputs (i+1)) inputs; - fold_map (init_outputs (i+1)) outputs; + concat [ indent i; "module "; (extern_atom n); + "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; - indent i; "endmodule\n\n"; - testbench + indent i; "endmodule\n\n" ] -let print_program pp v = pstr pp (pprint_module 0 "main" v) - let print_result pp lst = let rec print_result_in pp = function | [] -> fprintf pp "]\n" @@ -192,3 +193,12 @@ let print_result pp lst = print_result_in pp lst let print_value pp v = fprintf pp "%s" (literal v) + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> pstr pp (pprint_module 0 id f) + | _ -> () + +let print_program pp prog = + List.iter (print_globdef pp) prog.prog_defs; + pstr pp testbench diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index c9fca8e..0df9d06 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,6 +18,6 @@ val print_value : out_channel -> Value.value -> unit -val print_program : out_channel -> Verilog.coq_module -> unit +val print_program : out_channel -> Verilog.program -> unit val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit diff --git a/src/verilog/Test.v b/src/verilog/Test.v deleted file mode 100644 index 90c5312..0000000 --- a/src/verilog/Test.v +++ /dev/null @@ -1,99 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -From coqup Require Import Verilog Veriloggen Coquplib Value. -From compcert Require Import AST Errors Maps Op Integers. -From compcert Require RTL. -From Coq Require Import FSets.FMapPositive. -From bbv Require Import Word. -Import ListNotations. -Import HexNotationValue. -Import WordScope. - -Local Open Scope word_scope. - -Definition test_module : module := - let mods := [ - Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5))) - (Vnonblock (Vvar 7%positive) - (Vvar 6%positive))) - ] in - mkmodule (1%positive, 1%nat) - (2%positive, 1%nat) - (3%positive, 1%nat) - (4%positive, 1%nat) - (5%positive, 32%nat) - (6%positive, 32%nat) - nil - mods. - -Definition test_input : RTL.function := - let sig := mksignature nil Tvoid cc_default in - let params := nil in - let stacksize := 0 in - let entrypoint := 3%positive in - let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive)) - (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive) - (PTree.empty RTL.instruction)) in - RTL.mkfunction sig params stacksize code entrypoint. - -Definition test_input_program : RTL.program := - mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive. - -Compute transf_program test_input_program. - -Definition test_output_module : module := - {| mod_start := (4%positive, 1%nat); - mod_reset := (5%positive, 1%nat); - mod_clk := (6%positive, 1%nat); - mod_finish := (2%positive, 1%nat); - mod_return := (3%positive, 32%nat); - mod_state := (7%positive, 32%nat); - mod_args := []; - mod_body := - [Valways_ff (Vposedge 6%positive) - (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1")) - (Vnonblock (Vvar 7%positive) (32'h"3")) - (Vcase (Vvar 7%positive) - [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1")); - (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))] - (Some Vskip))); - Valways_ff (Vposedge 6%positive) - (Vcase (Vvar 7%positive) - [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1"))) - (Vblock (Vvar 3%positive) (Vvar 1%positive))); - (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))] - (Some Vskip)); - Vdecl 1%positive 32; Vdecl 7%positive 32] |}. - -Lemma valid_test_output : - transf_program test_input_program = OK test_output_module. -Proof. trivial. Qed. - -Definition test_fextclk := initial_fextclk test_output_module. - -Lemma manual_simulation : - step (State test_output_module empty_assocmap empty_assocmap - test_fextclk 1 (32'h"1")) - (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap) - empty_assocmap test_fextclk 2 (32'h"3")). -Proof. - repeat (econstructor; eauto); - try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); - apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat. -Qed. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 0e999de..8b83d49 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -87,6 +87,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). +Inductive scl_decl : Type := Scalar (sz : nat). +Inductive arr_decl : Type := Array (sz : nat) (ln : nat). (** * Verilog AST @@ -181,9 +183,17 @@ Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). The declarations are always register declarations as combinational logic can be done using combinational always block instead of continuous assignments. *) +Inductive io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. + +Inductive declaration : Type := +| Vdecl : option io -> reg -> nat -> declaration +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. + Inductive module_item : Type := -| Vdecl : reg -> nat -> module_item -| Vdeclarr : reg -> nat -> nat -> module_item +| Vdeclaration : declaration -> module_item | Valways : edge -> stmnt -> module_item | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. @@ -200,15 +210,22 @@ Inductive module_item : Type := *) Record module : Type := mkmodule { - mod_start : szreg; - mod_reset : szreg; - mod_clk : szreg; - mod_finish : szreg; - mod_return : szreg; - mod_state : szreg; (**r Variable that defines the current state, it should be internal. *) - mod_args : list szreg; + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_st : reg; (**r Variable that defines the current state, it should be internal. *) + mod_stk : reg; + mod_args : list reg; mod_body : list module_item; - }. + mod_entrypoint : node; +}. + +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := @@ -241,18 +258,28 @@ retrieved and set appropriately. which determines which part of the Verilog is executed. This is then the part of the Verilog that should match with the RTL. *) +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (assoc : assocmap), + stackframe. + Inductive state : Type := -| State: - forall (m : module) - (assoc : reg_associations) - (assoc : arr_associations) - (f : fextclk) - (cycle : nat) - (stvar : value), - state -| Finishstate: - forall v : value, - state. +| State : + forall (stack : list stackframe) + (m : module) + (st : node) + (reg_assoc : assocmap) + (arr_assoc : AssocMap.t (list value)), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := match op with @@ -383,14 +410,14 @@ Definition access_fext (f : fext) (r : reg) : res value := (** Return the location of the lhs of an assignment. *) Inductive location : Type := -| Reg (_ : reg) -| Array (_ : reg) (_ : nat). +| LocReg (_ : reg) +| LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := -| Base : forall f asr asa r, location_is f asr asa (Vvar r) (Reg r) +| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) | Indexed : forall f asr asa r iexp iv, expr_runp f asr asa iexp iv -> - location_is f asr asa (Vvari r iexp) (Array r (valueToNat iv)). + location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). (* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) (* match e with *) @@ -508,28 +535,28 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 | stmnt_runp_Vblock_reg: forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) (block_reg r asr rhsval) asa | stmnt_runp_Vnonblock_reg: forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) (nonblock_reg r asr rhsval) asa | stmnt_runp_Vblock_arr: forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) asr (block_arr r i asa rhsval) | stmnt_runp_Vnonblock_arr: forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) @@ -565,8 +592,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, - mi_stepp f sr sa (Vdecl lhs rhs) sr sa. + forall f sr sa lhs rhs io, + mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa. Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> @@ -607,8 +634,8 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) - | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) + | S O => (AssocMap.set (mod_reset m) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap) end. (*Definition module_run (n : nat) (m : module) : res assocmap := @@ -655,42 +682,60 @@ Qed. *) -Definition genv := Genv.t unit unit. - -Inductive step : state -> state -> Prop := -| step_module : - forall m stvar stvar' cycle f - asr0 asa0 asr1 asa1 - asr' asa', - mis_stepp (f cycle) asr0 asa0 - m.(mod_body) asr1 asa1 -> - asr' = merge_associations asr1 -> - asa' = merge_associations asa1 -> - Some stvar' = asr'.(assoc_blocking)!(fst m.(mod_state)) -> - step (State m asr0 asa0 f cycle stvar) - (State m asr' asa' f (S cycle) stvar') +Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') + | _, _ => empty_assocmap + end. + +Definition genv := Globalenvs.Genv.t fundef unit. + +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, + mis_stepp f (mkassociations asr empty_assocmap) + (mkassociations asa (AssocMap.empty (list value))) + m.(mod_body) + (mkassociations basr1 nasr1) + (mkassociations basa1 nasa1)-> + asr' = merge_assocmap nasr1 basr1 -> + asa' = AssocMapExt.merge (list value) nasa1 basa1 -> + asr'!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : - forall m asr asa f cycle stvar result, - asr.(assoc_blocking)!(fst m.(mod_finish)) = Some (1'h"1") -> - asr.(assoc_blocking)!(fst m.(mod_return)) = Some result -> - step (State m asr asa f cycle stvar) - (Finishstate result). + forall asr asa sf retval m st g, + asr!(m.(mod_finish)) = Some (1'h"1") -> + asr!(m.(mod_return)) = Some retval -> + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g res m args, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint)) + (init_params args m.(mod_args))) + (AssocMap.empty (list value))) +| step_return : + forall g m asr i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) + (AssocMap.empty (list value))). Hint Constructors step : verilog. -(*Inductive initial_state (m: module): state -> Prop := -| initial_state_intro: - forall hmi tmi, - hmi::tmi = mod_body m -> - initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH). - -(** A final state is a [Returnstate] with an empty call stack. *) - -Inductive final_state: state -> Integers.int -> Prop := - | final_state_intro: forall v, - final_state (Finishstate v) (valueToInt v). - -(** The small-step semantics for a module. *) - -Definition semantics (p: module) := - Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil). -*) +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + initial_state p (Callstate nil m nil). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + retvali = valueToInt retval -> + final_state (Returnstate nil retval) retvali. + +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). |