硅芯思见：断言如何与设计bind
一般在定义好断言之后，都会将其与特定的待检查设计绑定，那么具体应该如何将assertion与对应的设计进行绑定呢？常用的方法一般有两种：一种是将assertion直接内建在设计内部，这种方法简单易行也是最常用的方式。另一种是将assertion和设计分离，使用bind与特定的设计进行绑定连接。但是不管使用哪种方式，绑定的基本流程是一样的。
`timescale 1 ns /1 ps
module test(clk,rst,sig0,sig1);
input sig0;
input clk,rst;
output sig1;
bit sig1;
always @(posedge clk)
begin
if (rst == 1'b0) begin
sig1 <= 1'b0;
end else begin
sig1 <= sig0;
end
end
endmodule // test
//>>> STEP1 : define sva
module ast_chk(clk,rst,sig0,sig1);
input clk,rst,sig0,sig1;
// property
property p;
@(posedge clk)
disable iff(rst == 1'b0)
sig0 |-> ##1 sig1;
endproperty // p
// assert
a : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule // ast_chk
// tb
module top_tb;
bit clk,rst;
bit sig0; // default value : 0
bit sig1;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig0 = 1'b0; rst = 1'b0;
#2 rst = 1'b1; #2 sig0 = 1'b1;
#2 sig0 = 1'b0; #4 sig0 = 1'b1;
#3 sig0 = 1'b0; #4 $stop;
end
//>>> STEP2 : instance dut and sva
test u_dut(clk,rst,sig0,sig1);
ast_chk sva_01(clk,rst,sig0,sig1);
//>>> STEP3 : bind sva and dut
bind test ast_chk sva_01(clk,rst,sig0,sig1);
endmodule // top_tb 【仿真结果】 
示例中，将assertion的定义从设计本身中剥离出来进行单独的定义，然后在具体设计例化后再通过bind将assertion与设计中关心的信号进行连接。这里需要注意以下几点：
Ø bind时assertion与设计关联的信号不一定是设计端口所有信号，关联的端口数目可以少于设计实际端口数；
Ø bind时使用的是设计实例化时连接端口的实际信号名，不是设计定义时指定的端口名，当然设计例化时可以使用与原端口名同名的信号名；
Ø 通过上例中注释的步骤，可以将assertion bind归纳为以下三步：
通过示例中的bind方式，该assertion将会与该待测设计的所有实例进行bind，当然可以指定不同的观测信号名。其实bind的方式是比较灵活的，不止上例中一种方式，要了解其他方式必须对IEEE 1800中关于bind的格式有所了解，bind的使用格式可表示如下：
bind <module_name or instance_name> <checker_name> <checker_instance_name> <design_signals>
其中
Ø module_name和instance_name用于指定将要被监测的设计的模块名或者实例名；
Ø checker_name用于指定监测模块名，即定义断言属性的模块；
Ø checker_instance_name用于指定监测模块的实例名；
Ø design_signals用于指定将要监测的模块的信号；
通过定义可见bind的影响范围取决于bind时指定的是设计的模块名还是实例名：
Ø 如果bind时使用具体的实例化名，那么assertion仅可与特定的实例化设计关联，与同一模块的其他实例化不关联；
`timescale 1 ns /1 ps
module test(clk,rst,sig0,sig1);
input sig0;
input clk,rst;
output sig1;
bit sig1;
always @(posedge clk)
begin
if (rst == 1'b0) begin
sig1 <= 1'b0;
end else begin
sig1 <= sig0;
end
end
endmodule // test
//>>> STEP1 : define sva
module ast_chk(clk,rst,sig0,sig1);
input clk,rst,sig0,sig1;
// property
property p;
@(posedge clk)
disable iff(rst == 1'b0)
sig0 |-> ##1 sig1;
endproperty // p
// assert
a : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule // ast_chk
// tb
module top_tb;
bit clk,rst;
bit sig0; // default value : 0
bit sig1,sig2
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig0 = 1'b0; rst = 1'b0;
#2 rst = 1'b1; #2 sig0 = 1'b1;
#2 sig0 = 1'b0; #4 sig0 = 1'b1;
#3 sig0 = 1'b0; #4 $stop;
end
//>>> STEP2 : instance dut and sva
test u_dut0(clk,rst,sig0,sig1);
test u_dut1(clk,rst,sig0,sig2);
ast_chk sva_01(clk,rst,sig0,sig1);
//>>> STEP3 : bind sva and dut
bind test:u_dut0 ast_chk sva_01(clk,rst,sig0,sig1); //u_dut1可仿照
endmodule // top_tb 
示例中，在bind时待测设计通过实例化名与assertion进行bind，那么没有与assertion进行bind的设计将不会与assertion关联。可见，通过将assertion独立于设计之外，可以灵活的指定与assertion具体关联的设计，从而增加了断言的可复用性，可以在不同的设计中、不同的实例中被使用。
【使用modelsim、questasim进行断言仿真可参考如下命令】
-
vlog -sv abc.v
-
vsim -assertdebug -novopt testbench
-
view assertions
上述命令使用时一定要注意第二步析构时不能省略“-novopt”，否则将不能直观的在波形窗口对断言进行debug。
查看14道真题和解析
