Tutorials

Protocols

Learn More

The bind statement attaches an assertion module to existing RTL without adding assertion code inside the design source file.

The ‘bind’ directive allows binding assertions with

  1. Design module
  2. Interface 

Binding is possible with

  1. A specific instance of a module or interface
  2. All instances of a module or interface

Syntax:

To bind with specific instance

bind <dut_specific_instance_path> <assertion_module> <instance>

To bind with all instances

bind <dut_module> <assertion_module> <instance>
  • Use a module or interface type to bind the assertion to every instance of that type.
  • Use a hierarchical instance path to bind the assertion to one specific instance.
  • instance_name is the name of the new assertion-module instance created inside each selected target.

Why Bind Assertions?

Assertions can be written directly inside a design module, but that mixes verification code with RTL. Binding keeps the assertion code in a separate file while still allowing it to observe design signals.

A bound module is created during elaboration. It does not drive the design signals; its input ports only observe them for assertion checks.

bind example

when d is high at a rising clock edge, q must be high at the next rising edge. Reset stops the check.

assertion.sv

module assertion_dff (
  input clk, rst_n, d, q
);
  
  sequence seq1;
    d ##1 q;
  endsequence 
  
  property prop;
    @(posedge clk) disable iff(rst_n)
    d |=> seq1;
  endproperty
  
  dff_assert: assert property (prop) else $display("Assertion failed at time = %0t", $time);
endmodule
`include "assertion.sv"
module tb;
  reg clk, rst_n;
  reg d;
  wire q;
  
  D_flipflop dff1(clk, rst_n, d, q);
  D_flipflop dff2(clk, rst_n, d, q);
  
  // To bind with all instances of DUT
  bind D_flipflop assertion_dff all_inst(clk, rst_n, d, q);
  
  // To bind with single instance of DUT
  bind tb.dff2 assertion_dff single_inst(clk, rst_n, d, q);
  
  always #2 clk = ~clk;
  initial begin
    clk = 0; rst_n = 0;
    d = 0;
    
    #3 rst_n = 1;
    
    repeat(6) begin
      d = $urandom_range(0, 1);
      #3 rst_n = $urandom_range(0, 1);
    end
    $finish;
  end
  
  initial begin
    $monitor("At time = %0t: rst_n = %b, d = %b, q = %b", $time, rst_n, d, q);
  end
endmodule

Output:

At time = 0: rst_n = 0, d = 0, q = x
At time = 2: rst_n = 0, d = 0, q = 0
At time = 3: rst_n = 1, d = 1, q = 0
At time = 6: rst_n = 0, d = 1, q = 0
At time = 9: rst_n = 1, d = 0, q = 0
At time = 15: rst_n = 0, d = 0, q = 0
At time = 18: rst_n = 1, d = 1, q = 1

Selecting the Bind Target

Binding to all instances

Using the module type as the target attaches one assertion_dff instance to every D_flipflop instance, including dff1 and dff2.

bind D_flipflop assertion_dff all_inst (
  .clk(clk), .rst_n(rst_n), .d(d), .q(q)
);

For each target, names such as clk, d, and q are resolved in that target instance. Therefore, each assertion observes the signals belonging to its own flip-flop instance.

Binding to one specific instance

Using the hierarchical path tb.dff2 attaches the assertion only to dff2. Instance dff1 is not checked by this bind statement.

bind tb.dff2 assertion_dff single_inst (
  .clk(clk), .rst_n(rst_n), .d(d), .q(q)
);

The all-instance and specific-instance forms are alternatives in this example. If both are enabled, dff2 receives two assertion instances and the same failure may be reported twice.

Where to Place the Bind Statement

Keep the assertion module in a separate file and compile it with the testbench. The bind statement may be placed in a testbench or in a separate binding file, making the verification code easier to reuse without editing the RTL.

SystemVerilog Assertions