diff options
| -rw-r--r-- | src/Compiler.v | 5 | ||||
| -rw-r--r-- | src/translation/HTLgen.v | 160 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 17 | ||||
| -rw-r--r-- | src/translation/Veriloggen.v | 19 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 10 | ||||
| -rw-r--r-- | src/verilog/PrintHTL.ml | 12 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 18 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 24 |
8 files changed, 60 insertions, 205 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 80aae3f..6efd7a2 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,6 +82,7 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r + @@@ Inlining.transf_program @@ print (print_RTL 1) @@@ HTLgen.transl_program @@ print print_HTL @@ -143,8 +144,8 @@ Proof. exists p7; split. apply Inliningproof.transf_program_match; auto. exists p8; split. apply HTLgenproof.transf_program_match; auto. exists p9; split. apply Veriloggenproof.transf_program_match; auto. - inv T. (* reflexivity. *) -Admitted. + inv T. reflexivity. +Qed. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. 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) diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 2432e7e..620ef14 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -32,7 +32,6 @@ Local Open Scope assocmap. Definition reg := positive. Definition node := positive. -Definition ident := positive. Definition datapath := PTree.t Verilog.stmnt. Definition controllogic := PTree.t Verilog.stmnt. @@ -42,12 +41,6 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> Z.pos p0 <= Integers.Int.max_unsigned. -Inductive instantiation : Type := - (** [HTLinstantiation mod_name inst_name args dest fin]. This does not map directly - to a verilog instantiation. It omits all control signals (clk, rst, etc.) - except the finished signal *) - HTLinstantiation : ident -> ident -> list reg -> reg -> reg -> instantiation. - Record module: Type := mkmodule { mod_params : list reg; @@ -62,8 +55,7 @@ Record module: Type := mod_start : reg; mod_reset : reg; mod_clk : reg; - mod_insts : AssocMap.t instantiation; - mod_scldecls : AssocMap.t Verilog.scl_decl; + mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml index ffa853f..d87b755 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/verilog/PrintHTL.ml @@ -31,7 +31,6 @@ open VericertClflags let pstr pp = fprintf pp "%s" -(* TODO import from PrintVerilog.v *) let rec intersperse c = function | [] -> [] | [x] -> [x] @@ -39,15 +38,10 @@ let rec intersperse c = function let register a = sprintf "reg_%d" (P.to_int a) let registers a = String.concat "" (intersperse ", " (List.map register a)) -let vmodule a = sprintf "%s" (extern_atom a) -let instance a = sprintf "instance_%d" (P.to_int a) let print_instruction pp (pc, i) = fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) -let print_instantiation pp (pc, HTLinstantiation (mod_name, inst_name, args, dst, fin)) = - fprintf pp "%5d:\t %s %s(%s) -> %s\n" pc (vmodule mod_name) (instance inst_name) (registers args) (register dst) - let ptree_to_list ptree = List.sort (fun (pc1, _) (pc2, _) -> compare pc2 pc1) @@ -59,12 +53,6 @@ let print_module pp id f = fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); let datapath = ptree_to_list f.mod_datapath in let controllogic = ptree_to_list f.mod_controllogic in - let insts = ptree_to_list f.mod_insts in - if List.length insts > 0 then ( - fprintf pp " instances {\n"; - List.iter (print_instantiation pp) insts; - fprintf pp " }\n\n"; - ) else fprintf pp " "; fprintf pp "datapath {\n"; List.iter (print_instruction pp) datapath; fprintf pp " }\n\n controllogic {\n"; diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index a355a17..b3fb6c8 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -36,11 +36,6 @@ let fold_map f s = List.map f s |> concat let pstr pp = fprintf pp "%s" -let rec intersperse c = function - | [] -> [] - | [x] -> [x] - | x :: xs -> x :: c :: intersperse c xs - let pprint_binop l r = let unsigned op = sprintf "{%s %s %s}" l op r in let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in @@ -74,8 +69,6 @@ let unop = function | Vnot -> " ! " let register a = sprintf "reg_%d" (P.to_int a) -let vmodule a = sprintf "%s" (extern_atom a) -let instance a = sprintf "instance_%d" (P.to_int a) (*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) @@ -141,12 +134,6 @@ let print_io = function let decl i = function | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] - | Vdeclwire (r, sz) -> concat [indent i; declare "wire" (r, sz)] - | Vinstancedecl (m, name, args) -> concat [ - indent i; vmodule m; " "; - instance name; "("; concat (intersperse ", " (List.map register args)); ")"; - ";\n" - ] (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function @@ -158,6 +145,11 @@ let pprint_module_item i = function | Valways_comb (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + let make_io i io r = concat [indent i; io; " "; register r; ";\n"] let compose f g x = g x |> f diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 27522b4..3b0dd0a 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -39,7 +39,6 @@ Set Implicit Arguments. Definition reg : Type := positive. Definition node : Type := positive. -Definition ident : Type := positive. Definition szreg : Type := reg * nat. Record associations (A : Type) : Type := @@ -100,15 +99,7 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). -Inductive io : Type := -| Vinput : io -| Voutput : io -| Vinout : io. - -Inductive scl_decl : Type := -| VScalar (io: option Verilog.io) (sz : nat) -| VWire (sz : nat). - +Inductive scl_decl : Type := VScalar (sz : nat). Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST @@ -202,13 +193,18 @@ Inductive edge : Type := (** ** Module Items -Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). *) +Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). +The declarations are always register declarations as combinational logic can be +done using combinational always block instead of continuous assignments. *) + +Inductive io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. Inductive declaration : Type := | Vdecl : option io -> reg -> nat -> declaration -| Vdeclarr : option io -> reg -> nat -> nat -> declaration -| Vdeclwire : reg -> nat -> declaration -| Vinstancedecl : ident -> ident -> list reg -> declaration. +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. Inductive module_item : Type := | Vdeclaration : declaration -> module_item |