SVA assertions for Anvil-SV interfaces by Hotaru71 · Pull Request #86 · AnvilHDL/anvil

Hotaru71 · 2026-04-03T11:30:13Z

Add sv_extern_mode option to config for verification routing
Update compileDriver with verification_run and make_config
Update main.ml to route to verification path when -sv-extern is passed
Add assertName module for verification naming
Update codegen and codegenPort with verification codegen functions
Add one example called extern_example1_sender.anvil

arj4web · 2026-04-04T02:39:45Z

@Hotaru71, I assume #80 is obsolete now?

arj4web · 2026-04-04T02:44:44Z

@Hotaru71, please list down the properties for which assertions are added. Thanks.

arj4web · 2026-04-04T02:46:24Z

Dont add the generated sv files to commit

Copilot

Pull request overview

This PR introduces a new “verification mode” compilation path (triggered via -sv-extern) that generates verification-oriented SystemVerilog (assertion wrappers), along with supporting naming/helpers and an example.

Changes:

Added sv_extern_mode to the compiler config / CLI parsing and routed main into a new verification driver path.
Added CompileDriver.verification_run + verification codegen entrypoints (Codegen.verification_generate*), plus port helper utilities for verification.
Added an AssertName helper module and a new extern sender example.

Reviewed changes

Copilot reviewed 12 out of 13 changed files in this pull request and generated 11 comments.

Show a summary per file

File	Description
lib/config.mli	Extends `compile_config` with `sv_extern_mode`.
lib/config.ml	Parses `-sv-extern` and stores `sv_extern_mode` in config.
bin/main.ml	Routes to verification mode when `sv_extern_mode` is set.
lib/compileDriver.mli	Exposes `verification_run` API.
lib/compileDriver.ml	Adds verification compilation pipeline and config builder.
lib/codegenPort.mli	Adds verification port formatting/name utilities.
lib/codegenPort.ml	Implements verification port formatting/name utilities.
lib/codegen.mli	Exposes verification codegen entrypoints.
lib/codegen.ml	Implements verification SV generation (assertion wrappers, includes, instantiations).
lib/assertName.mli	New module API for verification naming.
lib/assertName.ml	New module implementation for verification naming.
examples/extern_example1_sender.anvil	Adds a new extern/verification-related example input.
examples/extern_example1_sender.anvil.sv	Adds the corresponding generated SV example artifact.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-04T02:47:17Z

+          match msg_def.sig_types with
+          | [] -> Printf.printf "parameter int N = #;\n"
+          | stype0 :: _ ->
+            match number_of_lifetime_cycles stype0.lifetime.e with
+            | Some n -> Printf.printf "parameter int N = %d;\n" n 
+            | None -> Printf.printf "parameter int N = #;\n"
+      else ()
+    in 


The lifetime-bound emission uses Printf.printf (stdout) and prints placeholder text like "parameter int N = #;", which won’t end up in the generated verification SystemVerilog and also produces invalid SV when lifetime cycles aren’t Cycles n. This should be emitted via CodegenPrinter/Out_channel (and avoid generating invalid syntax; e.g., skip the parameter or raise a compile error when the bound can’t be determined).

Suggested change

match msg_def.sig_types with

| [] -> Printf.printf "parameter int N = #;\n"

| stype0 :: _ ->

match number_of_lifetime_cycles stype0.lifetime.e with

| Some n -> Printf.printf "parameter int N = %d;\n" n

| None -> Printf.printf "parameter int N = #;\n"

else ()

in

match msg_def.sig_types with

| [] ->

failwith

(Printf.sprintf

"Cannot emit lifetime bound parameter for endpoint %s: message has no signal types."

ep.name)

| stype0 :: _ ->

match number_of_lifetime_cycles stype0.lifetime.e with

| Some n ->

CodegenPrinter.print_line printer

(Printf.sprintf "parameter int N = %d;" n)

| None ->

failwith

(Printf.sprintf

"Cannot emit lifetime bound parameter for endpoint %s: lifetime bound is not statically determinable."

ep.name)

else ()

in

Copilot · 2026-04-04T02:47:17Z

+      | (_, Dynamic) -> "typedef enum logic [1:0] {WAIT_ACK, DROP_ACK} state_t;"
+      | (Dynamic, _) -> "typedef enum logic [1:0] {WAIT_REQ, DROP_VALID} state_t;"
+      | _ -> "None"


Returning the literal string "None" for unsupported sync combinations will be printed into the generated SystemVerilog (via print_declaration_FSM), which will break compilation. Consider returning an empty string and skipping printing, or raising an error for unsupported combinations instead of emitting "None".

Copilot · 2026-04-04T02:47:17Z

