diff options
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 487 |
1 files changed, 345 insertions, 142 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index d7f88c1..4564237 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -16,171 +16,374 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Import HTL Coquplib. - From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST RTL. +From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. + +Hint Resolve AssocMap.gempty : htlh. +Hint Resolve AssocMap.gso : htlh. +Hint Resolve AssocMap.gss : htlh. +Hint Resolve Ple_refl : htlh. +Hint Resolve Ple_succ : htlh. Record state: Type := mkstate { - st_nextinst: positive; - st_instances: instances; + st_st : reg; + st_freshreg: reg; + st_freshstate: node; + st_datapath: datapath; + st_controllogic: controllogic; }. -Inductive res (A: Type) (S: Type): Type := - | Error: Errors.errmsg -> res A S - | OK: A -> S -> res A S. +Definition init_state (st : reg) : state := + mkstate st + 1%positive + 1%positive + (AssocMap.empty stmnt) + (AssocMap.empty stmnt). + +Module HTLState <: State. + + Definition st := state. + + Inductive st_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (forall n, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2. + Hint Constructors st_incr : htlh. + + Definition st_prop := st_incr. + Hint Unfold st_prop : htlh. + + Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + + Lemma st_trans : + forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans. + - rewrite H1. rewrite H. reflexivity. + - intros. destruct H4 with n. + + left; assumption. + + destruct H8 with n; + [ rewrite <- H0; left; assumption + | right; rewrite <- H0; apply H10 + ]. + - intros. destruct H5 with n. + + left; assumption. + + destruct H9 with n. + * rewrite <- H0. left. assumption. + * right. rewrite <- H0. apply H10. + Qed. + +End HTLState. +Export HTLState. -Arguments OK [A S]. -Arguments Error [A S]. +Module HTLMonad := Statemonad(HTLState). +Export HTLMonad. -Definition mon (A: Type) : Type := res A state. +Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). +Import HTLMonadExtra. +Export MonadNotation. -Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s. +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue 32 n)). -Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := - match f with - | Error msg => Error msg - | OK a s => g a +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + +Definition check_empty_node_datapath: + forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. +Proof. + intros. case (s.(st_datapath)!n); intros. right; auto. left; auto. +Defined. + +Definition check_empty_node_controllogic: + forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. +Proof. + intros. case (s.(st_controllogic)!n); intros. right; auto. left; auto. +Defined. + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +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 + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") 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)). +Lemma add_instr_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + 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 bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B := - match f with - | Error msg => Error msg - | OK a s => g a s +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue 32%nat 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") end. -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" := (bindS A (fun X Y => B)) - (at level 200, X ident, Y ident, A at level 100, B at level 200). +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 handle_error {A: Type} (f g: mon A) : mon A := - match f with - | OK a s' => OK a s' - | Error _ => g +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 init_state : state := - mkstate 1%positive empty_instances. - -Module PTree. - Export Maps.PTree. - - Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B) - (m : PTree.t A) (s : state) (i : positive) - {struct m} : mon (PTree.t B) := - match m with - | Leaf => OK Leaf s - | Node l o r => - let newo := - match o with - | None => OK None s - | Some x => - match f (prev i) x s with - | Error err => Error err - | OK val s' => OK (Some val) s' - end - end in - match newo with - | OK no s => - do (nl, s') <- xtraverse f l s (xO i); - do (nr, s'') <- xtraverse f r s' (xI i); - OK (Node nl no nr) s'' - | Error msg => Error msg - 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 Vadd r1 scale) (Vlit (ZToValue 32%nat offset))) + | Op.Aindexed2scaled scale offset, r1::r2::nil => + ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + | _, _ => 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 + | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other") + end. + +Lemma add_branch_instr_state_incr: + forall s e n n1 n2, + (st_datapath s) ! n = None -> + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). +Proof. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. + +Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left NSTM, left NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) + | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") end. - Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m := - xtraverse f m init_state xH. - - Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f). - -End PTree. - -Definition transf_instr (pc: node) (rtl: RTL.instruction) (s: state) - : mon HTL.instruction := - match rtl with - | RTL.Inop n => - (** Nop instruction should just become a Skip in Verilog, which is just a - semicolon. *) - ret (HTL.Hnop n) s - | RTL.Iop op args res n => - (** Perform an arithmetic operation over registers. This will just become - one binary operation in Verilog. This will contain a list of registers, - so these will just become a chain of binary operations in Verilog. *) - ret (HTL.Hnonblock op args res n) s - | RTL.Iload chunk addr args dst n => - (** Load from memory, which will maybe become a load from RAM, however, I'm - not sure yet how memory will be implemented or how it will formalised - be. *) - ret (HTL.Hload chunk addr args dst n) s - | RTL.Istore chunk addr args src n => - (** How memory will be laid out will also affect how stores are handled. For - now hopefully these can be ignored, and hopefull they are not used that - often when they are not required in C. *) - ret (HTL.Hstore chunk addr args src n) s - | RTL.Icall sig ros args res n => - (** Function call should become a module instantiation with start and end - signals appropriately wired up. *) - match ros with - | inr i => - let inst := mkinst i args in - let newinstances := PTree.set s.(st_nextinst) inst s.(st_instances) in - ret (HTL.Hinst sig i res n) - (mkstate ((s.(st_nextinst) + 1)%positive) - newinstances) - | _ => Error (Errors.msg "Function pointers are not supported.") - end - | RTL.Itailcall sig ros args => - (** Should be converted into a reset of the modules state, setting the - initial variables correctly. This would simulate a tailcall as it is - similar to jumping back to the top of the function in assembly. *) - match ros with - | inr i => ret (HTL.Htailcall sig i args) s - | _ => Error (Errors.msg "Function pointers are not supported.") +Definition transf_instr (fin rtrn: 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 n n' (nonblock dst instr) + | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.") + | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.") + | 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_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) + | None => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) + end end - | RTL.Ibuiltin ef args res n => - (** Builtin functions will have to supported manually, by implementing the - Verilog myself. *) - Error (Errors.msg "builtin functions are not supported.") - | RTL.Icond cond args n1 n2 => - (** Will be converted into two separate processes that are combined by a mux - at the end, with a start flag that propagates in the construct that should - be chosen. *) - ret (HTL.Hcond cond args n1 n2) s - | RTL.Ijumptable arg tbl => - (** A jump to a specific instruction in the list, this will require setting - the state in the state machine appropriately. This is trivial to - implement if no scheduling is involved, but as soon as that isn't the - case it might be difficult to find that location. It would help to - transform the CFG to a few basic blocks first which cannot have any - branching. *) - ret (HTL.Hjumptable arg tbl) s - | RTL.Ireturn r => - (** The return value of the function, which will just mean that the finished - signal goes high and the result is stored in the result register. *) - ret (HTL.Hfinish r) s end. -Definition transf_function (f: function) : Errors.res module := - match (PTree.traverse transf_instr f.(fn_code)) with - | OK code s => - Errors.OK (mkmodule - f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - code - s.(st_instances) - f.(fn_entrypoint)) - | Error err => Errors.Error err - end. +Lemma create_reg_state_incr: + forall s, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg: mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s). + +Definition transf_module (f: function) : mon module := + do fin <- create_reg; + do rtrn <- create_reg; + do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code)); + do start <- create_reg; + do rst <- create_reg; + do clk <- create_reg; + do current_state <- get; + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + fin + rtrn). -Definition transf_fundef (fd: fundef) : Errors.res moddecl := - transf_partial_fundef transf_function fd. +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_datapath (init_state st)) + (st_controllogic (init_state st)). -Definition transf_program (p: program) : Errors.res design := - transform_partial_program transf_fundef p. +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +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 => transl_module f + | _ => Errors.Error (Errors.msg "HTL: could not find main function") + end. |