From 3d3f165bc97774c8d6b9bcbea9e06daf688e617d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:36:18 +0100 Subject: Generate Verilog from HTL --- src/translation/Veriloggen.v | 684 +++---------------------------------------- 1 file changed, 40 insertions(+), 644 deletions(-) (limited to 'src/translation') 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 . *) -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. -- cgit From 13b880f99b7355010551ad1b93242cf7773aa202 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:37:42 +0100 Subject: Declare all registers properly in HTL --- src/translation/HTLgen.v | 106 +++++++++++++++++++++++++++++------------- src/translation/HTLgenproof.v | 6 ++- src/translation/HTLgenspec.v | 34 +++++++------- 3 files changed, 95 insertions(+), 51 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index b573b06..15100bf 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 s r sz, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (None, Scalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Proof. auto with htlh. Qed. + +Definition declare_reg (r : reg) (sz : nat) : mon unit := + fun s => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (None, Scalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr 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,6 +359,7 @@ 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 dst 32; add_instr n n' (nonblock dst instr) | Iload mem addr args dst n' => do src <- translate_arr_access mem addr args stack; @@ -363,61 +385,61 @@ 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 := +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon reg := fun s => let r := s.(st_freshreg) in OK r (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 <- 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 <- 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 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) @@ -427,14 +449,19 @@ Definition transf_module (f: function) : mon module := current_state.(st_st) stack 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)). @@ -442,15 +469,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 523c86c..4b7f268 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -540,6 +540,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 -> @@ -556,10 +557,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 4bf3843..8bb90c6 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,41 +184,41 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk m, + forall data control fin rtrn st stk 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) -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk fin rtrn) -> + st stk 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 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. @@ -239,11 +239,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 @@ -329,11 +329,11 @@ 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. -- cgit From 7ad63f341fe3c28ef20bfde755bdf21403077504 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:38:14 +0100 Subject: Remove Verilog proofs --- src/translation/Veriloggenproof.v | 23 ++------ src/translation/Veriloggenspec.v | 113 -------------------------------------- 2 files changed, 4 insertions(+), 132 deletions(-) (limited to 'src/translation') 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 . *) - -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. -- cgit From 0f9ab38389000edfa2376fabace69d2366d32647 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 13:18:40 +0100 Subject: Fix declaring function arguments correctly --- src/translation/HTLgen.v | 13 +++++----- src/translation/HTLgenspec.v | 62 +++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 66 insertions(+), 9 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 15100bf..bbce47c 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -125,28 +125,28 @@ Proof. Qed. Lemma declare_reg_state_incr : - forall s r sz, + forall i s r sz, st_incr s (mkstate s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (None, Scalar sz) s.(st_scldecls)) + (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 (r : reg) (sz : nat) : mon unit := +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 (None, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)) - (declare_reg_state_incr s r sz). + (declare_reg_state_incr i s r sz). Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := fun s => @@ -359,7 +359,7 @@ 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 dst 32; + 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; @@ -437,6 +437,7 @@ Definition transf_module (f: function) : mon module := do rtrn <- create_reg (Some Voutput) 32; do stack <- 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 _ <- 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; diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 8bb90c6..770b372 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -209,6 +209,20 @@ Lemma create_reg_controllogic_trans : 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 iop, create_arr iop sz ln s = OK x s' i -> @@ -255,6 +269,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' |- _ ] => @@ -395,9 +447,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. -- cgit From 86f42b92d87020875e2a7ef4ba40de12d261685f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 14:40:15 +0100 Subject: Add declaration of loads --- src/translation/HTLgen.v | 1 + src/translation/HTLgenspec.v | 9 +++++---- 2 files changed, 6 insertions(+), 4 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index bbce47c..a891d6c 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -363,6 +363,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni 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; diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 770b372..7909688 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -387,10 +387,11 @@ Proof. 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. -- cgit