diff options
Diffstat (limited to 'src/verilog')
-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 |
4 files changed, 16 insertions, 48 deletions
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 |