Can I use bind inside generate block

Question

I've a simple assertion: Lets say

assert @(posedge clk) (a |=> b);

I generally connect it with design signals using separate binding module

module bind_module;
  bind dut assertion a1 (.*);
 endmodule

I've a situation: dut has a bus of 45bits, each bit is generated / driven individually but all of them follow same assertion.

Can I use bind statement inside generate block? (for a range of 0 to 44) and then instead of .* use .a (in_bus[i]), .b (out_bus[i])

Answer 1

Assuming you intend the following:

genvar i;
generate
for(i=0; i<45; i=i+1) begin : gen_asrt
  bind dut assertion a1( .a(in_bus[i]), .b(out_bus[i]), .* );
end

This will not work for 2 reasons:

1. The instance name a1 is being clobbered on each loop. Each instance name within a module needs to be unique. Quoting from IEEE std 1800-2012 § 23.11 'Binding auxiliary code to scopes or instances':

   It is legal for more than one bind statement to bind a bind_instantiation into the same target scope. However, it shall be an error for a bind_instantiation to introduce an instance name that clashes with another name in the module name space of the target scope (see 3.13). This applies to both preexisting names as well as instance names introduced by other bind statements. The latter situation will occur if the design contains more than one instance of a module containing a bind statement.

2. i in the bind statement is referring to an i variable name within the scope of dut, not the genvar i. Again, quoting from IEEE std 1800-2012 § 23.11 'Binding auxiliary code to scopes or instances':

   When an instance is bound into a target scope, the effect will be as if the instance was present at the very end of the target scope. In other words, all declarations present in the target scope or imported into the target scope are visible to the bound instance. Wildcard import candidates that have been imported into the scope are visible, but a bind statement cannot cause the import of a wildcard candidate. Declarations present or imported into $unit are not visible in the bind statement.

How to bind this kind of checker:

You could create one module that handles the generate statements, then instantiate that module with a bind statement. Example:

module bind_assertions #(parameter SIZE=1) ( input clock, input [SIZE-1:0] a,b );
genvar i;
generate
  for(i=0; i<SIZE; i=i+1) begin : gen_asrt
    assertion a1_even( .a(a[i]), .b(b[i]), .* );
  end
endgenerate
endmodule

bind dut bind_assertions#(45) a1( .a(in_bus), .b(out_bus), .* );

Technically, you could bind an array of instances. It is legal syntax according to &sect 23.11's Syntax 23-9 plus Appendix A.4.1.1 'Module instantiation'. However it this seems to fail on all the simulators I currently have access to. Example (if it works on your simulator):

bind dut assertion a1[44:0]( .a(in_bus[44:0]), .b(out_bus[44:0]), .* );

Can bind exist within a generate block?

IEEE std 1800-2012 § 27.3 'Generate construct syntax' does mention bind_directive within the syntax for generate constructs is given in Syntax 27-1. Like binding an array of instances, not all simulators support this feature yet. IEEE std 1800-2009 § 27.3 also mentions bind_directive but IEEE std 1800-2005 (first IEEE version of SystemVerilog) does not. Example (if it works on your simulator):

parameter DO_BIND=1;
generate
  if(DO_BIND==1) begin
    bind dut bind_assertions#(45) a1( .a(in_bus), .b(out_bus), .* );
  end
endgenerate