システムタスク一覧
SystemVerilogでアサーションように用意されているシステムタスクです。
| システムタスク | 説明 |
| $rose | 立ち上がりの判定 |
| $stable | 無変化の判定 |
| $fell | 立ち下がりの判定 |
| $past | 過去の信号値を参照 |
| $onehot | 信号がワンホットか判定 |
| $onehot0 | 信号がワンホットもしくはALL0 か判定 |
| $countones | 2 進数表記で‘1’の数を返す |
| $isunknown | 信号にX，Z を含むかを判定 |
| $sampled | アサーションで使用する値を取得 |
| $asserton | アサーションをONにする |
| $assertoff | アサーションをOFFにする。すでに起動中のアサーションはOFFできない |
| $assertkill | アサーションをOFFにする |
$rose $fell $stable $pastを使った記述例
以下に記述例を示します。アサーション記述をDUTでbindし、使用する例です。
cnt_enが1のときカントするカウンターです。
module dut(
input clk ,
input rst ,
input cnt_en,
output cnt_en_out,
output reg [3:0] counter
) ;
parameter P_D = 1 ;
//cnt_en_out : renameして出力
assign cnt_en_out = cnt_en ;
//counter : 4bit counter
always @(posedge clk or negedge rst) begin
if(!rst) begin
counter <= #P_D 4'h0 ;
end
else if(cnt_en) begin
counter <= #P_D counter+1 ;
end
endmodule アサーションの条件は、「cnt_en=1ならば、カウンタの値は過去の値＋１である」です。
bindでdutに接続します。接続する記述は以下の通りです。
bind 接続先DUT名 アサーション記述のモジュール名 任意のインスタンス名 (接続信号を記載。アスタリスクはワイルドカード）property-endpropertyでアサーションを記述しています。
cnt_en_outに対して$rose $fell $stableを実行します。
cnt_en_outはcnt_enをリネームしてそのまま出力する信号なので毎回PASSします。
$pastについてはcnt_en=1のときはcounterが前回の値より1大きい というアサーションを記述しています。counter値が15から0になるタイミングで制約に一致しないため、FAILします。
bind dut sva01 sva01 (.*) ;
module sva01(
input clk ,
input rst ,
input cnt_en,
input [3:0] counter
) ;
property p01 ;
@(posedge clk) disable iff(!reset)
$rose(cnt_en) |-> $rose(cnt_en_out) ;
endproperty
property p02 ;
@(posedge clk) disable iff(!reset)
$fell(cnt_en) |-> $fell(cnt_en_out) ;
endproperty
property p03 ;
@(posedge clk) disable iff(!reset)
$stable(cnt_en) |-> $stable(cnt_en_out) ;
endproperty
property p04 ;
@(posedge clk) disable iff(!reset)
cnt_en==1 |=> counter == $past(counter+1) ;
endproperty
A_P01:assert property(p01) ;
A_P02:assert property(p02) ;
A_P03:assert property(p03) ;
A_P04:assert property(p04) ;
endmoduleproperty p04をFAILにしないためには、counterが15から0になるときはチェックしないようにします。cnt15 という信号を生成し、propertyの条件文に追加します。
「counter=15ならば次は0になる」というアサーションを追加すればcounterの値を全てチェックできます。
wire cnt15 ;
assign cnt15 = (counter=='d15) ? 1'b1 : 1'b0 ;
property p04 ;
@(posedge clk) disable iff(!reset)
(cnt_en==1) & (cnt15==0) |=>counter == $past(counter+1) ;
endproperty
property p05 ;
@(posedge clk) disable iff(!reset)
(cnt_en==1) & (cnt15==1) |=> counter == 0 ;
endproperty
$pastは変数の名前の後ろにサイクル数を指定できます。$past(counter+2,2)と記述すると2サイクル前のcounter値を表しています。
コメント