aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
diff options
context:
space:
mode:
Diffstat (limited to 'src/translation')
-rw-r--r--src/translation/HTLgen.v160
-rw-r--r--src/translation/HTLgenspec.v17
-rw-r--r--src/translation/Veriloggen.v19
3 files changed, 41 insertions, 155 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 8e060e4..68e0293 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -16,9 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-Require Import List.
-Import ListNotations.
-
From compcert Require Import Maps.
From compcert Require Errors Globalenvs Integers.
From compcert Require Import AST RTL.
@@ -34,9 +31,8 @@ Record state: Type := mkstate {
st_st : reg;
st_freshreg: reg;
st_freshstate: node;
- st_scldecls: AssocMap.t scl_decl;
+ st_scldecls: AssocMap.t (option io * scl_decl);
st_arrdecls: AssocMap.t (option io * arr_decl);
- st_insts: AssocMap.t instantiation;
st_datapath: datapath;
st_controllogic: controllogic;
}.
@@ -45,9 +41,8 @@ Definition init_state (st : reg) : state :=
mkstate st
1%positive
1%positive
- (AssocMap.empty scl_decl)
+ (AssocMap.empty (option io * scl_decl))
(AssocMap.empty (option io * arr_decl))
- (AssocMap.empty instantiation)
(AssocMap.empty stmnt)
(AssocMap.empty stmnt).
@@ -64,8 +59,6 @@ Module HTLState <: State.
(forall n,
s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
(forall n,
- s1.(st_insts)!n = None \/ s2.(st_insts)!n = s1.(st_insts)!n) ->
- (forall n,
s1.(st_controllogic)!n = None
\/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
st_incr s1 s2.
@@ -80,9 +73,8 @@ Module HTLState <: State.
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; intros; try congruence.
- - destruct H4 with n; destruct H9 with n; intuition congruence.
- - destruct H5 with n; destruct H10 with n; intuition congruence.
- - destruct H6 with n; destruct H11 with n; intuition congruence.
+ - destruct H4 with n; destruct H8 with n; intuition congruence.
+ - destruct H5 with n; destruct H9 with n; intuition congruence.
Qed.
End HTLState.
@@ -124,7 +116,6 @@ Lemma add_instr_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
Proof.
@@ -140,9 +131,8 @@ Lemma declare_reg_state_incr :
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (VScalar i sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
- s.(st_insts)
s.(st_datapath)
s.(st_controllogic)).
Proof. auto with htlh. Qed.
@@ -152,9 +142,8 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (VScalar i sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
- s.(st_insts)
s.(st_datapath)
s.(st_controllogic))
(declare_reg_state_incr i s r sz).
@@ -169,7 +158,6 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(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)
@@ -187,7 +175,6 @@ Lemma add_instr_skip_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n Vskip s.(st_controllogic))).
Proof.
@@ -206,7 +193,6 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(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,7 +210,6 @@ Lemma add_node_skip_state_incr :
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(AssocMap.set n Vskip s.(st_datapath))
(AssocMap.set n st s.(st_controllogic))).
Proof.
@@ -243,52 +228,12 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(AssocMap.set n Vskip s.(st_datapath))
(AssocMap.set n st s.(st_controllogic)))
(add_node_skip_state_incr s n st STM TRANS)
| _, _ => Error (Errors.msg "HTL.add_instr")
end.
-Fixpoint assocmap_nextavailable {A: Type} (m: AssocMap.t A) : positive :=
- match m with
- | AssocMap.Leaf => 1
- | AssocMap.Node _ _ r => (assocmap_nextavailable r)~1
- end.
-
-Theorem assocmap_nextavailable_correct : forall (A: Type) m, m!(@assocmap_nextavailable A m) = None.
-Proof. induction m; tauto. Qed.
-
-Lemma add_instance_state_incr :
- forall s inst,
- st_incr s
- (mkstate
- s.(st_st)
- s.(st_freshreg)
- s.(st_freshstate)
- s.(st_scldecls)
- s.(st_arrdecls)
- (AssocMap.set (assocmap_nextavailable s.(st_insts)) inst s.(st_insts))
- s.(st_datapath)
- s.(st_controllogic)).
-Proof.
-Admitted.
-
-Definition add_instance (mod_name: ident) (args: list reg) (finished: reg) (dst: reg) : mon unit :=
- fun s =>
- let instname := assocmap_nextavailable s.(st_insts) in
- let inst := HTL.HTLinstantiation mod_name instname args dst finished in
- OK tt (mkstate
- s.(st_st)
- s.(st_freshreg)
- s.(st_freshstate)
- s.(st_scldecls)
- s.(st_arrdecls)
- (AssocMap.set instname inst s.(st_insts))
- s.(st_datapath)
- s.(st_controllogic))
- (add_instance_state_incr s inst).
-
Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
@@ -441,7 +386,6 @@ Lemma add_branch_instr_state_incr:
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(AssocMap.set n Vskip (st_datapath s))
(AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
Proof.
@@ -460,7 +404,6 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
- s.(st_insts)
(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)
@@ -501,58 +444,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
end)
(enumerate 0 ns).
-Lemma create_reg_state_incr:
- forall s sz i,
- st_incr s (mkstate
- s.(st_st)
- (Pos.succ (st_freshreg s))
- (st_freshstate s)
- (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls))
- s.(st_arrdecls)
- s.(st_insts)
- (st_datapath s)
- (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (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) (VScalar i sz) s.(st_scldecls))
- (st_arrdecls s)
- (st_insts s)
- (st_datapath s)
- (st_controllogic s))
- (create_reg_state_incr s sz i).
-
-Lemma create_wire_state_incr:
- forall s sz,
- st_incr s (mkstate
- s.(st_st)
- (Pos.succ (st_freshreg s))
- (st_freshstate s)
- (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls))
- s.(st_arrdecls)
- s.(st_insts)
- (st_datapath s)
- (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_wire (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) (VWire sz) s.(st_scldecls))
- (st_arrdecls s)
- (st_insts s)
- (st_datapath s)
- (st_controllogic s))
- (create_wire_state_incr s sz).
-
Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
match ni with
(n, i) =>
@@ -578,14 +469,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
do dst <- translate_arr_access mem addr args stack;
add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
else error (Errors.msg "State is larger than 2^32.")
- | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
- | Icall sig (inr fn) args dst n' =>
- if Z.leb (Z.pos n') Integers.Int.max_unsigned then
- do finished <- create_wire 1;
- do res <- create_wire 32;
- (* TODO implement control and datapaths for instantiated module *)
- add_instance fn args finished res
- else error (Errors.msg "State is larger than 2^32.")
+ | 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 =>
@@ -607,6 +491,30 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
end
end.
+Lemma create_reg_state_incr:
+ forall s sz i,
+ st_incr s (mkstate
+ s.(st_st)
+ (Pos.succ (st_freshreg s))
+ (st_freshstate s)
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+ s.(st_arrdecls)
+ (st_datapath s)
+ (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (i : option io) (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) (i, VScalar sz) s.(st_scldecls))
+ (st_arrdecls s)
+ (st_datapath s)
+ (st_controllogic s))
+ (create_reg_state_incr s sz i).
+
Lemma create_arr_state_incr:
forall s sz ln i,
st_incr s (mkstate
@@ -615,7 +523,6 @@ Lemma create_arr_state_incr:
(st_freshstate s)
s.(st_scldecls)
(AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
- (st_insts s)
(st_datapath s)
(st_controllogic s)).
Proof. constructor; simpl; auto with htlh. Qed.
@@ -628,7 +535,6 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
(st_freshstate s)
s.(st_scldecls)
(AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
- (st_insts s)
(st_datapath s)
(st_controllogic s))
(create_arr_state_incr s sz ln i).
@@ -692,7 +598,6 @@ Definition transf_module (f: function) : mon module :=
start
rst
clk
- current_state.(st_insts)
current_state.(st_scldecls)
current_state.(st_arrdecls)
(conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
@@ -705,9 +610,8 @@ Definition max_state (f: function) : state :=
mkstate st
(Pos.succ st)
(Pos.succ (max_pc_function f))
- (AssocMap.set st (VScalar None 32) (st_scldecls (init_state st)))
+ (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
(st_arrdecls (init_state st))
- (st_insts (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 67b3648..541f9fa 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -167,12 +167,12 @@ Hint Constructors tr_code : htlspec.
Inductive tr_module (f : RTL.function) : module -> Prop :=
tr_module_intro :
- forall data control fin rtrn st stk stk_len m start rst clk insts scldecls arrdecls wf,
+ forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf,
m = (mkmodule f.(RTL.fn_params)
data
control
f.(RTL.fn_entrypoint)
- st stk stk_len fin rtrn start rst clk insts scldecls arrdecls wf) ->
+ st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) ->
(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 stk) ->
stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
@@ -444,10 +444,10 @@ Proof.
- monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
apply declare_reg_freshreg_trans in EQ1. congruence.
- monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
- (* - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *)
- (* congruence. *)
+ - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
+ congruence.
(*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*)
-Admitted.
+Qed.
Hint Resolve transf_instr_freshreg_trans : htlspec.
Lemma collect_trans_instr_freshreg_trans :
@@ -509,7 +509,6 @@ Lemma iter_expand_instr_spec :
c!pc = Some instr ->
tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
Proof.
-(* FIXME Broken by mpardalos
induction l; simpl; intros; try contradiction.
destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
destruct (peq pc pc1).
@@ -578,8 +577,7 @@ Proof.
destruct H2. inversion H2. subst. contradiction.
intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
destruct H2. inv H2. contradiction. assumption. assumption.
-*)
-Admitted.
+Qed.
Hint Resolve iter_expand_instr_spec : htlspec.
Lemma create_arr_inv : forall w x y z a b c d,
@@ -616,9 +614,7 @@ Proof.
monadInv Heqr.
repeat unfold_match EQ9. monadInv EQ9.
-Admitted.
-(* FIXME Broken by @mpardalos
(* TODO: We should be able to fold this into the automation. *)
pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5.
pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL.
@@ -643,4 +639,3 @@ Admitted.
eapply iter_expand_instr_spec; eauto with htlspec.
apply PTree.elements_complete.
Qed.
-*)
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 07034cc..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -16,9 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-Require Import List.
-Import ListNotations.
-
From compcert Require Import Maps.
From compcert Require Errors.
From compcert Require Import AST.
@@ -30,11 +27,8 @@ Definition transl_list_fun (a : node * Verilog.stmnt) :=
Definition transl_list st := map transl_list_fun st.
-Definition scl_to_Vdecl_fun (a : reg * scl_decl) :=
- match a with
- | (r, (VScalar io sz)) => (Vdecl io r sz)
- | (r, VWire sz) => (Vdeclwire r sz)
- end.
+Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
+ match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end.
Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
@@ -43,12 +37,6 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
-Definition inst_to_Vdecl_fun (m: HTL.module) (a: positive * HTL.instantiation) :=
- match a with (_, HTLinstantiation mod_name inst_name args fin dst) =>
- (Vinstancedecl mod_name inst_name ([mod_start m; mod_reset m; mod_clk m] ++ args ++ [dst;fin])) end.
-
-Definition inst_to_Vdecl (m: HTL.module) := map (inst_to_Vdecl_fun m).
-
Definition transl_module (m : HTL.module) : Verilog.module :=
let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
@@ -58,8 +46,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
(Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
:: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
:: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
- ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))
- ++ inst_to_Vdecl m (AssocMap.elements m.(mod_insts))) in
+ ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
Verilog.mkmodule m.(mod_start)
m.(mod_reset)
m.(mod_clk)
generated by cgit (git 2.34.1) at 2024-07-07 14:35:25 +0000