System Verilog Assertion Binding (SVA Bind)

In short: SVA bind lets you attach assertions to a design module without editing that module. You write your checkers in a separate assertion module, then use the bind keyword to connect them to a target module or a specific instance. The design source stays untouched, which is ideal when you are not allowed to change RTL.

Verification engineers often work with Verilog or VHDL modules they cannot modify. You still need to add SystemVerilog assertions to check that logic. The bind construct solves this cleanly: your checks live outside the design and are wired in at elaboration.

A simple way to picture it

Imagine a rental car you are not allowed to modify. You still want a dashcam recording how it is driven. Instead of rewiring the car, you clip a self-contained camera onto the windshield; it taps into what it needs and records, while the car stays exactly as the owner left it. SVA bind is that clip-on camera: your assertion module attaches to the design, watches its signals, and reports rule breaks, without changing a single line of the design.

How bind works

There are three pieces. First, the target: the design module you want to check. Second, an assertion module that declares ports matching the target signals and holds your properties. Third, the bind statement, which instantiates the assertion module inside the target so it can see the target signals. Binding happens at elaboration, so the assertion module effectively becomes part of the target hierarchy.

Step 1: the design under test

module dut (
  output logic [7:0] out,
  output logic       valid,
  input  logic       wr, rd, clk, rst_n,
  input  logic [7:0] in
);
  // ... design logic (you cannot edit this file) ...
endmodule : dut

Step 2: the assertion module

Wrap your properties in a module whose ports line up with the signals you want to observe. This wrapper and its port list are required for bind.

module dut_sva (
  input logic [7:0] out, in,
  input logic       valid,
  input logic       wr, rd, clk, rst_n
);
  // While reset is low, valid must be low
  a_reset_clears_valid: assert property (
    @(posedge clk) (!rst_n) |-> (valid == 1'b0)
  ) else $error("valid high during reset");

  // A write must be followed by valid within 2 cycles
  a_wr_leads_valid: assert property (
    @(posedge clk) disable iff (!rst_n)
      wr |-> ##[1:2] valid
  ) else $error("write did not produce valid in time");
endmodule : dut_sva

Step 3: the bind statement

The bind statement names the target module, the assertion module, an instance name, and the port connections. When the assertion module uses the same signal names as the target, you can use the SystemVerilog implicit connection .*. Otherwise you must map ports by name.

module tb;
  logic [7:0] out, in;
  logic       valid, wr, rd, clk, rst_n;

  dut dut_u1 (.*);   // design instance

  // Bind the checker into the module type: applies to every dut instance
  bind dut dut_sva sva_chk (.*);
endmodule : tb

That single line binds dut_sva into the dut module type. Because it targets the type, every instance of dut in the design gets the checker. The instance name here is sva_chk.

Binding to a specific instance only

Sometimes you want checks on one instance but not another. Bind to a named instance instead of the type by qualifying the target with the instance path.

// Two instances of the same module
dut dut_u1 (.*);
dut dut_u2 (.*);

// Check only dut_u1, leave dut_u2 unchecked
bind dut : dut_u1 dut_sva sva_chk (.*);

The form bind target_module : instance_name checker_module inst (...) restricts the bind to that one instance. This is handy when two instances follow different rules.

Mapping ports when names differ

If the checker port names do not match the target signal names, replace .* with explicit named connections. This is the safest style on real projects because it removes any guesswork about which signal feeds which check.

// Checker uses generic names; target uses project names
bind dut dut_sva sva_chk (
  .clk   (core_clk),
  .rst_n (reset_n),
  .out   (data_out),
  .in    (data_in),
  .valid (out_valid),
  .wr    (write_en),
  .rd    (read_en)
);

Binding into an interface

You can bind a checker into an interface as well, which is a clean way to police a protocol wherever that interface is used. The mechanism is the same: target the interface, instantiate the checker, connect the ports.

interface bus_if (input logic clk);
  logic req, gnt;
endinterface

module bus_sva (input logic clk, req, gnt);
  // A request must eventually be granted within 4 cycles
  a_req_gnt: assert property (
    @(posedge clk) req |-> ##[1:4] gnt
  );
endmodule

// Bind the checker into the interface
bind bus_if bus_sva chk (.*);

Common mistakes to avoid

  • Binding to a file name or a raw signal. You bind a module or interface into a target module or interface, never to a .sv file or to a single signal.
  • Skipping the port list in the checker. The wrapper module must declare ports even when you later connect with .*.
  • Using .* when names do not match. If any checker port has no same-named signal in the target, use explicit named connections.
  • Forgetting disable iff around reset, which can cause spurious failures while the block is in reset.
  • Assuming a type bind hits one instance. Binding to the module type applies to every instance; use the instance-qualified form to target one.

Expected output, in plain words

After elaboration, each bound checker runs as if it were written inside the target. If a design violates a property, the simulator reports the failing assertion with its label and your $error message, pointing at the target instance path. If nothing is violated, the checks stay quiet. Note: this behaviour is described from the IEEE 1800 rules for bind, not from a captured tool run, and exact messages vary by simulator. Confirm on your own tool.

Bind pairs well with the operators covered in our basic assertions examples and the timing rules in immediate vs concurrent assertions. For revision, see the interview questions and the broader SystemVerilog category.

Frequently asked questions

What is SVA bind used for?

SVA bind attaches assertion checkers to a design module without modifying the design source. You write properties in a separate assertion module and connect them with the bind keyword, which is ideal when you are not allowed to edit the RTL.

Do I bind to a module or to an instance?

You can do both. Binding to the module type, such as bind dut dut_sva chk (.*), applies the checker to every instance of that module. Binding with an instance qualifier, such as bind dut : dut_u1 dut_sva chk (.*), applies only to that one instance.

Does the assertion module need a port list?

Yes. The checker must be wrapped in a module that declares ports matching the target signals. The port list is required even if you later connect the ports using the .* implicit connection.

When can I use .* in a bind statement?

You can use .* when the checker port names exactly match the target signal names. If any names differ, replace .* with explicit named connections so each checker port maps to the correct target signal.

Can I bind assertions into an interface?

Yes. You can bind a checker module into an interface just as you bind into a module. This is a clean way to police a protocol wherever that interface is instantiated.

Does bind change the design behaviour?

No. Bound checkers only observe signals and report violations. They do not drive design signals or alter functionality, so the design behaves exactly as it did before the bind was added.

Similar Posts