From b22dfebd3a1638c431e9ab32fac391aa95f846eb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 1 Apr 2020 19:24:35 +0100 Subject: Complete translation from simple RTL to Verilog --- src/translation/Veriloggen.v | 263 ++++++++++++++++++++++++++----------------- 1 file changed, 162 insertions(+), 101 deletions(-) (limited to 'src') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 605448b..c2614ec 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -20,7 +20,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Verilog Coquplib. -From compcert Require Errors Op AST Integers. +From compcert Require Errors Op AST Integers Maps. From compcert Require Import RTL. Definition node : Type := positive. @@ -28,90 +28,95 @@ Definition reg : Type := positive. Definition ident : Type := positive. Inductive statetrans : Type := - | StateGoto (p : node) - | StateCond (c : expr) (t f : node). +| StateGoto (p : node) +| StateCond (c : expr) (t f : node). Record state: Type := mkstate { - st_variables: PositiveMap.t (nat * expr); + st_freshreg : reg; + st_freshstate : node; st_stm : PositiveMap.t stmnt; st_statetrans : PositiveMap.t statetrans; + st_decl : list (reg * nat); + st_fin : option reg; + st_ret : option reg; }. +(** Map from initial register allocations to new allocations. *) +Definition mapping: Type := PositiveMap.t reg. + Definition init_state : state := - mkstate (PositiveMap.empty (nat * expr)) (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). + mkstate 1%positive + 1%positive + (PositiveMap.empty stmnt) + (PositiveMap.empty statetrans) + nil + None + None. -Inductive res (A: Type) (S: Type): Type := - | Error: Errors.errmsg -> res A S - | OK: A -> S -> res A S. +Inductive res (A: Type) (s: state): Type := +| Error : Errors.errmsg -> res A s +| OK : A -> forall (_ : state), res A s. -Arguments OK [A S]. -Arguments Error [A S]. +Arguments OK [A s]. +Arguments Error [A s]. -Definition mon (A: Type) : Type := res A state. +Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s. +Definition ret {A: Type} (x: A) : mon A := + fun (s : state) => OK x s. Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := - match f with + fun (s : state) => + match f s with | Error msg => Error msg - | OK a s => g a + | OK a s' => + match g a s' with + | Error msg => Error msg + | OK b s'' => OK b s'' + 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)). -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 - 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). +(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 := - match f with - | OK a s' => OK a s' - | Error _ => g - end. - -Module PTree. - Export Maps.PTree. - - Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B) - (m : t A) (s : state) (i : positive) - {struct m} : mon (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 + fun (s : state) => + match f s with + | OK a s' => OK a s' + | Error _ => g s end. - Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m := - xtraverse f m init_state xH. +Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: state) => Error err. + +Definition get : mon state := fun s => OK s s. + +Definition set (s: state) : mon unit := fun _ => OK tt s. - Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f). +Definition run_mon {A: Type} (s: state) (m: mon A): Errors.res A := + match m s with + | OK a s' => Errors.OK a + | Error err => Errors.Error err + end. + +Definition map_state (f: state -> state): mon state := + fun s => let s' := f s in OK s' s'. -End PTree. +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) + 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) : option expr := Some (Vbinop op (Vvar r1) (Vvar r2)). @@ -176,37 +181,77 @@ Definition translate_instr (op : Op.operation) (args : list reg) : option expr : | _, _ => None end. -Definition add_instr (n : node) (n' : node) (s : state) (st : stmnt) : mon node := - OK n' (mkstate s.(st_variables) - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans))). - -Definition option_err {A : Type} (str : string) (v : option A) (s : state) : mon A := - match v with - | Some v' => OK v' s - | _ => Error (Errors.msg str) - end. - -Definition transf_instr (n : node) (i : instruction) (s : state) : mon node := - match i with - | Inop n' => - add_instr n n' s Vskip - | Iop op args dst n' => - match translate_instr op args with - | Some instr => add_instr n n' s (nonblock dst instr) - | _ => Error (Errors.msg "Instruction is not implemented.") - end - | 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 => Error (Errors.msg "Condition not implemented.") - | Ijumptable _ _ => Error (Errors.msg "Jumptable not implemented.") - | Ireturn r => - match r with - | Some x => OK n s - | None => OK n s +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon node := + fun s => + OK n' (mkstate s.(st_freshreg) + (Pos.max (Pos.succ n) s.(st_freshstate)) + (PositiveMap.add n st s.(st_stm)) + (PositiveMap.add n (StateGoto n') s.(st_statetrans)) + s.(st_decl) + s.(st_fin) + s.(st_ret)). + +Definition add_reg (r: reg) (s: state) : state := + mkstate (Pos.max (Pos.succ r) s.(st_freshreg)) + s.(st_freshstate) + s.(st_stm) + s.(st_statetrans) + ((r, 32%nat) :: s.(st_decl)) + s.(st_fin) + s.(st_ret). + +Definition add_instr_reg (r: reg) (n: node) (n': node) (st: stmnt) : mon node := + do _ <- map_state (add_reg r); + add_instr n n' st. + +Definition decl_fresh_reg (sz : nat) : mon reg := + fun s => + let r := s.(st_freshreg) in + OK r (mkstate + (Pos.succ r) + s.(st_freshstate) + s.(st_stm) + s.(st_statetrans) + ((r, sz) :: s.(st_decl)) + s.(st_fin) + s.(st_ret)). + +Definition add_fin_ret (f r: reg) : mon unit := + fun s => OK tt (mkstate + s.(st_freshreg) + s.(st_freshstate) + s.(st_stm) + s.(st_statetrans) + s.(st_decl) + (Some f) (Some r)). + +Definition transf_instr (ni: node * instruction) : mon node := + match ni with + (n, i) => + match i with + | Inop n' => add_instr n n' Vskip + | Iop op args dst n' => + match translate_instr op args with + | Some instr => add_instr_reg dst n n' (block dst instr) + | _ => error (Errors.msg "Instruction is not implemented.") + end + | 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 => error (Errors.msg "Condition not implemented.") + | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented.") + | Ireturn r => + do fin <- decl_fresh_reg 1%nat; + do rtrn <- decl_fresh_reg 32%nat; + do _ <- add_fin_ret fin rtrn; + match r with + | Some r' => + add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: block rtrn (Vvar r') :: nil)) + | None => + add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: nil)) + end end end. @@ -225,23 +270,39 @@ Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt := Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)). -Definition make_globals (globals : PositiveMap.t (nat * expr)) : verilog := nil. +Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item := + match e with + | (r, n)::es => Vdecl r n (Vlit (ZToValue n 0%Z)) :: allocate_regs es + | nil => nil + end. -Definition make_verilog (s : state) : verilog := - let r := 500%positive in - (make_statetrans r s.(st_statetrans)) :: (make_stm r s.(st_stm)) - :: (make_globals s.(st_variables)). +Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item := + (Valways (Voredge (Vposedge clk) (Vposedge rst)) + (Vcond (Vbinop Veq (Vvar rst) (Vlit (ZToValue 1%nat 1%Z))) + (nonblock st (posToExpr entry)) + (make_statetrans st s.(st_statetrans)))) + :: (Valways Valledge (make_stm st s.(st_stm))) + :: (allocate_regs s.(st_decl)). (** To start out with, the assumption is made that there is only one function/module in the original code. *) -Definition transf_module (m: function) : Errors.res verilog := - match PTree.traverse transf_instr m.(fn_code) with - | OK _ s => Errors.OK (make_verilog s) - | Error err => Errors.Error err + +Definition transf_module (f: function) : mon module := + do _ <- traverselist transf_instr (Maps.PTree.elements f.(fn_code)); + do start <- decl_fresh_reg 1%nat; + do rst <- decl_fresh_reg 1%nat; + do clk <- decl_fresh_reg 1%nat; + do st <- decl_fresh_reg 32%nat; + do current_state <- get; + let mi := make_module_items f.(fn_entrypoint) clk st rst current_state in + match current_state.(st_fin), current_state.(st_ret) with + | Some fin, Some rtrn => + ret (mkmodule start rst clk fin rtrn f.(fn_params) mi) + | _, _ => error (Errors.msg "Veriloggen: finish and return signals not generated") end. Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) - {struct flist} : option function := +{struct flist} : option function := match flist with | (i, AST.Gfun (AST.Internal f)) :: xs => if Pos.eqb i main @@ -251,8 +312,8 @@ Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef | nil => None end. -Definition transf_program (d : program) : Errors.res verilog := +Definition transf_program (d : program) : Errors.res module := match main_function d.(AST.prog_main) d.(AST.prog_defs) with - | Some m => transf_module m - | _ => Errors.Error (Errors.msg "Could not find main module") + | Some f => run_mon init_state (transf_module f) + | _ => Errors.Error (Errors.msg "Veriloggen: could not find main module") end. -- cgit