+    (
+      match g.extern_module, g.proc_body with
+      | _ ->
+        let initEvents = fst @@ List.hd g.threads in
+        codegen_endpoints printer graphs initEvents;
+    );
+
+    (* Retreive the user module name *)
+    let s = AssertName.user_sv () in
+    (* Print user module instantiation *)
+    Printf.sprintf "%s user_sv (" s |> CodegenPrinter.print_line printer;
+    let _ = verification_codegen_instantiations printer graphs g.messages.args in
+    (
+      match g.extern_module, g.proc_body with
+      | _ ->
+        let initEvents = fst @@ List.hd g.threads in
+        codegen_endpoints printer graphs initEvents;
+    );


codegen_endpoints is called after verification_codegen_ports already emitted declarations, and it’s invoked multiple times (before user instantiation, before anvil instantiation, etc.). Since codegen_endpoints prints signal declarations, this will cause duplicate declarations in the generated SV. Consider removing these calls or refactoring to emit endpoint declarations exactly once (and emit only connections inside instantiations).

Suggested change

(

match g.extern_module, g.proc_body with

| _ ->

let initEvents = fst @@ List.hd g.threads in

codegen_endpoints printer graphs initEvents;

);

(* Retreive the user module name *)

let s = AssertName.user_sv () in

(* Print user module instantiation *)

Printf.sprintf "%s user_sv (" s |> CodegenPrinter.print_line printer;

let _ = verification_codegen_instantiations printer graphs g.messages.args in

(

match g.extern_module, g.proc_body with

| _ ->

let initEvents = fst @@ List.hd g.threads in

codegen_endpoints printer graphs initEvents;

);

(* Retreive the user module name *)

let s = AssertName.user_sv () in

(* Print user module instantiation *)

Printf.sprintf "%s user_sv (" s |> CodegenPrinter.print_line printer;

let _ = verification_codegen_instantiations printer graphs g.messages.args in

Copilot · 2026-04-04T02:47:17Z

