diff options
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/HTL.v | 9 | ||||
-rw-r--r-- | src/verilog/PrintHTL.ml | 9 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.ml | 13 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 5 |
5 files changed, 20 insertions, 18 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 6ab733f..4d0ba42 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -32,6 +32,7 @@ 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. @@ -41,6 +42,12 @@ 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; @@ -55,7 +62,7 @@ Record module: Type := mod_start : reg; mod_reset : reg; mod_clk : reg; - mod_insts : AssocMap.t Verilog.instantiation; + mod_insts : AssocMap.t instantiation; 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 f4e3e5c..ffa853f 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/verilog/PrintHTL.ml @@ -31,6 +31,7 @@ open VericertClflags let pstr pp = fprintf pp "%s" +(* TODO import from PrintVerilog.v *) let rec intersperse c = function | [] -> [] | [x] -> [x] @@ -38,12 +39,14 @@ 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_instance pp (pc, i) = - fprintf pp "%5d:\t%s" pc (pprint_instantiation 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 @@ -59,7 +62,7 @@ let print_module pp id f = let insts = ptree_to_list f.mod_insts in if List.length insts > 0 then ( fprintf pp " instances {\n"; - List.iter (print_instance pp) insts; + List.iter (print_instantiation pp) insts; fprintf pp " }\n\n"; ) else fprintf pp " "; fprintf pp "datapath {\n"; diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index a2fd78f..6fe2292 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -109,13 +109,6 @@ let rec pprint_stmnt i = | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] -let pprint_instantiation = function - | Vinstantiation (m, name, args) -> concat [ - vmodule m; " "; - instance name; "("; concat (intersperse ", " (List.map register args)); ")"; - ";\n" - ] - let rec pprint_edge = function | Vposedge r -> concat ["posedge "; register r] | Vnegedge r -> concat ["negedge "; register r] @@ -148,7 +141,11 @@ 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)] - | Vinstancedecl inst -> concat [indent i; pprint_instantiation inst] + | 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 diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 1a37126..6a15ee9 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,8 +18,6 @@ val pprint_stmnt : int -> Verilog.stmnt -> string -val pprint_instantiation : Verilog.instantiation -> string - val print_value : out_channel -> ValueInt.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 4f5c838..6f65fdc 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -177,9 +177,6 @@ Inductive stmnt : Type := | Vblock : expr -> expr -> stmnt | Vnonblock : expr -> expr -> stmnt. -Inductive instantiation : Type := - Vinstantiation : ident -> ident -> list reg -> instantiation. - (** ** Edges These define when an always block should be triggered, for example if the always @@ -209,7 +206,7 @@ Inductive io : Type := Inductive declaration : Type := | Vdecl : option io -> reg -> nat -> declaration | Vdeclarr : option io -> reg -> nat -> nat -> declaration -| Vinstancedecl : instantiation -> declaration. +| Vinstancedecl : ident -> ident -> list reg -> declaration. Inductive module_item : Type := | Vdeclaration : declaration -> module_item |