Systemverilog assertion來檢查壞信號轉換

Question

我想寫一個斷言，只有當一個信號在'clk'的上升沿轉換時纔會觸發。我寫了下面的代碼來測試我的想法

module test(); 

bit clk, clkb; 
int d; 

assign clkb = ~clk; 

initial begin 
    clk = 0; 
    forever #100 clk = ~clk; 
end 

initial begin 
    d = 10; 
    #150 d = 20; 
end 

sva_d_chgd: assert property (@(posedge clk) $stable(d,@(clkb))) 
    else $error($psprintf("err: time = %0d, clk = %b, d = %0d", $time, clk, d)); 

always @ (d or clk) begin 
    $display("time = %0d, clk = %b, d = %0d", $time, clk, d); 
    if ($time > 200) $finish; 
end 
endmodule 

上面的代碼返回VCS以下的輸出：

time = 0, clk = 0, d = 10 
time = 100, clk = 1, d = 10 
"test.vs", 18: test.sva_d_chgd: started at 100s failed at 100s 
     Offending '$stable(d, @(clkb))' 
Error: "test.vs", 18: test.sva_d_chgd: at time 100 
err: time = 100, clk = 1, d = 10 
time = 150, clk = 1, d = 20 
time = 200, clk = 0, d = 20 
time = 300, clk = 1, d = 20 
$finish called from file "test.vs", line 23. 
$finish at simulation time     300 

爲什麼在時間100斷言火的時候「d」保持穩定，直到時間150？

Answer 1

在你的代碼中，在clk的每個posedge上進行穩定檢查，以查看「d」的值是否在clkb的前兩個邊緣之間發生了變化。因爲在clk的第一個posedge中沒有以前的「d」的clkb邊緣值，所以穩定返回「unknown」而不是「true」或「false」，這會導致斷言失敗。

我已經添加了一個復位信號給你的代碼，並禁用斷言，直到clk的第一個posedge。當「d」變化時，我也會移動。

module test(); 

bit clk, clkb, rst; 
int d; 

assign clkb = ~clk; 

initial begin 
    clk = 0; 
    forever #100 clk = ~clk; 
end 

initial begin 
    rst = 1; 
    #150 rst = 0; 
end 

initial begin 
    d = 10; 
    #250 d = 20; 
end 

sva_d_chgd: assert property (@(posedge clk) 
          disable iff (rst) 
          $stable(d,@(clkb))) 
    else $error($psprintf("err: time = %0d, clk = %b, d = %0d", $time, clk, d)); 

always @ (d or clk) begin 
    $display("time = %0d, clk = %b, d = %0d", $time, clk, d); 
    if ($time > 400) $finish; 
end 
endmodule 

下面是輸出：

# time = 0, clk = 0, d = 10 
# time = 100, clk = 1, d = 10 
# time = 200, clk = 0, d = 10 
# time = 250, clk = 0, d = 20 
# time = 300, clk = 1, d = 20 
# ** Error: err: time = 300, clk = 1, d = 20 
# Time: 300 ns Started: 300 ns Scope: test.sva_d_chgd File: assert_test.sv Line: 26 
# time = 400, clk = 0, d = 20 
# time = 500, clk = 1, d = 20 
# ** Note: $finish : assert_test.sv(30) 
# Time: 500 ns Iteration: 1 Instance: /test 

這得到周圍的斷言的第一不必要的失敗，但我覺得你編碼的斷言的方式現在還沒有真正捕捉你要找的條件。