+          String.concat "\n" [
+            Printf.sprintf "`include \"nosyn_user_sender.svh\"\n";
+            Printf.sprintf "assert property (data_stable_valid_high(%s, state_curr, %s))" valid_name data;


The generated verification SV includes `include directives for .svh files (e.g. nosyn_user_sender.svh) that don’t exist anywhere in this repository. Unless these files are generated/installed elsewhere, the verification output will not compile; consider adding them to the repo or documenting/embedding these properties so the output is self-contained.

Copilot · 2026-04-04T02:47:17Z

+            Printf.sprintf "assert property (valid_low_during_DROP_VALID (state_curr, %s)" valid_name;
+            Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n";


In the (Dynamic, _) / Left case, the generated assertion string is syntactically incomplete (missing closing parenthesis / terminator on the valid_low_during_DROP_VALID property), which will produce invalid SystemVerilog. Also the subsequent $error message references the wrong assertion name. Please fix the emitted assertion line so it’s valid SV and the error label matches the property.

Suggested change

Printf.sprintf "assert property (valid_low_during_DROP_VALID (state_curr, %s)" valid_name;

Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n";

Printf.sprintf "assert property (valid_low_during_DROP_VALID (state_curr, %s))" valid_name;

Printf.sprintf "else $error(\"Assertion Failed: valid_low_during_DROP_VALID\");\n";

Copilot · 2026-04-04T02:47:18Z

+let verification_compile out config =
+  let open Config in
+  let toplevel_filename = List.hd config.input_filenames in
+  let cunits = ref [] in


verification_compile doesn’t mirror the normal compile path’s behavior: it ignores config.just_check and does not emit the standard SV preamble (Codegen.generate_preamble). If verification output is meant to be compiled/simulated similarly, consider reusing the same preamble + just_check gating so behavior is consistent across modes.

Copilot · 2026-04-04T02:47:18Z

+  | anvil_file :: gen_sv_file :: user_sv_file :: _ ->
+    AssertName.generate gen_sv_file user_sv_file;
+    let c = make_config anvil_file in
+    (try verification_compile stdout c
+    with


verification_run rebuilds a fresh config via make_config, which drops user-specified flags from the original CLI config (e.g., -verbose, -disable-lt-checks, -O, -two-round, etc.) and also ignores sv_extern_mode’s value entirely. Consider deriving the verification config from the passed-in config (overriding only input_filenames/output handling) so verification behaves consistently with normal compilation and the mode value is actually used.

Copilot · 2026-04-04T02:47:18Z

+      ("-json", Arg.Set json_output, "Output compilation results in JSON format");
+      ("-sv-extern", Arg.Set_string sv_extern_mode, "SV extern mode: extern (default), anvil, all, none")
    ]
    add_input_filename
    "anvil [-stdin] [-verbose] [-disable-lt-checks] [-O <opt-level>] [-two-round] [-json] [-strict-dtc] <file1> [<file2>] ...";


The -sv-extern flag is parsed as a required string argument and documented as having a default of "extern", but the actual default is the empty string and the value is only used as a boolean trigger. Also the Arg.parse usage string printed on -help does not mention -sv-extern. Consider either (a) making -sv-extern a boolean flag if it only enables verification routing, or (b) validating/using the mode string (Arg.Symbol / custom parser) and updating the help/usage text accordingly.

Copilot · 2026-04-04T02:47:18Z

+let user_sv () : string =
+  match !user_sv_ref with
+  | Some s -> strip_sv_name s
+  | None -> failwith "AssertName.sender: not initialised (call AssertName.generate first)"


The failure message references AssertName.sender even though the function is user_sv; this makes debugging initialization failures confusing. Consider updating the message to match the function/module names and be consistent with the other error strings.

Suggested change

| None -> failwith "AssertName.sender: not initialised (call AssertName.generate first)"

| None -> failwith "AssertName.user_sv: not initialised (call AssertName.generate first)"

Copilot · 2026-04-04T02:47:19Z

+  | Some s -> s
+  | None -> failwith "AssertName.receiver: not initialised (call AssertName.generate first)"


anvil_sv currently returns the stored string unchanged (likely a file path), unlike user_sv which strips to a basename without extension. If anvil_sv is intended to be used as a SystemVerilog module identifier, it should probably apply strip_sv_name as well. Also the failure message references AssertName.receiver, which doesn’t match the function name.

Suggested change

| Some s -> s

| None -> failwith "AssertName.receiver: not initialised (call AssertName.generate first)"

| Some s -> strip_sv_name s

| None -> failwith "AssertName.anvil_sv: not initialised (call AssertName.generate first)"

Hotaru71 · 2026-04-04T13:19:26Z

@Hotaru71, I assume #80 is obsolete now?

Yes #80 is obsolete now.

arj4web · 2026-04-05T01:37:46Z

@Hotaru71 seems like this is a WIP. Copilot flagged some functional correctness issues ? You can take a look and fix them if they are correct. Once done, I can review in detail.

Hotaru71 · 2026-04-09T17:58:45Z

@Hotaru71, please list down the properties for which assertions are added. Thanks.

The following assertion properties have been added:

ack_low_when_valid_high: Ensures that acknowledgment is not asserted when valid is raised.
ack_low_after_handshake: Deassert acknowledgment signal after handshake.
data_stable_valid_high: Ensures that data remains stable while waiting for the acknowledgment signal.
valid_high_until_ack_high: acknowledgment: Ensures that valid remains asserted until acknowledgment is received.
ack_high_valid_low: Ensures that valid is deasserted after acknowledgment is observed.
data_stable_N_cycles_after_ack_high: Ensures that data remains stable for N cycles after acknowledgment, where N is defined by the lifetime contract.
wait_req_ack_low: Ensures that valid stays asserted when acknowledgment is still low.
ack_low_during_DROP_ACK: Ensures that acknowledgment remains low during the drop-ack phase.
data_stable_N_cycles: Ensures that data remains stable for N cycles after acknowledgment, where N is defined by the lifetime contract.
valid_low_during_DROP_VALID: Ensures that valid remains low during the drop-valid phase.

arj4web · 2026-04-10T02:18:42Z

u can seperate the added code for wrapper generation in different module

arj4web · 2026-04-10T02:19:28Z


 (** Generate code for a {!type:EventGraph.event_graph_collection} to a specified output channel. *)
 val generate : out_channel -> Config.compile_config -> EventGraph.event_graph_collection -> unit
+


Specifically these 3

arj4web · 2026-04-10T02:22:51Z

arj4web · 2026-04-10T02:25:23Z

@Hotaru71, please list down the properties for which assertions are added. Thanks.

The following assertion properties have been added:

ack_low_when_valid_high: Ensures that acknowledgment is not asserted when valid is raised.

ack_low_after_handshake: Deassert acknowledgment signal after handshake.

data_stable_valid_high: Ensures that data remains stable while waiting for the acknowledgment signal.

valid_high_until_ack_high: acknowledgment: Ensures that valid remains asserted until acknowledgment is received.

ack_high_valid_low: Ensures that valid is deasserted after acknowledgment is observed.

data_stable_N_cycles_after_ack_high: Ensures that data remains stable for N cycles after acknowledgment, where N is defined by the lifetime contract.

wait_req_ack_low: Ensures that valid stays asserted when acknowledgment is still low.

ack_low_during_DROP_ACK: Ensures that acknowledgment remains low during the drop-ack phase.

data_stable_N_cycles: Ensures that data remains stable for N cycles after acknowledgment, where N is defined by the lifetime contract.

valid_low_during_DROP_VALID: Ensures that valid remains low during the drop-valid phase.

Can u please add these in a markdown file as a readme in properties (lib) directory (where u have assertions)

Also add more test cases in that case ? I see only one

Copilot

Pull request overview

Copilot reviewed 17 out of 18 changed files in this pull request and generated 5 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-10T02:29:33Z

+  match List.rev config.input_filenames with
+  | anvil_file :: gen_sv_file :: user_sv_file :: _ ->
+    AssertName.generate gen_sv_file user_sv_file;
+    let c = { config with
+      input_filenames = [anvil_file];
+      output_filename = None;
+    } in


verification_run requires three input files per the error message, but gen_sv_file is only used to initialise AssertName.anvil_sv_ref (and AssertName.anvil_sv() isn’t referenced anywhere in the verification codegen). As written, the second argument has no functional effect and the tool still prints verification output to stdout, so requiring it is misleading. Either use gen_sv_file as an actual output path (write generated SV there) or drop it from the required inputs / error message.

Copilot · 2026-04-10T02:29:34Z

+        function
+        | Text msg_text -> Printf.eprintf "%s\n" msg_text
+        | Codespan (file_name, span) -> (
+          let file_name = Option.get file_name in
+          Printf.eprintf "%s:%d:%d:\n" file_name span.st.pos_lnum (span.st.pos_cnum - span.st.pos_bol);
+        )


This error-printing path does Option.get file_name for Codespan fragments, but Codespan explicitly allows filename to be None (e.g. Except.codespan_local). If a compile error includes a Codespan (None, ...), this will raise and mask the real compilation error. Handle the None case (print span without filename, or skip the location line) instead of using Option.get.

Copilot · 2026-04-10T02:29:34Z

+    List.concat_map (fun (msg : message_def) ->
+      let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in
+      List.mapi (fun i (_stype : sig_type_chan_local) ->
+        CodegenFormat.format_msg_data_signal_name endpoint.name msg.name i
+      ) msg.sig_types
+    ) cc.messages


data_port_names currently generates a data signal name for every msg.sig_types entry, even when the corresponding signal type is unit. Those unit-typed signals are not emitted as ports elsewhere (e.g. gather_ports_from_endpoint skips unit_dtype), so this can produce names for signals that do not exist and break the generated verification SV. Filter out unit-typed signal types (or reuse message_has_data_port / gather_ports ordering) when building data_port_names.

Copilot · 2026-04-10T02:29:34Z

+  (* The list of signals, later use for indexing *)
+  let valid_names = CodegenPort.valid_port_names graphs.channel_classes g.messages.args in
+  let ack_names = CodegenPort.ack_port_names graphs.channel_classes g.messages.args in
+  let data_names = CodegenPort.data_port_names graphs.channel_classes g.messages.args in
+


The valid_names / ack_names lists are built by filtering messages by whether they have a valid/ack port, but later they’re indexed by count which ranges over all messages (total_count). If a channel class mixes sync modes across messages, indexing will misalign (or fall back to ""), generating invalid SV (e.g. if ()) or referencing the wrong signal. Build a per-message mapping (e.g. by iterating messages with their original indices and producing string option slots) so count always maps to the correct valid/ack/data signal names for that specific message.

Copilot · 2026-04-10T02:29:34Z

+property data_stable_N_cycles_after_ack_high (current_state, counter_0, data);
+    @(posedge clk_i) ((current_state==DROP_VALID || counter_0!=0) |-> (_endp_res_0 == $past(data)));
+endproperty


This property references _endp_res_0, which is not declared anywhere in the property arguments or in the generated wrapper modules, so the included SVH will not compile. It looks like this should reference the data argument (or data_0) consistently instead of _endp_res_0.

Copilot

Pull request overview

Copilot reviewed 24 out of 25 changed files in this pull request and generated 12 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-18T00:54:32Z

+  CodegenPrinter.print_line printer ".clk_i(clk_i),";
+  CodegenPrinter.print_line printer ".rst_ni(rst_ni),";
+  let rec print_port_list port_list =
+  match port_list with
+  | [] -> ()
+  | port :: [] ->
+    let s = CodegenPort.instanformat port in 
+    Printf.sprintf ".%s (%s)" s s |> CodegenPrinter.print_line printer
+  | port :: port_list' ->
+    let s = CodegenPort.instanformat port in 
+    Printf.sprintf ".%s (%s)," s s |> CodegenPrinter.print_line printer;
+    print_port_list port_list'
+  in
+  print_port_list port_list;


verification_codegen_instantiations always prints .clk_i(...), and .rst_ni(...), with trailing commas. If port_list is empty (e.g. a proc has no non-unit message ports and no dynamic sync ports), the generated instance will end with a dangling comma before );, which is invalid SystemVerilog. Handle the empty list case by omitting the trailing comma(s) or by printing the last connection without a comma.

Suggested change

CodegenPrinter.print_line printer ".clk_i(clk_i),";

CodegenPrinter.print_line printer ".rst_ni(rst_ni),";

let rec print_port_list port_list =

match port_list with

| [] -> ()

| port :: [] ->

let s = CodegenPort.instanformat port in

Printf.sprintf ".%s (%s)" s s |> CodegenPrinter.print_line printer

| port :: port_list' ->

let s = CodegenPort.instanformat port in

Printf.sprintf ".%s (%s)," s s |> CodegenPrinter.print_line printer;

print_port_list port_list'

in

print_port_list port_list;

let connections =

[

".clk_i(clk_i)";

".rst_ni(rst_ni)";

] @ List.map (fun port ->

let s = CodegenPort.instanformat port in

Printf.sprintf ".%s (%s)" s s

) port_list

in

let rec print_connections connections =

match connections with

| [] -> ()

| [connection] ->

CodegenPrinter.print_line printer connection

| connection :: connections' ->

CodegenPrinter.print_line printer (connection ^ ",");

print_connections connections'

in

print_connections connections;

Copilot · 2026-04-18T00:54:33Z

+property data_stable_valid_high (valid, current_state, data);
+    @(posedge clk_i) ((valid && !$rose(valid)) && (current_state inside {WAIT_REQ, WAIT_ACK})) |-> data == $past(data);
+endproperty 


These properties use $past(...) without any reset gating. On the first sampled clock edge (and during/just after reset), $past and state/data signals can be X, which can cause spurious assertion failures in simulators/formal tools. Consider adding disable iff (!rst_ni) to the property clocking event (or otherwise guarding against reset/first-cycle sampling).

Copilot · 2026-04-18T00:54:33Z

@@ -0,0 +1,3 @@
+property data_stable_N_cycles (state_curr_0, counter_0, data_0);
+    @(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));


These properties use $past(...) without any reset gating, which can cause X-propagation/spurious failures around reset or the first sampled edge. Consider adding disable iff (!rst_ni) (or an equivalent guard) to the property clocking event.

Suggested change

@(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));

@(posedge clk_i) disable iff (!rst_ni) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));

Copilot · 2026-04-18T00:54:33Z

+## Examples
+
+You can try the assertion flow using the provided example designs in the `examples` directory. There are 6 examples, with filenames in the format:
+
+- `extern_exampleN_sender.anvil` / `extern_exampleN_receiver.sv`
+- or `extern_exampleN_receiver.anvil` / `extern_exampleN_sender.sv`
+


The PR description says it "Add[s] one example", but this change adds multiple extern_example* files (and the README documents 6 examples). Please update the PR description (or the README) so they agree on how many examples are included.

Copilot · 2026-04-18T00:54:33Z

+      ("-json", Arg.Set json_output, "Output compilation results in JSON format");
+      ("-sv-extern", Arg.Set_string sv_extern_mode, "SV extern mode: extern")
    ]
    add_input_filename
-    "anvil [-stdin] [-verbose] [-disable-lt-checks] [-O <opt-level>] [-two-round] [-json] [-strict-dtc] <file1> [<file2>] ...";
+    "anvil [-stdin] [-verbose] [-disable-lt-checks] [-O <opt-level>] [-two-round] [-json] [-strict-dtc] [-sv-extern] <file1> [<file2>] ...";


The help/usage string lists [-sv-extern] as if it takes no argument, but the flag is defined with Arg.Set_string so it requires a mode argument (e.g. -sv-extern extern). Update the usage string (and ideally the flag help text) to reflect the required <mode> parameter to avoid confusing CLI users.

Copilot · 2026-04-18T00:54:34Z

@@ -0,0 +1,3 @@
+property data_stable_N_cycles (state_curr_0, counter_0, data_0);
+    @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));


These properties use $past(...) without any reset gating. On the first sampled clock edge (and during/just after reset), $past and state/data signals can be X, which can cause spurious assertion failures. Consider adding disable iff (!rst_ni) (or an equivalent guard) to the property clocking event.

Suggested change

@(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));

@(posedge clk_i) disable iff (!rst_ni) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));

Copilot · 2026-04-18T00:54:34Z

+endproperty
+
+property data_stable_N_cycles (state_curr_0, counter_0, data_0);
+    @(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));


These properties use $past(...) without any reset gating, which can cause X-propagation/spurious failures around reset or the first sampled edge. Consider adding disable iff (!rst_ni) (or an equivalent guard) to the property clocking event.

Suggested change

@(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));

@(posedge clk_i) disable iff (!rst_ni) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0)));

Copilot · 2026-04-18T00:54:35Z

+    @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));
+endproperty 
+
+property valid_low_during_DROP_VALID (state_curr_0, valid_0);
+    @(posedge clk_i) (state_curr_0==DROP_VALID) |-> !valid_0;


These properties use $past(...) without any reset gating, which can cause X-propagation/spurious failures around reset or the first sampled edge. Consider adding disable iff (!rst_ni) (or an equivalent guard) to the property clocking event.

Suggested change

@(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));

endproperty

property valid_low_during_DROP_VALID (state_curr_0, valid_0);

@(posedge clk_i) (state_curr_0==DROP_VALID) |-> !valid_0;

@(posedge clk_i) disable iff (!rst_ni) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0)));

endproperty

property valid_low_during_DROP_VALID (state_curr_0, valid_0);

@(posedge clk_i) disable iff (!rst_ni) (state_curr_0==DROP_VALID) |-> !valid_0;

Copilot · 2026-04-18T00:54:35Z


  json_output : bool; (** output compilation results in JSON format *)
  input_filenames : string list; (** list of file names to be compiled *)
+  sv_extern_mode: string;


sv_extern_mode is added to compile_config without any interface comment explaining expected values (it looks like only "extern" is supported). Please add a short doc comment like the other fields so downstream consumers know how to use it.

Suggested change

sv_extern_mode: string;

sv_extern_mode: string; (** SystemVerilog extern handling mode; use "extern" to enable it *)

Copilot · 2026-04-18T00:54:35Z

+    (try verification_compile stdout c
+    with
+    | CompileError msg ->
+      let open Except in
+      Printf.eprintf "Verification compilation failed!\n";
+      List.iter (
+        function
+        | Text msg_text -> Printf.eprintf "%s\n" msg_text
+        | Codespan (file_name, span) ->
+          let line = span.st.pos_lnum in
+          let col = span.st.pos_cnum - span.st.pos_bol in
+          match file_name with
+          | Some file_name ->
+              Printf.eprintf "%s:%d:%d:\n" file_name line col
+          | None ->
+              Printf.eprintf "<unknown>:%d:%d:\n" line col
+      ) msg;
+      exit 1)
+  | _ ->
+    Printf.eprintf "Error: -sv-extern requires two input files: <anvil-file> <user-sv-file>\n";
+    exit 1


verification_run calls exit 1 on error. Since this lives in the library (lib/), exiting the process makes the function hard to reuse and is inconsistent with compile, which raises CompileError and lets bin/main.ml decide how to exit. Prefer returning/raising an error (e.g. CompileError) and handling printing + exit in main.ml.

Suggested change

(try verification_compile stdout c

with

| CompileError msg ->

let open Except in

Printf.eprintf "Verification compilation failed!\n";

List.iter (

function

| Text msg_text -> Printf.eprintf "%s\n" msg_text

| Codespan (file_name, span) ->

let line = span.st.pos_lnum in

let col = span.st.pos_cnum - span.st.pos_bol in

match file_name with

| Some file_name ->

Printf.eprintf "%s:%d:%d:\n" file_name line col

| None ->

Printf.eprintf "<unknown>:%d:%d:\n" line col

) msg;

exit 1)

| _ ->

Printf.eprintf "Error: -sv-extern requires two input files: <anvil-file> <user-sv-file>\n";

exit 1

verification_compile stdout c

| _ ->

raise_compile_error None

[Except.Text "Error: -sv-extern requires two input files: <anvil-file> <user-sv-file>"]

Hotaru71

fixed SV instantiation printing to avoid dangling commas on empty port lists
cleaned up line-oriented codegen to avoid embedded newlines in print_line calls
updated assertion block emission to print multi-line output correctly
changed verification_run to raise compile errors instead of exiting in lib code
added synchronized rst_assert_ni signal for assertion reset gating
made valid/ack signal lookup conditional so missing handshake signals only fail when actually required
added extern verification examples and README updates

arj4web

These are some of the listed issues :

The example directory is incomplete.
Documentation for properties should be made clearer. Based on my interpretation of the SVA properties, I found errors in the handshake-related properties.
The properties are incorrect with regard to the handshake protocol that Anvil follows.
How interfacing works in general is unclear to me because the shadow state is instantiated statically. You can clear that in the doc if that's the assumption.
The compiled driver code uses a lot of duplicate and unnecessarily complicated logic. If the goal of the PR is to provide assertions for handshakes, this can be done by adding calls to the assertion-generation code during the normal flow when the configuration is enabled. Note that extern modules can be imported in Anvil, which means u have access to the SV files they import. The current PR takes a decoupled approach, where the user is expected to interface the Anvil code with SV.

These are some major issues that need attention before merging this PR.

arj4web · 2026-04-19T04:28:57Z

  two_round_graph: bool;
  json_output: bool;
  input_filenames: string list;
+  sv_extern_mode: string;


This should be a bool flag, why do u need string

arj4web · 2026-04-19T04:30:24Z

 let () =
  let config = Anvil.Config.parse_args() in
-  if config.json_output then
+  if config.sv_extern_mode = "extern" then


You do not need to run a seperate instance of compiler right ? You can make it generally a flag so that when extern module is added in compilation we generate assertions then

arj4web · 2026-04-19T04:32:59Z

+    left res : (logic[8]@#3)
+}
+
+proc extern_example2_receiver (endp : left ch) {


I dont understand any of these examples. Are they intended to be interfaced with other modules ? If yes do i need to provide them ? can u add a README on these examples so i can understand their purpose and how to run them ?

arj4web · 2026-04-19T04:33:49Z


+MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
+PROPERTIES_DIR ?= $(abspath $(MAKEFILE_DIR)/../extern_properties)
+assert:


It seems like the user is expected to provide the SV module and the test bench ?

arj4web · 2026-04-19T04:36:55Z

+
+```bash
+make MODULE_NAME=extern_example1_sender
+make assert MODULE_NAME=extern_example1_sender USER_SV_MODULE=extern_example1_receiver


make assert MODULE_NAME=extern_example1_sender USER_SV_MODULE=extern_example1_receiver 0 [12:35:26] dune exec anvil -- -sv-extern extern extern_example1_sender.anvil extern_example1_receiver.sv > extern_example1_receiver_assert.sv Entering directory '/home/aditya/Workspace/anvil' Leaving directory '/home/aditya/Workspace/anvil' verilator -Wall --binary --exe --assert --trace --build \ -I/home/aditya/Workspace/anvil/extern_properties --timing \ --top-module extern_example1_receiver_assert \ extern_example1_receiver.sv extern_example1_sender.anvil.sv extern_example1_receiver_assert.sv \ -o sim.out \ -Wno-UNDRIVEN -Wno-UNUSED %Error: Cannot find file containing module: 'extern_example1_receiver.sv' ... See the manual at https://verilator.org/verilator_doc.html?v=5.036 for more assistance. ... Looked in: /home/aditya/Workspace/anvil/extern_properties/extern_example1_receiver.sv /home/aditya/Workspace/anvil/extern_properties/extern_example1_receiver.sv.v /home/aditya/Workspace/anvil/extern_properties/extern_example1_receiver.sv.sv extern_example1_receiver.sv extern_example1_receiver.sv.v extern_example1_receiver.sv.sv obj_dir/extern_example1_receiver.sv obj_dir/extern_example1_receiver.sv.v obj_dir/extern_example1_receiver.sv.sv %Error: Exiting due to 1 error(s) make: *** [Makefile:51: assert] Error 1

Seems like the files in examples are missing ?

arj4web · 2026-04-19T04:40:19Z

+### Handshake Behavior
+
+#### `ack_low_when_valid_high`
+Ensures that the acknowledgment (`ack`) signal is not asserted at the moment the valid signal is raised.


This is incorrect, ack signal is asserted when valid is asserted. Once they are both high the handshake is completed. This is AXI style of handshake : https://fpgacpu.ca/fpga/handshake.html (valid ready handshake)

arj4web · 2026-04-19T04:48:28Z

+endproperty 
+
+property valid_high_until_ack_high (valid, current_state, ack);
+    @(posedge clk_i) ((valid || $rose(valid)) && (current_state inside {WAIT_REQ, WAIT_ACK}) && !ack |=> valid);


Similarly this is incorrect, because the valid signal remains asserted when the ack is high. The handshake completes when both are high.

My hunch is that the 2 properties together may also cause combinational loop.

arj4web · 2026-04-19T05:00:44Z

       {graphs with EventGraph.external_event_graphs = all_event_graphs}) all_collections
  end

