aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/translation/HTLgen.v127
-rw-r--r--src/translation/HTLgenspec.v79
-rw-r--r--src/translation/Veriloggen.v97
-rw-r--r--src/verilog/HTL.v40
-rw-r--r--src/verilog/PrintVerilog.ml8
-rw-r--r--src/verilog/Verilog.v300
6 files changed, 446 insertions, 205 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 78b1864..b573b06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -27,10 +27,15 @@ Hint Resolve AssocMap.gss : htlh.
Hint Resolve Ple_refl : htlh.
Hint Resolve Ple_succ : htlh.
+Inductive scl_decl : Type := Scalar (sz : nat).
+Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+
Record state: Type := mkstate {
st_st : reg;
st_freshreg: reg;
st_freshstate: node;
+ st_scldecls: AssocMap.t scl_decl;
+ st_arrdecls: AssocMap.t arr_decl;
st_datapath: datapath;
st_controllogic: controllogic;
}.
@@ -39,6 +44,8 @@ Definition init_state (st : reg) : state :=
mkstate st
1%positive
1%positive
+ (AssocMap.empty scl_decl)
+ (AssocMap.empty arr_decl)
(AssocMap.empty stmnt)
(AssocMap.empty stmnt).
@@ -68,19 +75,9 @@ Module HTLState <: State.
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.
+ intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
+ - destruct H4 with n; destruct H8 with n; intuition congruence.
+ - destruct H5 with n; destruct H9 with n; intuition congruence.
Qed.
End HTLState.
@@ -102,13 +99,13 @@ Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
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.
+ intros. case (s.(st_datapath)!n); tauto.
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.
+ intros. case (s.(st_controllogic)!n); tauto.
Defined.
Lemma add_instr_state_incr :
@@ -120,6 +117,8 @@ Lemma add_instr_state_incr :
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
Proof.
@@ -136,6 +135,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(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)
@@ -151,6 +152,8 @@ Lemma add_instr_skip_state_incr :
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n Vskip s.(st_controllogic))).
Proof.
@@ -167,6 +170,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n Vskip s.(st_controllogic)))
(add_instr_skip_state_incr s n st STM TRANS)
@@ -224,9 +229,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.
@@ -263,6 +273,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::nil => 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.
@@ -274,6 +286,8 @@ Lemma add_branch_instr_state_incr:
s.(st_st)
(st_freshreg s)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(AssocMap.set n Vskip (st_datapath s))
(AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
Proof.
@@ -290,13 +304,34 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
s.(st_st)
(st_freshreg s)
(st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
(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 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
@@ -304,8 +339,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 n n' (nonblock 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 n n' (block dst src)
+ | Istore mem addr args src n' =>
+ do dst <- translate_arr_access mem addr args stack;
+ add_instr 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.")
@@ -324,32 +363,61 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
end.
Lemma create_reg_state_incr:
- forall s,
+ forall s sz,
+ st_incr s (mkstate
+ s.(st_st)
+ (Pos.succ (st_freshreg s))
+ (st_freshstate s)
+ (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls))
+ s.(st_arrdecls)
+ (st_datapath s)
+ (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (sz : nat) : mon reg :=
+ fun s => let r := s.(st_freshreg) in
+ OK r (mkstate
+ s.(st_st)
+ (Pos.succ r)
+ (st_freshstate s)
+ (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls))
+ (st_arrdecls s)
+ (st_datapath s)
+ (st_controllogic s))
+ (create_reg_state_incr s sz).
+
+Lemma create_arr_state_incr:
+ forall s sz ln,
st_incr s (mkstate
s.(st_st)
(Pos.succ (st_freshreg s))
(st_freshstate s)
+ s.(st_scldecls)
+ (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls))
(st_datapath s)
(st_controllogic s)).
Proof. constructor; simpl; auto with htlh. Qed.
-Definition create_reg: mon reg :=
+Definition create_arr (sz : nat) (ln : nat) : mon reg :=
fun s => let r := s.(st_freshreg) in
OK r (mkstate
s.(st_st)
(Pos.succ r)
(st_freshstate s)
+ s.(st_scldecls)
+ (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls))
(st_datapath s)
(st_controllogic s))
- (create_reg_state_incr s).
+ (create_arr_state_incr s sz ln).
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 fin <- create_reg 1;
+ do rtrn <- create_reg 32;
+ do stack <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
+ do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+ do start <- create_reg 1;
+ do rst <- create_reg 1;
+ do clk <- create_reg 1;
do current_state <- get;
ret (mkmodule
f.(RTL.fn_params)
@@ -357,6 +425,7 @@ Definition transf_module (f: function) : mon module :=
current_state.(st_controllogic)
f.(fn_entrypoint)
current_state.(st_st)
+ stack
fin
rtrn).
@@ -365,6 +434,8 @@ Definition max_state (f: function) : state :=
mkstate st
(Pos.succ st)
(Pos.succ (max_pc_function f))
+ (st_scldecls (init_state st))
+ (st_arrdecls (init_state st))
(st_datapath (init_state st))
(st_controllogic (init_state st)).
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index ca069c1..86f27be 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -136,68 +136,93 @@ Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
-| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e
+| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e
+| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r).
Hint Constructors tr_op : htlspec.
-Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
| tr_instr_Inop :
forall n,
- tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+ tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
| tr_instr_Iop :
forall n op args e dst,
tr_op op args e ->
- tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+ tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
| tr_instr_Icond :
forall n1 n2 cond args s s' i c,
translate_condition cond args s = OK c s' i ->
- tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+ tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
| tr_instr_Ireturn_None :
- tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+ tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
(block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
| tr_instr_Ireturn_Some :
forall r,
- tr_instr fin rtrn st (RTL.Ireturn (Some r))
- (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+ tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
+ (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip
+| tr_instr_Iload :
+ forall mem addr args s s' i c dst n,
+ translate_arr_access mem addr args stk s = OK c s' i ->
+ tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n)
+| tr_instr_Istore :
+ forall mem addr args s s' i c src n,
+ translate_arr_access mem addr args stk s = OK c s' i ->
+ tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src))
+ (state_goto st n).
Hint Constructors tr_instr : htlspec.
Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
- (fin rtrn st : reg) : Prop :=
+ (fin rtrn st stk : reg) : Prop :=
tr_code_intro :
forall s t,
c!pc = Some i ->
stmnts!pc = Some s ->
trans!pc = Some t ->
- tr_instr fin rtrn st i s t ->
- tr_code c pc i stmnts trans fin rtrn st.
+ tr_instr fin rtrn st stk i s t ->
+ tr_code c pc i stmnts trans fin rtrn st stk.
Hint Constructors tr_code : htlspec.
Inductive tr_module (f : RTL.function) : module -> Prop :=
tr_module_intro :
- forall data control fin rtrn st m,
+ forall data control fin rtrn st stk m,
(forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
- tr_code f.(RTL.fn_code) pc i data control fin rtrn st) ->
+ tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
m = (mkmodule f.(RTL.fn_params)
data
control
f.(RTL.fn_entrypoint)
- st fin rtrn) ->
+ st stk fin rtrn) ->
tr_module f m.
Hint Constructors tr_module : htlspec.
Lemma create_reg_datapath_trans :
- forall s s' x i,
- create_reg s = OK x s' i ->
+ forall sz s s' x i,
+ create_reg sz s = OK x s' i ->
s.(st_datapath) = s'.(st_datapath).
Proof. intros. monadInv H. trivial. Qed.
Hint Resolve create_reg_datapath_trans : htlspec.
Lemma create_reg_controllogic_trans :
- forall s s' x i,
- create_reg s = OK x s' i ->
+ forall sz s s' x i,
+ create_reg sz s = OK x s' i ->
s.(st_controllogic) = s'.(st_controllogic).
Proof. intros. monadInv H. trivial. Qed.
Hint Resolve create_reg_controllogic_trans : htlspec.
+Lemma create_arr_datapath_trans :
+ forall sz ln s s' x i,
+ create_arr sz ln s = OK x s' i ->
+ s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_datapath_trans : htlspec.
+
+Lemma create_arr_controllogic_trans :
+ forall sz ln s s' x i,
+ create_arr sz ln s = OK x s' i ->
+ s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_controllogic_trans : htlspec.
+
Lemma get_refl_x :
forall s s' x i,
get s = OK x s' i ->
@@ -214,10 +239,14 @@ Hint Resolve get_refl_s : htlspec.
Ltac inv_incr :=
repeat match goal with
- | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
+ | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] =>
let H1 := fresh "H" in
assert (H1 := H); eapply create_reg_datapath_trans in H;
eapply create_reg_controllogic_trans in H1
+ | [ H: create_arr _ _ ?s = OK _ ?s' _ |- _ ] =>
+ let H1 := fresh "H" in
+ assert (H1 := H); eapply create_arr_datapath_trans in H;
+ eapply create_arr_controllogic_trans in H1
| [ H: get ?s = OK _ _ _ |- _ ] =>
let H1 := fresh "H" in
assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
@@ -281,13 +310,13 @@ Ltac destruct_optional :=
match goal with H: option ?r |- _ => destruct H end.
Lemma iter_expand_instr_spec :
- forall l fin rtrn s s' i x c,
- HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
+ forall l fin rtrn stack s s' i x c,
+ HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
list_norepet (List.map fst l) ->
(forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
(forall pc instr, In (pc, instr) l ->
c!pc = Some instr ->
- tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+ tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
Proof.
induction l; simpl; intros; try contradiction.
destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
@@ -354,9 +383,9 @@ Proof.
econstructor; simpl; trivial.
intros.
inv_incr.
- assert (STC: st_controllogic s8 = st_controllogic s2) by congruence.
- assert (STD: st_datapath s8 = st_datapath s2) by congruence.
- assert (STST: st_st s8 = st_st s2) by congruence.
+ assert (STC: st_controllogic s9 = st_controllogic s3) by congruence.
+ assert (STD: st_datapath s9 = st_datapath s3) by congruence.
+ assert (STST: st_st s9 = st_st s3) by congruence.
rewrite STC. rewrite STD. rewrite STST.
eapply iter_expand_instr_spec; eauto with htlspec.
apply PTree.elements_complete.
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/HTL.v b/src/verilog/HTL.v
index bf38b29..cb081b2 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -43,6 +43,7 @@ Record module: Type :=
mod_controllogic : controllogic;
mod_entrypoint : node;
mod_st : reg;
+ mod_stk : reg;
mod_finish : reg;
mod_return : reg
}.
@@ -59,32 +60,43 @@ Inductive state : Type :=
| State :
forall (m : module)
(st : node)
- (assoc : assocmap),
+ (reg_assoc : assocmap)
+ (arr_assoc : AssocMap.t (list value)),
state
| Returnstate : forall v : value, state.
Inductive step : genv -> state -> Events.trace -> state -> Prop :=
| step_module :
- forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval,
+ forall g t m st ctrl data
+ asr asa
+ basr1 basa1 nasr1 nasa1
+ basr2 basa2 nasr2 nasa2
+ asr' asa'
+ f stval pstval,
m.(mod_controllogic)!st = Some ctrl ->
m.(mod_datapath)!st = Some data ->
Verilog.stmnt_runp f
- (Verilog.mkassociations assoc0 empty_assocmap)
+ (Verilog.mkassociations asr empty_assocmap)
+ (Verilog.mkassociations asa (AssocMap.empty (list value)))
ctrl
- (Verilog.mkassociations assoc1 nbassoc0) ->
+ (Verilog.mkassociations basr1 nasr1)
+ (Verilog.mkassociations basa1 nasa1) ->
Verilog.stmnt_runp f
- (Verilog.mkassociations assoc1 nbassoc0)
+ (Verilog.mkassociations basr1 nasr1)
+ (Verilog.mkassociations basa1 nasa1)
data
- (Verilog.mkassociations assoc2 nbassoc1) ->
- assoc3 = merge_assocmap nbassoc1 assoc2 ->
- assoc3!(m.(mod_st)) = Some stval ->
+ (Verilog.mkassociations basr2 nasr2)
+ (Verilog.mkassociations basa2 nasa2) ->
+ asr' = merge_assocmap nasr2 basr2 ->
+ asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+ asr'!(m.(mod_st)) = Some stval ->
valueToPos stval = pstval ->
- step g (State m st assoc0) t (State m pstval assoc3)
+ step g (State m st asr asa) t (State m pstval asr' asa')
| step_finish :
- forall g t m st assoc retval,
- assoc!(m.(mod_finish)) = Some (1'h"1") ->
- assoc!(m.(mod_return)) = Some retval ->
- step g (State m st assoc) t (Returnstate retval).
+ forall g t m st asr asa retval,
+ asr!(m.(mod_finish)) = Some (1'h"1") ->
+ asr!(m.(mod_return)) = Some retval ->
+ step g (State m st asr asa) t (Returnstate retval).
Hint Constructors step : htl.
Inductive initial_state (p: program): state -> Prop :=
@@ -94,7 +106,7 @@ Inductive initial_state (p: program): state -> Prop :=
Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
st = m.(mod_entrypoint) ->
- initial_state p (State m st empty_assocmap).
+ initial_state p (State m st empty_assocmap (AssocMap.empty (list value))).
Inductive final_state : state -> Integers.int -> Prop :=
| final_state_intro : forall retval retvali,
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..74c08fe 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -34,16 +34,59 @@ From compcert Require Import Errors Smallstep Globalenvs.
Import HexNotationValue.
Import AssocMapNotation.
+Set Implicit Arguments.
+
Definition reg : Type := positive.
Definition node : Type := positive.
Definition szreg : Type := reg * nat.
-Record associations : Type :=
+Record associations (A : Type) : Type :=
mkassociations {
- assoc_blocking : assocmap;
- assoc_nonblocking : assocmap
+ assoc_blocking : AssocMap.t A;
+ assoc_nonblocking : AssocMap.t A
}.
+Definition reg_associations := associations value.
+Definition arr_associations := associations (list value).
+
+Definition assocmap_arr := AssocMap.t (list value).
+
+Definition merge_associations {A : Type} (assoc : associations A) :=
+ mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
+ (AssocMap.empty A).
+
+Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
+ match a ! r with
+ | None => None
+ | Some arr => nth_error arr i
+ end.
+
+Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
+ match i, l with
+ | _, nil => nil
+ | S n, h :: t => h :: list_set n x t
+ | O, h :: t => x :: t
+ end.
+
+Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
+ match a ! r with
+ | None => a
+ | Some arr => AssocMap.set r (list_set i v arr) a
+ end.
+
+Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
+ mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
+
+Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
+ mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)).
+
+Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
+ mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
+
+Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
+ mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
+
+
(** * Verilog AST
The Verilog AST is defined here, which is the target language of the
@@ -97,6 +140,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 +182,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.
@@ -198,8 +243,8 @@ retrieved and set appropriately.
Inductive state : Type :=
| State:
forall (m : module)
- (assoc : assocmap)
- (nbassoc : assocmap)
+ (assoc : reg_associations)
+ (assoc : arr_associations)
(f : fextclk)
(cycle : nat)
(stvar : value),
@@ -240,47 +285,52 @@ Definition unop_run (op : unop) : value -> value :=
| Vnot => vbitneg
end.
-Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
| erun_Vlit :
- forall fext assoc v,
- expr_runp fext assoc (Vlit v) v
+ forall fext reg stack v,
+ expr_runp fext reg stack (Vlit v) v
| erun_Vvar :
- forall fext assoc v r,
- assoc!r = Some v ->
- expr_runp fext assoc (Vvar r) v
+ forall fext reg stack v r,
+ reg!r = Some v ->
+ expr_runp fext reg stack (Vvar r) v
+ | erun_Vvari :
+ forall fext reg stack v iexp i r,
+ expr_runp fext reg stack iexp i ->
+ arr_assocmap_lookup stack r (valueToNat i) = Some v ->
+ expr_runp fext reg stack (Vvari r iexp) v
| erun_Vvar_empty :
- forall fext assoc r sz,
- assoc!r = None ->
- expr_runp fext assoc (Vvar r) (ZToValue sz 0)
+ forall fext reg stack r sz,
+ reg!r = None ->
+ expr_runp fext reg stack (Vvar r) (ZToValue sz 0)
| erun_Vinputvar :
- forall fext assoc r v,
+ forall fext reg stack r v,
fext!r = Some v ->
- expr_runp fext assoc (Vinputvar r) v
+ expr_runp fext reg stack (Vinputvar r) v
| erun_Vbinop :
- forall fext assoc op l r lv rv oper EQ resv,
- expr_runp fext assoc l lv ->
- expr_runp fext assoc r rv ->
+ forall fext reg stack op l r lv rv oper EQ resv,
+ expr_runp fext reg stack l lv ->
+ expr_runp fext reg stack r rv ->
oper = binop_run op ->
resv = oper lv rv EQ ->
- expr_runp fext assoc (Vbinop op l r) resv
+ expr_runp fext reg stack (Vbinop op l r) resv
| erun_Vunop :
- forall fext assoc u vu op oper resv,
- expr_runp fext assoc u vu ->
+ forall fext reg stack u vu op oper resv,
+ expr_runp fext reg stack u vu ->
oper = unop_run op ->
resv = oper vu ->
- expr_runp fext assoc (Vunop op u) resv
+ expr_runp fext reg stack (Vunop op u) resv
| erun_Vternary_true :
- forall fext assoc c ts fs vc vt,
- expr_runp fext assoc c vc ->
- expr_runp fext assoc ts vt ->
+ forall fext reg stack c ts fs vc vt,
+ expr_runp fext reg stack c vc ->
+ expr_runp fext reg stack ts vt ->
valueToBool vc = true ->
- expr_runp fext assoc (Vternary c ts fs) vt
+ expr_runp fext reg stack (Vternary c ts fs) vt
| erun_Vternary_false :
- forall fext assoc c ts fs vc vf,
- expr_runp fext assoc c vc ->
- expr_runp fext assoc fs vf ->
+ forall fext reg stack c ts fs vc vf,
+ expr_runp fext reg stack c vc ->
+ expr_runp fext reg stack fs vf ->
valueToBool vc = false ->
- expr_runp fext assoc (Vternary c ts fs) vf.
+ expr_runp fext reg stack (Vternary c ts fs) vf.
Hint Constructors expr_runp : verilog.
Definition handle_opt {A : Type} (err : errmsg) (val : option A)
@@ -314,6 +364,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
@@ -332,14 +383,23 @@ Definition access_fext (f : fext) (r : reg) : res value :=
if valueToBool cv then expr_run s te else expr_run s fe
end.*)
-(** Return the name of the lhs of an assignment. For now, this function is quite
-simple because only assignment to normal variables is supported and needed. *)
+(** Return the location of the lhs of an assignment. *)
-Definition assign_name (e : expr) : res reg :=
- match e with
- | Vvar r => OK r
- | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
- end.
+Inductive location : Type :=
+| Reg (_ : reg)
+| Array (_ : 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)
+| 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)).
+
+(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *)
+(* match e with *)
+(* | Vvar r => OK r *)
+(* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *)
+(* end. *)
(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
match st with
@@ -409,61 +469,74 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
Definition stmnt_run (s : state) (st : stmnt) : res state :=
stmnt_run' (stmnt_height st) s st. *)
-Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
+Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
+ stmnt -> reg_associations -> arr_associations -> Prop :=
| stmnt_runp_Vskip:
- forall f a, stmnt_runp f a Vskip a
+ forall f ar al, stmnt_runp f ar al Vskip ar al
| stmnt_runp_Vseq:
- forall f st1 st2 as0 as1 as2,
- stmnt_runp f as0 st1 as1 ->
- stmnt_runp f as1 st2 as2 ->
- stmnt_runp f as0 (Vseq st1 st2) as2
+ forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2,
+ stmnt_runp f asr0 asa0 st1 asr1 asa1 ->
+ stmnt_runp f asr1 asa1 st2 asr2 asa2 ->
+ stmnt_runp f asr0 asa1 (Vseq st1 st2) asr2 asa2
| stmnt_runp_Vcond_true:
- forall as0 as1 f c vc stt stf,
- expr_runp f as0.(assoc_blocking) c vc ->
+ forall asr0 asa0 asr1 asa1 f c vc stt stf,
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
valueToBool vc = true ->
- stmnt_runp f as0 stt as1 ->
- stmnt_runp f as0 (Vcond c stt stf) as1
+ stmnt_runp f asr0 asa0 stt asr1 asa1 ->
+ stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
| stmnt_runp_Vcond_false:
- forall as0 as1 f c vc stt stf,
- expr_runp f as0.(assoc_blocking) c vc ->
+ forall asr0 asa0 asr1 asa1 f c vc stt stf,
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
valueToBool vc = false ->
- stmnt_runp f as0 stf as1 ->
- stmnt_runp f as0 (Vcond c stt stf) as1
+ stmnt_runp f asr0 asa0 stt asr1 asa1 ->
+ stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
| stmnt_runp_Vcase_nomatch:
- forall e ve as0 f as1 me mve sc cs def,
- expr_runp f as0.(assoc_blocking) e ve ->
- expr_runp f as0.(assoc_blocking) me mve ->
+ forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
mve <> ve ->
- stmnt_runp f as0 (Vcase e cs def) as1 ->
- stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+ stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 ->
+ stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
| stmnt_runp_Vcase_match:
- forall e ve as0 f as1 me mve sc cs def,
- expr_runp f as0.(assoc_blocking) e ve ->
- expr_runp f as0.(assoc_blocking) me mve ->
+ forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
mve = ve ->
- stmnt_runp f as0 sc as1 ->
- stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+ stmnt_runp f asr0 asa0 sc asr1 asa1 ->
+ stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
| stmnt_runp_Vcase_default:
- forall as0 as1 f st e ve,
- expr_runp f as0.(assoc_blocking) e ve ->
- stmnt_runp f as0 st as1 ->
- stmnt_runp f as0 (Vcase e nil (Some st)) as1
-| stmnt_runp_Vblock:
- forall lhs name rhs rhsval assoc assoc' nbassoc f,
- assign_name lhs = OK name ->
- expr_runp f assoc rhs rhsval ->
- assoc' = (AssocMap.set name rhsval assoc) ->
- stmnt_runp f (mkassociations assoc nbassoc)
+ forall asr0 asa0 asr1 asa1 f st e ve,
+ expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+ stmnt_runp f asr0 asa0 st asr1 asa1 ->
+ 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) ->
+ 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) ->
+ 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) ->
+ expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+ stmnt_runp f asr asa
(Vblock lhs rhs)
- (mkassociations assoc' nbassoc)
-| stmnt_runp_Vnonblock:
- forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
- assign_name lhs = OK name ->
- expr_runp f assoc rhs rhsval ->
- nbassoc' = (AssocMap.set name rhsval nbassoc) ->
- stmnt_runp f (mkassociations assoc nbassoc)
+ 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) ->
+ expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+ stmnt_runp f asr asa
(Vnonblock lhs rhs)
- (mkassociations assoc nbassoc').
+ asr (nonblock_arr r i asa rhsval).
Hint Constructors stmnt_runp : verilog.
(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
@@ -476,36 +549,39 @@ 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.*)
-Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop :=
+Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
+ module_item -> reg_associations -> arr_associations -> Prop :=
| mi_stepp_Valways :
- forall f s0 st s1 c,
- stmnt_runp f s0 st s1 ->
- mi_stepp f s0 (Valways c st) s1
+ forall f sr0 sa0 st sr1 sa1 c,
+ stmnt_runp f sr0 sa0 st sr1 sa0 ->
+ mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
| mi_stepp_Valways_ff :
- forall f s0 st s1 c,
- stmnt_runp f s0 st s1 ->
- mi_stepp f s0 (Valways_ff c st) s1
+ forall f sr0 sa0 st sr1 sa1 c,
+ stmnt_runp f sr0 sa0 st sr1 sa1 ->
+ mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
| mi_stepp_Valways_comb :
- forall f s0 st s1 c,
- stmnt_runp f s0 st s1 ->
- mi_stepp f s0 (Valways_comb c st) s1
+ forall f sr0 sa0 st sr1 sa1 c,
+ stmnt_runp f sr0 sa0 st sr1 sa1 ->
+ mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
| mi_stepp_Vdecl :
- forall f s lhs rhs,
- mi_stepp f s (Vdecl lhs rhs) s.
+ forall f sr sa lhs rhs,
+ mi_stepp f sr sa (Vdecl lhs rhs) sr sa.
Hint Constructors mi_stepp : verilog.
-Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop :=
+Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
+ list module_item -> reg_associations -> arr_associations -> Prop :=
| mis_stepp_Cons :
- forall f mi mis s0 s1 s2,
- mi_stepp f s0 mi s1 ->
- mis_stepp f s1 mis s2 ->
- mis_stepp f s0 (mi :: mis) s2
+ forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
+ mi_stepp f sr0 sa0 mi sr1 sa1 ->
+ mis_stepp f sr1 sa1 mis sr2 sa2 ->
+ mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2
| mis_stepp_Nil :
- forall f s,
- mis_stepp f s nil s.
+ forall f sr sa,
+ mis_stepp f sr sa nil sr sa.
Hint Constructors mis_stepp : verilog.
(*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
@@ -586,19 +662,21 @@ Definition genv := Genv.t unit unit.
Inductive step : state -> state -> Prop :=
| step_module :
- forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
- mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap)
- m.(mod_body)
- (mkassociations assoc1 nbassoc) ->
- assoc2 = merge_assocmap nbassoc assoc1 ->
- Some stvar' = assoc2!(fst m.(mod_state)) ->
- step (State m assoc0 empty_assocmap f cycle stvar)
- (State m assoc2 empty_assocmap f (S cycle) stvar')
+ 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')
| step_finish :
- forall m assoc f cycle stvar result,
- assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
- assoc!(fst m.(mod_return)) = Some result ->
- step (State m assoc empty_assocmap f cycle stvar)
+ 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).
Hint Constructors step : verilog.
generated by cgit (git 2.34.1) at 2024-07-09 07:04:34 +0000