3

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

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

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

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

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

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

4

1 回答 1

2

假设您打算执行以下操作：

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在bind 语句中是指i范围内的变量名dut，而不是genvar i. 再次引用IEEE std 1800-2012 § 23.11 'Binding assistant code to scopes or instances'：

    当一个实例被绑定到一个目标作用域时，效果就像该实例出现在目标作用域的最末端一样。换句话说，目标范围内的所有声明或导入到目标范围内的所有声明对绑定实例都是可见的。已导入范围的通配符导入候选是可见的，但绑定语句不能导致通配符候选的导入。存在或导入$unit的声明在绑定语句中不可见。

如何绑定这种检查器：

您可以创建一个处理生成语句的模块，然后使用绑定语句实例化该模块。例子：

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

可以bind存在于一个generate块中吗？

IEEE std 1800-2012 § 27.3“生成构造语法”bind_directive在语法 27-1 中给出了生成构造的语法。与绑定实例数组一样，并非所有模拟器都支持此功能。IEEE std 1800-2009 § 27.3 也提到bind_directive但 IEEE std 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
于 2013-12-19T22:11:20.077 回答