From 571123367af7e6549f78a829faf6e3eb6cb65e6a Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 13 Nov 2024 13:13:29 +0000 Subject: [PATCH] SV: Various improvements Subsets of primitives can be linked with DPI-C, e.g. just the memory functions in the library Fix for pow2 with fixed-width integers Allowing passing CFLAGS and LDFLAGS options to verilator Option for linking Sail runtime with generated verilator emulator --- editors/sail-mode.el | 2 +- lib/sv/sail_modules.sv | 36 ++++--- src/lib/mappings.ml | 147 +++++++++++++++++++------- src/lib/smt_gen.ml | 14 ++- src/lib/util.ml | 1 + src/lib/util.mli | 4 +- src/lib/value.ml | 3 + src/sail_sv_backend/jib_sv.ml | 8 +- src/sail_sv_backend/jib_sv.mli | 1 + src/sail_sv_backend/sail_plugin_sv.ml | 88 ++++++++++++--- test/c/pow2_var.expect | 4 + test/c/pow2_var.sail | 23 ++++ 12 files changed, 253 insertions(+), 78 deletions(-) create mode 100644 test/c/pow2_var.expect create mode 100644 test/c/pow2_var.sail diff --git a/editors/sail-mode.el b/editors/sail-mode.el index 3466bbc5a..a1db504e5 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -34,7 +34,7 @@ '("val" "outcome" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by" "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from" - "pure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private" + "pure" "impure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private" "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield" "mapping" "where" "with" "implicit" "instantiation" "impl" "forwards" "backwards")) diff --git a/lib/sv/sail_modules.sv b/lib/sv/sail_modules.sv index 7ed4978fa..322815c28 100644 --- a/lib/sv/sail_modules.sv +++ b/lib/sv/sail_modules.sv @@ -37,7 +37,7 @@ module print_endline out_sail_stdout = {in_sail_stdout, in_str, "\n"}; out_return = SAIL_UNIT; end -endmodule // print_endline +endmodule function automatic bit valid_hex_bits(int n, string hex); int len = hex.len(); @@ -72,23 +72,29 @@ function automatic bit valid_hex_bits(int n, string hex); end; return 1'h1; -endfunction // valid_hex_bits +endfunction function automatic string string_take(string str, int n); return str.substr(0, n - 1); -endfunction // string_take +endfunction function automatic string string_drop(string str, int n); return str.substr(n, str.len() - 1); -endfunction // string_drop +endfunction function automatic int string_length(string str); return str.len(); -endfunction // string_length +endfunction + +`ifdef SAIL_DPI_MEMORY +import "DPI-C" function bit[7:0] sail_read_byte(logic [63:0] addr); +import "DPI-C" function bit sail_read_tag(logic [63:0] addr); +`else logic [7:0] sail_memory [logic [63:0]]; bit sail_tag_memory [logic [63:0]]; +`endif typedef struct { logic [63:0] paddr; @@ -99,15 +105,17 @@ typedef sail_write sail_memory_writes [$]; function automatic sail_bits emulator_read_mem(logic [63:0] addrsize, sail_bits addr, sail_int n); logic [63:0] paddr; - /* verilator lint_off UNOPTFLAT */ logic [SAIL_BITS_WIDTH-1:0] buffer; - sail_int i; + logic [SAIL_INDEX_WIDTH-2:0] i; paddr = addr.bits[63:0]; - for (i = n; i > 0; i = i - 1) begin - buffer = buffer << 8; - buffer[7:0] = sail_memory[paddr + (i[63:0] - 1)]; + for (i = n[SAIL_INDEX_WIDTH-2:0]; i > 0; i = i - 1) begin +`ifdef SAIL_DPI_MEMORY + buffer[7 + (i * 8) -: 8] = sail_read_byte(paddr + (64'(i) - 1)); +`else + buffer[7 + (i * 8) -: 8] = sail_memory[paddr + (64'(i) - 1)]; +`endif end return '{n[SAIL_INDEX_WIDTH-1:0] * 8, buffer}; @@ -124,10 +132,14 @@ endfunction function automatic bit emulator_read_tag(logic [63:0] addrsize, sail_bits addr); logic [63:0] paddr; paddr = addr.bits[63:0]; +`ifdef SAIL_DPI_MEMORY + return sail_read_tag(paddr); +`else if (sail_tag_memory.exists(paddr) == 1) return sail_tag_memory[paddr]; else return 1'b0; +`endif endfunction module emulator_write_mem @@ -160,10 +172,10 @@ module emulator_write_tag output sail_unit ret, output sail_memory_writes out_writes ); -endmodule // emulator_write_tag +endmodule function automatic string sail_string_of_bits(sail_bits bv); return ""; -endfunction // sail_string_of_bits +endfunction `endif diff --git a/src/lib/mappings.ml b/src/lib/mappings.ml index 4d9462607..d73af354f 100644 --- a/src/lib/mappings.ml +++ b/src/lib/mappings.ml @@ -75,9 +75,40 @@ } ]} - which is quite complicated. The [$[mapping_match]] attribute - ensures the type checker can re-check the mapping despite - the added option type. *) + which is quite complicated. The [$[mapping_match]] attribute + ensures the type checker can re-check the mapping despite + the added option type. + + There are a few constraints that make this rewrite as tricky looking as it is: + + - We don't want to duplicate any expression (`` and ``). + - We can't change the evaluation order, as this might change the + observable side effects of the expression. This includes the order + in which we evaluate `mapping_forwards` relative to all the other + expressions. + - The scope of all pattern bindings should be preserved. + - The match can be embedded in any context (so we can't use `return`). + - Mappings can be nested e.g. `m1(m2(m3()))`. + + If the mapping match is in a return position we can instead rewrite to + + {@sail[ + let y = x in { + $[complete] match y { + => return , + z if mapping_forwards_matches(z) => $[complete] match mapping_forwards(z) { + A => return , + _ => (), + }, + _ => (), + }; + $[] match y { + + } + } + ]} + + which avoids the nested match statements and option type. *) open Ast open Ast_util @@ -175,23 +206,29 @@ let name_gen prefix = in fresh -(* Take a arm like " => " and turn it into " => Some()" *) -let some_arm = function - | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, mk_exp (E_app (mk_id "Some", [exp]))), annot) - | Pat_aux (Pat_when (pat, guard, exp), annot) -> - Pat_aux (Pat_when (pat, guard, mk_exp (E_app (mk_id "Some", [exp]))), annot) +let wrap_some ~return_position exp = + if return_position then mk_exp (E_return exp) else mk_exp (E_app (mk_id "Some", [exp])) -let wildcard_none = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) +(* Take a arm like " => " and turn it into " => Some()", or + " => return " when in return position. *) +let some_arm ~return_position = function + | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, wrap_some ~return_position exp), annot) + | Pat_aux (Pat_when (pat, guard, exp), annot) -> Pat_aux (Pat_when (pat, guard, wrap_some ~return_position exp), annot) + +(* Create an arm like "_ => None()" or "_ => ()" (when in return position) *) +let wildcard_arm ~return_position () = + if return_position then mk_pexp (Pat_exp (mk_pat P_wild, mk_lit_exp L_unit)) + else mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) let unwrap_some = mk_pexp (Pat_exp (mk_pat (P_app (mk_id "Some", [mk_pat (P_id (mk_id "result"))])), mk_exp (E_id (mk_id "result")))) let none_pexp exp = mk_pexp (Pat_exp (mk_pat (P_app (mk_id "None", [mk_pat (P_lit (mk_lit L_unit))])), exp)) +let remove_completeness_attribute uannot = uannot |> remove_attribute "incomplete" |> remove_attribute "complete" + let match_completeness c (E_aux (aux, (l, uannot))) = - let uannot = - uannot |> remove_attribute "incomplete" |> remove_attribute "complete" |> add_attribute (gen_loc l) c None - in + let uannot = uannot |> remove_completeness_attribute |> add_attribute (gen_loc l) c None in match aux with | E_match _ -> E_aux (aux, (l, uannot)) | _ -> Reporting.unreachable l __POS__ "Non-match in match_completeness" @@ -237,7 +274,7 @@ let tuple_exp = function [exp] -> exp | exps -> mk_exp (E_tuple exps) let tuple_pat = function [pat] -> pat | pats -> mk_pat (P_tuple pats) -let rec mappings_match is_mapping subst mappings pexp = +let rec mappings_match ~terminal ~return_position is_mapping subst mappings pexp = let handle_mapping (subst_id, P_aux (aux, (l, uannot))) = match aux with | P_app (mapping, [subpat]) -> @@ -257,50 +294,78 @@ let rec mappings_match is_mapping subst mappings pexp = let subpat = tuple_pat (List.map (fun (_, _, subpat) -> subpat) mappings) in let match_exp = let arms = - [ - construct_pexp (subpat, guard_opt, mk_exp (E_app (mk_id "Some", [exp])), (gen_loc l, empty_uannot)); - wildcard_none; - ] + if terminal then [construct_pexp (subpat, guard_opt, exp, (gen_loc l, empty_uannot))] + else + [ + construct_pexp (subpat, guard_opt, wrap_some ~return_position exp, (gen_loc l, empty_uannot)); + wildcard_arm ~return_position (); + ] in - rewrite_match_untyped is_mapping subst head_exp arms (gen_loc l, empty_uannot) + rewrite_match_untyped ~return_position is_mapping subst head_exp arms (gen_loc l, empty_uannot) in construct_pexp (pat, Some guard_exp, match_exp, (gen_loc l, empty_uannot)) -and rewrite_arms is_mapping subst msa (l, uannot) = +and rewrite_arms ~return_position is_mapping subst msa (l, uannot) = let head_exp_tmp = mk_id "head_exp#" in - let mmatch = mappings_match is_mapping subst msa.mappings msa.subst_arm in + let mmatch terminal = mappings_match ~terminal ~return_position is_mapping subst msa.mappings msa.subst_arm in let new_head_exp = - mk_exp (E_match (mk_exp (E_id head_exp_tmp), List.map some_arm msa.before_arms @ [mmatch; wildcard_none])) + mk_exp + (E_match + ( mk_exp (E_id head_exp_tmp), + List.map (some_arm ~return_position) msa.before_arms @ [mmatch false; wildcard_arm ~return_position ()] + ) + ) |> match_complete in let outer_match = - match msa.after_arms with - | [] -> - E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot)) - |> match_incomplete - | _ -> - let after_match = - rewrite_match_untyped is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms (l, uannot) - in - E_aux - ( E_match (new_head_exp, [unwrap_some; none_pexp after_match]), - (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot) - ) - |> match_complete + if return_position then ( + match msa.after_arms with + | [] -> + mk_exp + (E_match (mk_exp (E_id head_exp_tmp), List.map (some_arm ~return_position) msa.before_arms @ [mmatch true])) + |> match_incomplete + | _ -> + let after_match = + rewrite_match_untyped ~return_position is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms + (l, uannot) + in + E_aux (E_block [new_head_exp; after_match], (l, remove_completeness_attribute uannot)) + ) + else ( + match msa.after_arms with + | [] -> + E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot)) + |> match_incomplete + | _ -> + let after_match = + rewrite_match_untyped ~return_position is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms + (l, uannot) + in + E_aux + ( E_match (new_head_exp, [unwrap_some; none_pexp after_match]), + (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot) + ) + |> match_complete + ) in - mk_exp (E_let (mk_letbind (mk_pat (P_id head_exp_tmp)) msa.head_exp, outer_match)) + (* Make sure we don't generate a pointless `let head_exp# = head_exp# in ...` *) + match msa.head_exp with + | E_aux (E_id id, _) when string_of_id id = "head_exp#" -> outer_match + | _ -> mk_exp (E_let (mk_letbind (mk_pat (P_id head_exp_tmp)) msa.head_exp, outer_match)) -and rewrite_match_untyped is_mapping subst head_exp arms (l, (uannot : uannot)) = +and rewrite_match_untyped ~return_position is_mapping subst head_exp arms (l, (uannot : uannot)) = match split_arms (fun x -> x) is_mapping subst [] arms with | before_arms, Some (subst_arm, mappings, after_arms) -> - rewrite_arms is_mapping subst { head_exp; before_arms; subst_arm; mappings; after_arms } (l, uannot) + rewrite_arms ~return_position is_mapping subst + { head_exp; before_arms; subst_arm; mappings; after_arms } + (l, uannot) | _, None -> E_aux (E_match (head_exp, arms), (l, uannot)) -and rewrite_match_typed is_mapping subst head_exp arms (l, (tannot : tannot)) = +and rewrite_match_typed ~return_position is_mapping subst head_exp arms (l, (tannot : tannot)) = match split_arms map_uannot is_mapping subst [] arms with | before_arms, Some (subst_arm, mappings, after_arms) -> let rewritten_match = - rewrite_arms is_mapping subst + rewrite_arms ~return_position is_mapping subst (strip_mapping_split_arms { head_exp; before_arms; subst_arm; mappings; after_arms }) (l, untyped_annot tannot) in @@ -311,7 +376,9 @@ let rewrite_exp (aux, annot) = match aux with | E_match (head_exp, arms) -> let fresh = name_gen "mapping" in - rewrite_match_typed (fun m -> Env.is_mapping m (env_of_annot annot)) fresh head_exp arms annot + rewrite_match_typed ~return_position:false + (fun m -> Env.is_mapping m (env_of_annot annot)) + fresh head_exp arms annot | _ -> E_aux (aux, annot) let rewrite_ast ast = diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index f53727e39..ef0dc8805 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -353,6 +353,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | CT_fint n, CT_lbits -> let* x = signed_size ~into:lbits_size ~from:n x in return (Fn ("Bits", [bvint lbits_index (Big_int.of_int n); x])) + | CT_fint n, CT_fint m -> signed_size ~into:m ~from:n x | CT_lbits, CT_fbits n -> unsigned_size ~into:n ~from:lbits_size (Fn ("contents", [x])) | CT_fbits n, CT_fbits m -> unsigned_size ~into:m ~from:n x | CT_fbits n, CT_lbits -> @@ -1242,11 +1243,12 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct match (cval_ctyp v, ret_ctyp) with | CT_constant n, _ when Big_int.greater_equal n Big_int.zero -> return (bvint (int_size ret_ctyp) (Big_int.pow_int_positive 2 (Big_int.to_int n))) - | CT_lint, CT_lint -> - let* v = smt_cval v in + | ctyp, _ -> (* TODO: Check we haven't shifted too far *) - return (bvshl (bvone lint_size) v) - | _ -> builtin_type_error "pow2" [v] (Some ret_ctyp) + let sz = int_size ctyp in + let ret_sz = int_size ret_ctyp in + let* shift = bind (smt_cval v) (signed_size ~into:ret_sz ~from:sz) in + return (bvshl (bvone ret_sz) shift) let builtin_count_leading_zeros v ret_ctyp = let rec lzcnt ret_sz sz smt = @@ -1367,6 +1369,10 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct in return (Fn ("or", constructors)) | (CT_fbits _ | CT_lbits), (CT_fbits _ | CT_lbits) -> builtin_eq_bits x y + | CT_bit, CT_bit -> + let* x = smt_cval x in + let* y = smt_cval y in + return (Fn ("=", [x; y])) | (CT_constant _ | CT_fint _ | CT_lint), (CT_constant _ | CT_fint _ | CT_lint) -> builtin_eq_int x y | CT_unit, CT_unit -> return (Bool_lit true) | CT_enum _, CT_enum _ -> diff --git a/src/lib/util.ml b/src/lib/util.ml index be0138c44..554f403d1 100644 --- a/src/lib/util.ml +++ b/src/lib/util.ml @@ -347,6 +347,7 @@ let string_to_list s = module IntSet = Set.Make (Int) module IntMap = Map.Make (Int) +module StringSet = Set.Make (String) module StringMap = Map.Make (String) module IntIntSet = Set.Make (struct diff --git a/src/lib/util.mli b/src/lib/util.mli index fc479bd17..ca2951bc5 100644 --- a/src/lib/util.mli +++ b/src/lib/util.mli @@ -268,11 +268,13 @@ val string_to_list : string -> char list (** {2 Useful sets} *) -(** Sets of Integers *) +(** Sets of integers and strings *) module IntSet : Set.S with type elt = int and type t = Set.Make(Int).t module IntMap : Map.S with type key = int and type 'a t = 'a Map.Make(Int).t +module StringSet : Set.S with type elt = string and type t = Set.Make(String).t + module StringMap : Map.S with type key = string and type 'a t = 'a Map.Make(String).t module IntIntSet : Set.S with type elt = int * int diff --git a/src/lib/value.ml b/src/lib/value.ml index c06419150..e0b33c734 100644 --- a/src/lib/value.ml +++ b/src/lib/value.ml @@ -457,6 +457,8 @@ let value_undefined_vector = function | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2)) | _ -> failwith "value undefined_vector" +let value_undefined_range = function [v1; v2] -> v1 | _ -> failwith "value undefined_range" + let value_undefined_list = function [_] -> V_list [] | _ -> failwith "value undefined_list" let value_undefined_bitvector = function @@ -795,6 +797,7 @@ let primops = ("undefined_unit", fun _ -> V_unit); ("undefined_bit", fun _ -> V_bit Sail_lib.B0); ("undefined_int", fun _ -> V_int Big_int.zero); + ("undefined_range", value_undefined_range); ("undefined_nat", fun _ -> V_int Big_int.zero); ("undefined_bool", fun _ -> V_bool false); ("undefined_bitvector", value_undefined_bitvector); diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 8c7ab4eed..a083ad396 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -129,13 +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 sv_dpi_from_attr sets 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") + | AD_aux (AD_string s, _) -> Some (StringSet.mem s sets) + | AD_aux (_, l) -> raise (Reporting.err_general l "dpi field must be a boolean or string") (* The direct footprint contains information about the effects directly performed by the function itself, i.e. not those from any @@ -465,6 +466,7 @@ module type CONFIG = sig val unreachable : string list val comb : bool val ignore : string list + val dpi_sets : StringSet.t end module Make (Config : CONFIG) = struct @@ -2434,7 +2436,7 @@ module Make (Config : CONFIG) = struct 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 + match sv_dpi_from_attr Config.dpi_sets 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 -> diff --git a/src/sail_sv_backend/jib_sv.mli b/src/sail_sv_backend/jib_sv.mli index aed6f502d..a96681ba1 100644 --- a/src/sail_sv_backend/jib_sv.mli +++ b/src/sail_sv_backend/jib_sv.mli @@ -71,6 +71,7 @@ module type CONFIG = sig val unreachable : string list val comb : bool val ignore : string list + val dpi_sets : Util.StringSet.t end module Make (Config : CONFIG) : sig diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 09d0cc39e..049485316 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -60,6 +60,7 @@ open Interactive.State open Sv_optimize +module StringSet = Util.StringSet module R = Jib_sv let opt_output_dir = ref None @@ -70,6 +71,11 @@ type verilate_mode = Verilator_none | Verilator_compile | Verilator_run let opt_verilate = ref Verilator_none let opt_verilate_args = ref None +let opt_verilate_cflags = ref None +let opt_verilate_ldflags = ref None +let opt_verilate_link_sail_runtime = ref false + +let append_flag opt flag = match !opt with None -> opt := Some flag | Some flags -> opt := Some (flags ^ " " ^ flag) let opt_line_directives = ref false @@ -90,6 +96,8 @@ let opt_nomem = ref false let opt_unreachable = ref [] let opt_fun2wires = ref [] +let opt_dpi_sets = ref StringSet.empty + let opt_int_specialize = ref None let opt_disable_optimizations = ref false @@ -118,9 +126,21 @@ let verilog_options = " Invoke verilator on generated output" ); ( "-sv_verilate_args", - Arg.String (fun s -> opt_verilate_args := Some s), + Arg.String (fun s -> append_flag opt_verilate_args s), " Extra arguments to pass to verilator" ); + ( "-sv_verilate_cflags", + Arg.String (fun s -> append_flag opt_verilate_cflags s), + " Verilator CFLAGS argument" + ); + ( "-sv_verilate_ldflags", + Arg.String (fun s -> append_flag opt_verilate_ldflags s), + " Verilator LDFLAGS argument" + ); + ( "-sv_verilate_link_sail_runtime", + Arg.Set opt_verilate_link_sail_runtime, + " Link the Sail C runtime with the generated verilator C++" + ); ("-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"); @@ -151,6 +171,10 @@ let verilog_options = " Run n specialization passes on Sail Int-kinded type variables" ); ("-sv_disable_optimizations", Arg.Set opt_disable_optimizations, " disable SystemVerilog specific optimizations"); + ( "-sv_dpi", + Arg.String (fun s -> opt_dpi_sets := StringSet.add s !opt_dpi_sets), + " Use SystemVerilog DPI-C for a set of primitives (e.g. memory)" + ); ] let verilog_rewrites = @@ -336,19 +360,38 @@ let wrap_module pre mod_name ins_outs doc = ^^ hardline ^^ string "endmodule" ^^ hardline let verilator_cpp_wrapper name = - [ - sprintf "#include \"V%s.h\"" name; - "#include \"verilated.h\""; - "int main(int argc, char** argv) {"; - " VerilatedContext* contextp = new VerilatedContext;"; - " contextp->commandArgs(argc, argv);"; - sprintf " V%s* top = new V%s{contextp};" name name; - " while (!contextp->gotFinish()) { top -> eval(); }"; - " delete top;"; - " delete contextp;"; - " return 0;"; - "}"; - ] + if not !opt_verilate_link_sail_runtime then + [ + sprintf "#include \"V%s.h\"" name; + "#include \"verilated.h\""; + "int main(int argc, char** argv) {"; + " VerilatedContext* contextp = new VerilatedContext;"; + " contextp->commandArgs(argc, argv);"; + sprintf " V%s* top = new V%s{contextp};" name name; + " while (!contextp->gotFinish()) { top -> eval(); }"; + " delete top;"; + " delete contextp;"; + " return 0;"; + "}"; + ] + else + [ + sprintf "#include \"V%s.h\"" name; + "#include \"verilated.h\""; + "#include \"rts.h\""; + "int main(int argc, char** argv) {"; + " VerilatedContext* contextp = new VerilatedContext;"; + (* " contextp->commandArgs(argc, argv);"; *) + " setup_rts();"; + " process_arguments(argc, argv);"; + sprintf " V%s* top = new V%s{contextp};" name name; + " while (!contextp->gotFinish()) { top -> eval(); }"; + " cleanup_rts();"; + " delete top;"; + " delete contextp;"; + " return 0;"; + "}"; + ] (* let make_genlib_file filename = @@ -389,6 +432,7 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = let unreachable = !opt_unreachable let comb = !opt_comb let ignore = !opt_fun2wires + let dpi_sets = !opt_dpi_sets end) in let open SV in let sail_dir = Reporting.get_sail_dir default_sail_dir in @@ -410,6 +454,9 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = let include_doc = (if !opt_nostrings then string "`define SAIL_NOSTRINGS" ^^ hardline else empty) + ^^ List.fold_left + (fun doc set -> ksprintf string "SAIL_DPI_%s" (String.uppercase_ascii set) ^^ hardline) + empty (StringSet.elements !opt_dpi_sets) ^^ string "`include \"sail.sv\"" ^^ hardline ^^ ksprintf string "`include \"sail_genlib_%s.sv\"" out ^^ (if !opt_nomem then empty else hardline ^^ string "`include \"sail_memory.sv\"") @@ -453,7 +500,12 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = let doc = let base = Generate_primop2.basic_defs !opt_max_unknown_bitvector_width !opt_max_unknown_integer_width in let reg_ref_enums, reg_ref_functions = sv_register_references spec_info in - string base ^^ string "`include \"sail_modules.sv\"" ^^ twice hardline + Util.fold_left_last + (fun last doc set -> + ksprintf string "`define SAIL_DPI_%s" (String.uppercase_ascii set) ^^ if last then twice hardline else hardline + ) + empty (StringSet.elements !opt_dpi_sets) + ^^ string base ^^ string "`include \"sail_modules.sv\"" ^^ twice hardline ^^ separate_map (twice hardline) (pp_def None) svir_types ^^ twice hardline ^^ reg_ref_enums ^^ reg_ref_functions ^^ separate_map (twice hardline) (pp_def None) svir @@ -614,14 +666,16 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = Util.close_output_with_check file_info; let extra = match !opt_verilate_args with None -> "" | Some args -> " " ^ args in + let cflags = match !opt_verilate_cflags with None -> "" | Some args -> sprintf " -CFLAGS \"%s\"" args in + let ldflags = match !opt_verilate_ldflags with None -> "" | Some args -> sprintf " -LDFLAGS \"%s\"" 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%s" - sail_sv_libdir out out out extra + "verilator --cc --exe --build -j 0 --top-module sail_toplevel -I%s --Mdir %s_obj_dir sim_%s.cpp %s.sv%s%s%s" + sail_sv_libdir out out out extra cflags ldflags in print_endline ("Verilator command: " ^ verilator_command); let _ = Unix.system verilator_command in diff --git a/test/c/pow2_var.expect b/test/c/pow2_var.expect new file mode 100644 index 000000000..d6de668a8 --- /dev/null +++ b/test/c/pow2_var.expect @@ -0,0 +1,4 @@ +x = 1 +y = 2 +z = 8 +w = 16 diff --git a/test/c/pow2_var.sail b/test/c/pow2_var.sail new file mode 100644 index 000000000..afe6c6501 --- /dev/null +++ b/test/c/pow2_var.sail @@ -0,0 +1,23 @@ +default Order dec + +$include + +register R : int + +register T : range(0, 5) + +val main : unit -> unit + +$[jib_debug] +function main() = { + let x = 2 ^ 0; + let y = 2 ^ 1; + R = 3; + let z = 2 ^ R; + T = 4; + let w = 2 ^ T; + print_int("x = ", x); + print_int("y = ", y); + print_int("z = ", z); + print_int("w = ", w); +}