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 +++---------------------------------------- src/verilog/Verilog.v | 183 +++++++----- 2 files changed, 154 insertions(+), 713 deletions(-) (limited to 'src') 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. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 845d706..b4b2f00 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). -- cgit