+let verification_compile out config =


This function seems like a copy of the orignal one. Please just merge it into the orignal one with the config dictating what compile path to take

arj4web · 2026-04-19T05:05:35Z

+  | anvil_file :: user_sv_file :: _ ->
+      ExternName.generate user_sv_file;
+      let c = {
+        config with
+        input_filenames = [anvil_file];
+        output_filename = None;
+      } in
+      verification_compile stdout c


extern files are kept in extern imports already. Why do we need to pass it as a parameter again

Same goes for all other compile driver logic. You can just configure it in during the extern component compilation.

arj4web · 2026-04-19T05:16:55Z

+        | Right -> 
+          let valid_name = require_valid () in
+          let ack_name = require_ack () in
+          let block = ff_block "WAIT_ACK" "DROP_VALID" in


Does this make the assumption that these are the only named states for handshake logic ?

jasonyu1996 · 2026-08-22T00:32:42Z

I'm gonna take a look this weekend. Thanks!

jasonyu1996

Two issues I'd like to see addressed:

Remove the duplicate code and integrate the feature into the existing code instead
Fix the test cases

jasonyu1996 · 2026-08-23T22:55:45Z

Seems like these tests do not work due to missing files (extern_memory_subsystem_sources.sv)?

jasonyu1996 · 2026-08-23T22:56:20Z

