assertionで使用するシステムタスク

システムタスク一覧

SystemVerilogでアサーションように用意されているシステムタスクです。

$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) ;
endmodule

property 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値を表しています。