diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 818284c40..8c7ab4eed 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -129,6 +129,14 @@ let sv_return_type_from_attribute attr_data_opt = | None -> Some ctyp | Some _ -> raise (Reporting.err_general l "return_type field should not have positional argument") +let sv_dpi_from_attr attr_data_opt = + let open Util.Option_monad in + let* fields = Option.bind attr_data_opt attribute_data_object in + let* dpi = List.assoc_opt "dpi" fields in + match dpi with + | AD_aux (AD_bool b, _) -> Some b + | AD_aux (_, l) -> raise (Reporting.err_general l "dpi field must be a boolean") + (* The direct footprint contains information about the effects directly performed by the function itself, i.e. not those from any transitive function calls. It is constructed by the footprint @@ -525,15 +533,18 @@ module Make (Config : CONFIG) = struct let simple_type str = (str, None) - let rec sv_ctyp = function + let rec sv_ctyp ?(two_state = false) = function | CT_bool -> simple_type "bit" + | CT_bit when two_state -> simple_type "bit" | CT_bit -> simple_type "logic" | CT_fbits 0 -> simple_type "sail_zwbv" + | CT_fbits width when two_state -> ksprintf simple_type "bit [%d:0]" (width - 1) | CT_fbits width -> ksprintf simple_type "logic [%d:0]" (width - 1) | CT_sbits max_width -> let logic = sprintf "logic [%d:0]" (max_width - 1) in ksprintf simple_type "struct packed { logic [7:0] size; %s bits; }" logic | CT_lbits -> simple_type "sail_bits" + | CT_fint width when two_state -> ksprintf simple_type "bit [%d:0]" (width - 1) | CT_fint width -> ksprintf simple_type "logic [%d:0]" (width - 1) | CT_lint -> ksprintf simple_type "logic [%d:0]" (Config.max_unknown_integer_width - 1) | CT_string -> simple_type (if Config.nostrings then "sail_unit" else "string") @@ -541,20 +552,25 @@ module Make (Config : CONFIG) = struct | CT_variant (id, _) | CT_struct (id, _) | CT_enum (id, _) -> simple_type (sv_type_id_string id) | CT_constant c -> let width = required_width c in - ksprintf simple_type "logic [%d:0]" (width - 1) + if two_state then ksprintf simple_type "bit [%d:0]" (width - 1) + else ksprintf simple_type "logic [%d:0]" (width - 1) | CT_ref ctyp -> ksprintf simple_type "sail_reg_%s" (Util.zencode_string (string_of_ctyp ctyp)) | CT_fvector (len, ctyp) -> let outer_index = sprintf "[%d:0]" (len - 1) in begin - match sv_ctyp ctyp with + match sv_ctyp ~two_state ctyp with | ty, Some inner_index -> (ty, Some (inner_index ^ outer_index)) | ty, None -> (ty, Some outer_index) end | CT_list ctyp -> begin - match sv_ctyp ctyp with ty, Some inner_index -> (ty, Some (inner_index ^ "[$]")) | ty, None -> (ty, Some "[$]") + match sv_ctyp ~two_state ctyp with + | ty, Some inner_index -> (ty, Some (inner_index ^ "[$]")) + | ty, None -> (ty, Some "[$]") end | CT_vector ctyp -> begin - match sv_ctyp ctyp with ty, Some inner_index -> (ty, Some (inner_index ^ "[]")) | ty, None -> (ty, Some "[]") + match sv_ctyp ~two_state ctyp with + | ty, Some inner_index -> (ty, Some (inner_index ^ "[]")) + | ty, None -> (ty, Some "[]") end | CT_real -> simple_type "sail_real" | CT_rounding_mode -> simple_type "sail_rounding_mode" @@ -2199,6 +2215,30 @@ module Make (Config : CONFIG) = struct | SVD_fundef f -> pp_fundef f | SVD_module m -> pp_module m | SVD_type type_def -> pp_type_def type_def + | SVD_dpi_function { function_name; return_type; param_types } -> + let ret_ty, typedef = + match return_type with + | Some ret_ctyp -> + (* Per the SystemVerilog LRM, a DPI function can only return + two-state types other than a single logic *) + let ret_ty, index_ty = sv_ctyp ~two_state:true ret_ctyp in + begin + match index_ty with + | Some index -> + let encoded = Util.zencode_string (string_of_ctyp ret_ctyp) in + let new_ty = string ("t_" ^ pp_sv_name_string function_name ^ "_" ^ encoded) in + ( new_ty, + separate space [string "typedef"; string ret_ty; new_ty; string index] ^^ semi ^^ twice hardline + ) + | None -> (string ret_ty, empty) + end + | None -> (string "void", empty) + in + let params = List.mapi (fun n ctyp -> wrap_type ctyp (string ("param" ^ string_of_int n))) param_types in + typedef + ^^ separate space [string "import"; string "\"DPI-C\""; string "function"; ret_ty; pp_sv_name function_name] + ^^ parens (separate (comma ^^ space) params) + ^^ semi let sv_fundef_with ctx f params param_ctyps ret_ctyp fun_body = let sv_ret_ty, index_ty = sv_ctyp ret_ctyp in @@ -2390,7 +2430,40 @@ module Make (Config : CONFIG) = struct let svir_cdef spec_info ctx fn_ctyps (CDEF_aux (aux, def_annot)) = match aux with - | CDEF_val (f, _, param_ctyps, ret_ctyp) -> ([], Bindings.add f (param_ctyps, ret_ctyp) fn_ctyps) + | CDEF_val (f, ext_name, param_ctyps, ret_ctyp) -> + let sv_function_attr_opt = get_def_attribute "sv_function" def_annot in + if Option.is_some sv_function_attr_opt then ( + let _, sv_function_attr = Option.get sv_function_attr_opt in + match sv_dpi_from_attr sv_function_attr with + (* If the dpi attribute isn't present, or is false don't do anything *) + | None | Some false -> ([], Bindings.add f (param_ctyps, ret_ctyp) fn_ctyps) + | Some true -> + let ret_ctyp = + match sv_return_type_from_attribute sv_function_attr with None -> ret_ctyp | Some ctyp' -> ctyp' + in + let param_ctyps = + match sv_types_from_attribute ~arity:(List.length param_ctyps) sv_function_attr with + | None -> param_ctyps + | Some conversions -> + List.map + (fun (ctyp, convert) -> match convert with None -> ctyp | Some ctyp' -> ctyp') + (List.combine param_ctyps conversions) + in + + let dpi_import = + SVD_aux + ( SVD_dpi_function + { + function_name = Option.fold ~none:(SVN_id f) ~some:(fun s -> SVN_string s) ext_name; + return_type = Some ret_ctyp; + param_types = param_ctyps; + }, + def_annot.loc + ) + in + ([dpi_import], Bindings.add f (param_ctyps, ret_ctyp) fn_ctyps) + ) + else ([], Bindings.add f (param_ctyps, ret_ctyp) fn_ctyps) | CDEF_fundef (f, _, params, body) -> let debug_attr = get_def_attribute "jib_debug" def_annot in if List.mem (string_of_id f) Config.ignore then ([], fn_ctyps) diff --git a/src/sail_sv_backend/jib_sv.mli b/src/sail_sv_backend/jib_sv.mli index b954cdcb0..aed6f502d 100644 --- a/src/sail_sv_backend/jib_sv.mli +++ b/src/sail_sv_backend/jib_sv.mli @@ -106,7 +106,7 @@ module Make (Config : CONFIG) : sig val sv_fundef_with : Jib_compile.ctx -> string -> Ast.id list -> Jib.ctyp list -> Jib.ctyp -> PPrint.document -> PPrint.document - val sv_ctyp : Jib.ctyp -> string * string option + val sv_ctyp : ?two_state:bool -> Jib.ctyp -> string * string option val wrap_type : Jib.ctyp -> PPrint.document -> PPrint.document diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index ec3c5f301..09d0cc39e 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -69,6 +69,7 @@ let opt_includes = ref [] type verilate_mode = Verilator_none | Verilator_compile | Verilator_run let opt_verilate = ref Verilator_none +let opt_verilate_args = ref None let opt_line_directives = ref false @@ -116,6 +117,10 @@ let verilog_options = ), " Invoke verilator on generated output" ); + ( "-sv_verilate_args", + Arg.String (fun s -> opt_verilate_args := Some s), + " Extra arguments to pass to verilator" + ); ("-sv_lines", Arg.Set opt_line_directives, " output `line directives"); ("-sv_comb", Arg.Set opt_comb, " output an always_comb block instead of initial block"); ("-sv_inregs", Arg.Set opt_inregs, " take register values from inputs"); @@ -608,12 +613,15 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = (verilator_cpp_wrapper "sail_toplevel"); Util.close_output_with_check file_info; + let extra = match !opt_verilate_args with None -> "" | Some args -> " " ^ args in + (* Verilator sometimes just spuriously returns non-zero exit codes even when it suceeds, so we don't use system_checked here, and just hope for the best. *) let verilator_command = - sprintf "verilator --cc --exe --build -j 0 --top-module sail_toplevel -I%s --Mdir %s_obj_dir sim_%s.cpp %s.sv" - sail_sv_libdir out out out + sprintf + "verilator --cc --exe --build -j 0 --top-module sail_toplevel -I%s --Mdir %s_obj_dir sim_%s.cpp %s.sv%s" + sail_sv_libdir out out out extra in print_endline ("Verilator command: " ^ verilator_command); let _ = Unix.system verilator_command in diff --git a/src/sail_sv_backend/sv_ir.ml b/src/sail_sv_backend/sv_ir.ml index d9cc87983..616f12189 100644 --- a/src/sail_sv_backend/sv_ir.ml +++ b/src/sail_sv_backend/sv_ir.ml @@ -107,6 +107,7 @@ and sv_def_aux = output_connections : sv_place list; } | SVD_always_comb of sv_statement + | SVD_dpi_function of { function_name : sv_name; return_type : Jib.ctyp option; param_types : Jib.ctyp list } and sv_place = | SVP_id of Jib.name @@ -357,6 +358,11 @@ let rec visit_sv_def (vis : svir_visitor) outer_def = | SVD_always_comb statement -> let statement' = visit_sv_statement vis statement in if statement == statement' then no_change else SVD_aux (SVD_always_comb statement', l) + | SVD_dpi_function { function_name; return_type; param_types } -> + let return_type' = map_no_copy_opt (visit_ctyp (vis :> common_visitor)) return_type in + let param_types' = map_no_copy (visit_ctyp (vis :> common_visitor)) param_types in + if return_type == return_type' && param_types = param_types' then no_change + else SVD_aux (SVD_dpi_function { function_name; return_type = return_type'; param_types = param_types' }, l) in do_visit vis (vis#vdef outer_def) aux outer_def diff --git a/src/sail_sv_backend/sv_ir.mli b/src/sail_sv_backend/sv_ir.mli index 6d0e1e923..1ce84c6eb 100644 --- a/src/sail_sv_backend/sv_ir.mli +++ b/src/sail_sv_backend/sv_ir.mli @@ -105,6 +105,7 @@ and sv_def_aux = output_connections : sv_place list; } | SVD_always_comb of sv_statement + | SVD_dpi_function of { function_name : sv_name; return_type : Jib.ctyp option; param_types : Jib.ctyp list } and sv_place = | SVP_id of Jib.name diff --git a/src/sail_sv_backend/sv_optimize.ml b/src/sail_sv_backend/sv_optimize.ml index 30eb598d9..ddff13965 100644 --- a/src/sail_sv_backend/sv_optimize.ml +++ b/src/sail_sv_backend/sv_optimize.ml @@ -615,7 +615,7 @@ module RemoveUnusedVariables = struct let rec def_uses stack uses (SVD_aux (aux, l)) = match aux with - | SVD_type _ | SVD_null -> () + | SVD_type _ | SVD_null | SVD_dpi_function _ -> () | SVD_fundef { params; body; _ } -> let paramset = List.fold_left (fun set (id, _) -> NameSet.add (name id) set) NameSet.empty params in push (Function paramset) stack; diff --git a/test/c/sv_dpi.expect b/test/c/sv_dpi.expect new file mode 100644 index 000000000..0553d3a2e --- /dev/null +++ b/test/c/sv_dpi.expect @@ -0,0 +1 @@ +x = 7 diff --git a/test/c/sv_dpi.sail b/test/c/sv_dpi.sail new file mode 100644 index 000000000..b2ecb11c1 --- /dev/null +++ b/test/c/sv_dpi.sail @@ -0,0 +1,23 @@ +default Order dec + +$include + +$iftarget systemverilog + +$option --sv-verilate-args "include/sv_dpi.cpp" + +$[sv_function { types = ["int", "int"], return_type = "int", dpi = true }] +val foo = impure "sv_dpi_foo" : (int, int) -> int + +$else + +function foo(x : int, y : int) -> int = x + y + +$endif + +val main : unit -> unit + +function main() = { + let x = foo(2, 5); + print_int("x = ", x) +} diff --git a/test/sv/.gitignore b/test/sv/.gitignore index 8df2fcca4..fa697bc49 100644 --- a/test/sv/.gitignore +++ b/test/sv/.gitignore @@ -1,2 +1,2 @@ # Ignore generated directories from SV tests -**/* +*_obj_dir/* diff --git a/test/sv/include/sv_dpi.cpp b/test/sv/include/sv_dpi.cpp new file mode 100644 index 000000000..533553383 --- /dev/null +++ b/test/sv/include/sv_dpi.cpp @@ -0,0 +1,7 @@ +#include "svdpi.h" +#include "Vsail_toplevel__Dpi.h" + +svBitVecVal sv_dpi_foo(const svLogicVecVal* param0, const svLogicVecVal* param1) +{ + return param0->aval + param1->aval; +}