+Received DRAM read data: 16045690981097406530
+Received CPU config command:   165
+Received AXI request:  268435520
+- /home/daoen/anvil_newest/anvil_verification_clean/examples/extern_combined_messages_ultimate_wrapper.sv:48: Verilog $finish


This definitely shouldn't be here

jasonyu1996 · 2026-08-23T23:02:24Z

+    )
+  end
+
+let verification_run (config : Config.compile_config) : unit =


Do we absolutely need to copypaste the existing code?

jasonyu1996 · 2026-08-23T23:03:44Z

Same question. Do we need to duplicate all this code?

…tor errors

…odegen.ml

…Makefile

…ssages

anvil_verification_clean: add compiler support for verification mode

9c9d1a0

arj4web marked this pull request as draft April 4, 2026 02:39

arj4web requested a review from Copilot April 4, 2026 02:40

arj4web marked this pull request as ready for review April 4, 2026 02:40

Copilot started reviewing on behalf of arj4web April 4, 2026 02:40 View session

arj4web changed the title ~~anvil_verification_clean: add compiler support for verification mode~~ SVA assertions for Anvil-SV interfaces Apr 4, 2026

arj4web reviewed Apr 4, 2026

View reviewed changes

Copilot AI reviewed Apr 4, 2026

View reviewed changes

