aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/translation/Veriloggen.v97
-rw-r--r--src/verilog/PrintVerilog.ml8
-rw-r--r--src/verilog/Verilog.v4
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.*)
generated by cgit (git 2.34.1) at 2024-07-05 20:45:08 +0000