我可以在生成块中使用bind吗？

Question

我有一个简单的断言：让我们说

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

我通常使用单独的绑定模块将其与设计信号连接

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

我有一种情况：dut有一个45位的总线，每个位都是单独生成/驱动的，但它们都遵循相同的断言。

我可以在generate块中使用bind语句吗？ （范围为0到44）然后代替。*使用.a (in_bus[i]), .b (out_bus[i])

Answer 1

假设您打算如下：

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

这不会有两个原因：

1. 实例名称a1正在每个循环中被破坏。模块中的每个实例名称都必须是唯一的。引自IEEE std 1800-2012§23.11'将辅助代码绑定到范围或实例'： 多个bind语句将bind_instantiation绑定到同一目标范围是合法的。但是，如果bind_instantiation引入的实例名称与目标作用域的模块名称空间中的另一个名称冲突，则应该是错误的（请参阅3.13）。这适用于预先存在的名称以及其他bind语句引入的实例名称。如果设计包含多个包含bind语句的模块实例，则会出现后一种情况。
2. 绑定语句中的i指的是i范围内的dut变量名，而不是genvar i。再次引用IEEE std 1800-2012§23.11“将辅助代码绑定到范围或实例”： 当实例绑定到目标作用域时，效果就像实例存在于目标作用域的最末端一样。换句话说，目标作用域中存在的或导入到目标作用域的所有声明对绑定实例都是可见的。已导入到作用域中的通配符导入候选项是可见的，但绑定语句不能导致导入通配符。存在或导入$unit的声明在绑定语句中不可见。

How to bind this kind of checker:

您可以创建一个处理generate语句的模块，然后使用bind语句实例化该模块。例：

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), .* );

从技术上讲，您可以绑定一组实例。根据＆第23.11节的语法23-9以及附录A.4.1.1“模块实例化”，它是合法的语法。然而，这似乎在我目前可以访问的所有模拟器上都失败了。示例（如果它适用于您的模拟器）：

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'生成构造语法'确实在生成构造的语法中提到bind_directive在语法27-1中给出。与绑定一组实例一样，并非所有模拟器都支持此功能。 IEEE std1800-2009§27.3也提到了bind_directive，但IEEE标准1800-2005（SystemVerilog的第一个IEEE版本）却没有。示例（如果它适用于您的模拟器）：

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