arj4web marked this pull request as draft April 5, 2026 01:37

fix: resolve functional correctness issues from code review

fdef590

Remove generated sv files

6da52e7

arj4web reviewed Apr 10, 2026

View reviewed changes

Comment thread lib/codegen.ml

arj4web Apr 10, 2026

Copy link
Copy Markdown

Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

u can seperate the added code for wrapper generation in different module

arj4web reviewed Apr 10, 2026

View reviewed changes

Comment thread lib/codegenPort.mli

arj4web Apr 10, 2026

Copy link
Copy Markdown

Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here

arj4web requested a review from Copilot April 10, 2026 02:25

Copilot started reviewing on behalf of arj4web April 10, 2026 02:26 View session

Copilot AI reviewed Apr 10, 2026

View reviewed changes

Fix signal-name lookup and add more examples

51f07db

arj4web requested a review from Copilot April 18, 2026 00:47

Copilot started reviewing on behalf of arj4web April 18, 2026 00:47 View session

Copilot AI reviewed Apr 18, 2026

View reviewed changes

fix extern verification codegen, reset gating, and signal lookup

61322ed

Hotaru71 commented Apr 18, 2026

View reviewed changes

arj4web reviewed Apr 19, 2026

View reviewed changes

arj4web requested a review from jasonyu1996 April 19, 2026 05:30

