diff options
-rw-r--r-- | src/translation/Veriloggen.v | 97 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.ml | 8 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 4 |
3 files changed, 82 insertions, 27 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f127b11..4a6f23e 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -61,12 +61,17 @@ Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t /\ (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 nat; + st_decl: PositiveMap.t decl; st_wf: valid_freshstate st_stm st_freshstate /\ states_have_transitions st_stm st_statetrans; }. @@ -94,7 +99,7 @@ Definition init_state : state := 1%positive (PositiveMap.empty stmnt) (PositiveMap.empty statetrans) - (PositiveMap.empty nat) + (PositiveMap.empty decl) init_state_wf. Inductive state_incr: state -> state -> Prop := @@ -204,7 +209,7 @@ 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%nat l)). + Vbinop op (Vvar r) (Vlit (ZToValue 32 l)). Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -245,9 +250,14 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | 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))) + 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. @@ -284,6 +294,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | 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. @@ -380,7 +392,7 @@ Definition add_reg (r: reg) (s: state) : state := (st_freshstate s) (st_stm s) (st_statetrans s) - (PositiveMap.add r 32%nat (st_decl s)) + (PositiveMap.add r (mkdecl 32 0) (st_decl s)) (st_wf s). Lemma add_reg_state_incr: @@ -417,9 +429,9 @@ 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 (sz: nat): mon (reg * nat) := +Definition decl_io (d: decl) : mon (reg * decl) := fun s => let r := s.(st_freshreg) in - OK (r, sz) (mkstate + OK (r, d) (mkstate (Pos.succ r) (st_freshstate s) (st_stm s) @@ -431,22 +443,22 @@ Definition decl_io (sz: nat): mon (reg * nat) := (** Declare a new register which is given, by changing [st_decl] and without affecting anything else. *) -Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) := - fun s => OK (r, sz) (mkstate +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 sz s.(st_decl)) + (PositiveMap.add r d s.(st_decl)) (st_wf s)) - (change_decl_state_incr s (PositiveMap.add r sz s.(st_decl))). + (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 (sz : nat) : mon (reg * nat) := - do (r, s) <- decl_io sz; - declare_reg r s. +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, @@ -512,7 +524,26 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := | _, _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") end. -Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := +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 @@ -520,8 +551,12 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := | Iop op args dst n' => do instr <- translate_instr op args; add_instr_reg dst n n' (block dst instr) - | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.") - | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.") + | 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.") @@ -554,8 +589,11 @@ 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)) (Some Vskip). -Definition allocate_reg (e : reg * nat) : module_item := - match e with (r, n) => Vdecl r n end. +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) @@ -570,17 +608,22 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m 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 1; - do rtrn <- decl_io 32; - do _ <- traverselist (transf_instr (fst fin) (fst rtrn)) (Maps.PTree.elements f.(fn_code)); - do start <- decl_io 1; - do rst <- decl_io 1; - do clk <- decl_io 1; - do st <- decl_fresh_reg 32; + 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 start rst clk fin rtrn st (map set_int_size f.(fn_params)) mi). + 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, diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 29c4f5a..bdd8581 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -70,6 +70,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s + | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"] @@ -111,9 +112,16 @@ let declare i t = concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; ";\n" ] +let declarearr i t = + function (r, sz, ln) -> + concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + register r; + " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] + (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function | Vdecl (r, sz) -> declare i "reg" (r, sz) + | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln) | Valways (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] | Valways_ff (e, s) -> diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index ce7ddd9..e2b85b2 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -97,6 +97,7 @@ Inductive unop : Type := Inductive expr : Type := | Vlit : value -> expr | Vvar : reg -> expr +| Vvari : reg -> expr -> expr | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr @@ -138,6 +139,7 @@ done using combinational always block instead of continuous assignments. *) Inductive module_item : Type := | Vdecl : reg -> nat -> module_item +| Vdeclarr : reg -> nat -> nat -> module_item | Valways : edge -> stmnt -> module_item | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. @@ -314,6 +316,7 @@ Definition access_fext (f : fext) (r : reg) : res value := | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r | _ => Error (msg "Verilog: Wrong state") end + | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") | Vinputvar r => access_fext s r | Vbinop op l r => let lv := expr_run s l in @@ -476,6 +479,7 @@ Hint Constructors stmnt_runp : verilog. | (Valways_ff _ st)::ls => run st ls | (Valways_comb _ st)::ls => run st ls | (Vdecl _ _)::ls => mi_step s ls + | (Vdeclarr _ _ _)::ls => mi_step s ls | nil => OK s end.*) |