[SVA] 6. サンプル

SVA (SystemVerilog Assertion) 並列アサーションの簡単なサンプル集。必要に応じて negedge にしたり disable iff を入れたりしてください。

  @(negedge clk)  ...;

  @(posedge clk) disable iff (rst)  ...;

信号 A と 信号 B が接続されていること

always_comb begin
  sva_connect : assert (A === B);
end

信号 A がパルスであること

property p_pulse (clk, a);
  @(posedge clk)  $rose(a) |=> ~a;  // もしくは $rose(a) |=> $fell(a)
endproperty

SVA_PULSE: assert property( p_pulse(CLOCK, A) );

以下でもOK。

  @(posedge clk)  $rose(a) |=> $fell(a)

  @(posedge clk)  $rose(a) |=> not (a)

信号 A が n サイクルのレベルであること

property p_level (clk, a, n);
  @(posedge clk)  $rose(a) |=> $stable(a)[*n-1] ##1 $fell(a);
endproperty

SVA_LEVEL: assert property( p_level(CLOCK, A, 4) );

信号 A が n～m サイクルのレベルであること

property p_level (clk, a, n, m);
  @(posedge clk)  $rose(a) |=> $stable(a)[*n-1:m-1] ##1 $fell(a);
endproperty

SVA_LEVEL: assert property( p_level(CLOCK, A, 2, 4) );

信号 A を n サイクルシフトした信号が B であること

property p_delay (clk, a, b, n);
  @(posedge clk)  b |-> $past(a, n);
endproperty

SVA_DELAY: assert property( p_delay(CLOCK, A, B, 4) );

単純に考えると以下のようになるが、これだと A を契機とせずに B だけ変化した場合も OK となる。

property p_delay (clk, a, b, n);
  @(posedge clk)  a |-> ##n b;
endproperty

信号 A が 0 の間 信号 B が 1 にならないこと

property p_never (clk, a, b);
  @(posedge clock)  ~a |-> ~b;
endproperty

SVA_NEVER: assert property( p_never(CLOCK, A, B) );

「信号 B が 1 のとき 信号 A も 1 であること」と同じ意味なので以下でも OK。

property p_never (clk, a, b);
  @(posedge clk)  b |-> a;
endproperty

SVA_NEVER: assert property( p_never(CLOCK, A, B) );

信号 A が 1 の間 信号 B が変化しないこと

property p_stable (clk, a, b);
  @(posedge clk)  a |=> $stable(b);
endproperty

SVA_STABLE: assert property( p_stable(CLOCK, A, B) );

A の立下りポイントの変化は許容するようにするには...どうしたらいいんでしょうね。いい記述方法が思いつかないです。

property p_stable (clk, a, b);
  @(posedge clk)  (a ##1 a) |-> (b == $past(b) );
endproperty

信号 A 立ち上がりの n サイクル後に 信号 B が変化すること

property p_changed (clk, a, b, n);
  @(posedge clk)  $rose(a) |-> ##n $changed(b);
endproperty

SVA_CHANGED: assert property( p_changed(CLOCK, A, B, 4) );

信号 A 立ち上がりのタイミングで 信号 B がインクリメントされること

property p_changed (clk, a, b);
  @(posedge clk)  $rose(a) |-> (b == $past(b, 1) + 1'd1);
endproperty

SVA_CHANGED: assert property( p_changed(CLOCK, A, B) );

インクリメントは + 1 とせず上記のように + 1'd1 としておくと安全。+ 1 とすると桁あふれ時 (b が '1 から 0 に戻るとき) に不一致となる恐れがある。

多ビット信号 A がワンホットであること

property p_onehot (clk, a);
  @(posedge clock)  $onehot(a);
endproperty

SVA_ONEHOT: assert property( p_onehot(CLOCK, A) );

多ビット信号 A がゼロ・ワンホットであること

property p_zero_onehot (clk, a);
  @(posedge clock)  $onehot0(a);
endproperty

SVA_ZERO_ONEHOT: assert property( p_zero_onehot(CLOCK, A) );

多ビット信号 A のパリティチェック

p = 0 は偶数パリティ。p = 1 は奇数パリティ。

property p_parity (clk, rst, a, p);
  @(posedge clk) disable iff (rst)  $countbits(a, 1) % 2 == p;
endproperty

SVA_PARITY: assert property( p_parity(CLOCK, RESET, A, 0) );

多ビット信号 A が n～m の値になること

property p_range (clk, a, n, m);
  @(posedge clock)  a >= n && a <= m;
endproperty

SVA_RANGE: assert property( p_range(CLOCK, A, 0, 4) );

信号 A のリセット解除直前の値が正しいこと

property p_reset (clk, rst, a, v);
  @(posedge clock)  $fell(rst) |-> $past(a) === v);
endproperty

SVA_RESET: assert property( p_reset(CLOCK, RESRT, A, 0) );