Hotaru71 added 5 commits August 14, 2026 02:56

Add SystemVerilog extern verification integration

00e372b

Merge branch 'kisp-nus:master' into anvil_verification_clean

bdab022

Update extern verification codegen and add TB1-TB4 integration examples

64d3974

Clean up unnecessary changes in extern verification patch

519ef2c

Clean up unnecessary changes

0ed00ed

jasonyu1996 requested changes Aug 23, 2026

View reviewed changes

Hotaru71 added 6 commits August 24, 2026 23:14

Added Missing Files in Example Directory

d021f43

Add trailing newlines to extern SystemVerilog sources to avoid Verila…

d850ce2

…tor errors

Refactor lib/compileDriver.ml and remove unused code from lib/externC…

bd5c152

…odegen.ml

Filter Verilator finish messages from extern test output in examples/…

c3c5730

…Makefile

Fix extern_dyn_dyn_invalid_valid module mapping

fec9659

Update extern verification test outputs to remove Verilator finish me…

655f517

…ssages

Hotaru71 marked this pull request as ready for review September 4, 2026 20:35

		Printf.sprintf "assert property (valid_low_during_DROP_VALID (state_curr, %s)" valid_name;
		Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n";

	\| None -> failwith "AssertName.sender: not initialised (call AssertName.generate first)"
	\| None -> failwith "AssertName.user_sv: not initialised (call AssertName.generate first)"

		\| Some s -> s
		\| None -> failwith "AssertName.receiver: not initialised (call AssertName.generate first)"


		(** Generate code for a {!type:EventGraph.event_graph_collection} to a specified output channel. *)
		val generate : out_channel -> Config.compile_config -> EventGraph.event_graph_collection -> unit

		@@ -0,0 +1,3 @@
		property data_stable_N_cycles (state_curr_0, counter_0, data_0);
		@(posedge clk_i) ((state_curr_0==DROP_ACK \|\| counter_0!=0) \|-> (data_0 == $past(data_0)));

	@(posedge clk_i) ((state_curr_0==DROP_ACK \|\| counter_0!=0) \|-> (data_0 == $past(data_0)));
	@(posedge clk_i) disable iff (!rst_ni) ((state_curr_0==DROP_ACK \|\| counter_0!=0) \|-> (data_0 == $past(data_0)));

		@@ -0,0 +1,3 @@
		property data_stable_N_cycles (state_curr_0, counter_0, data_0);
		@(posedge clk_i) ((state_curr_0==DROP_VALID \|\| counter_0!=0) \|-> (data_0 == $past(data_0)));

	sv_extern_mode: string;
	sv_extern_mode: string; (** SystemVerilog extern handling mode; use "extern" to enable it *)

Conversation

Hotaru71 commented Apr 3, 2026

Uh oh!

arj4web commented Apr 4, 2026

Uh oh!

arj4web commented Apr 4, 2026

Uh oh!

arj4web Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Hotaru71 commented Apr 4, 2026

Uh oh!

arj4web commented Apr 5, 2026

Uh oh!

Hotaru71 commented Apr 9, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

arj4web commented Apr 10, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

arj4web Apr 4, 2026 •

edited

Loading

arj4web left a comment •

edited

Loading