# [[DV筆記] Systemverilog - Assertion](/s6FcwjQkRSKJ8GWLDy3Wwg)
## 前言
Assertion絕對是身為 DV 的必備技能，跟 coverage 的語法有些類似，有點雜，所以急需要整理起來
## 基本語法
一般 assertion 都是搭配 clk 去觸發，因為如果都是用組合邏輯去寫，會很浪費 memory
### Immediate Assertion
在 simulation 過程中，會被立即檢查，使用 ==assert==

<label>: assert (expression) <pass_statement> else <fail_statement>

module design_ex (input clk, reqA, reqB, in);
  always @(posedge clk) begin 
    assert (reqA || reqB) else $error("assertion failed");
    assert (in == 0) else $warning("assertion warning for in == 0");
  end
endmodule

immediate assertion 會在 clk edge 後檢查，如果要避免與 simulation 變化造成的問題，可以寫:

assert final (in == 0);

### Concurrent Assertion
使用 ==assert property== 關鍵字，通常用來檢查時序邏輯或是更複雜的sequence

module example_module;
    logic clk, rst, valid;


    property p1;
        @(posedge clk) disable iff (rst) valid |-> $stable(valid);
    endproperty

    assert property (p1);

endmodule

Concurrent assertion 又可以使用 sequence 或是 property blcok 去描述，但是通常 sequence 是描述只有組合邏輯的 assertion，而 property 則是可以描述跟時序有關的 assertion，像是 a ==|->== b 這個只能寫在 property 中。

>[!Note]
我好像都是只有使用 property

## Assertion Function 使用

$rose(a);//a signal 0 -> 1
$fell(a);//a signal 1 -> 0
$stable(a);//a signal 不變
$intersect(a,b);//a,b 同時發生，同時結束
a within b; //b發生時間內包含 a 發生
a ##2 b;//a 發生後 2 clk b 發生
a ##[1:3]b; // a 發生後 1-3 clk 內 b 發生
a ## [1:$]b; // a 發生後 1 clk 到 simulation 結束之間 b 發生
c throughout (a ##2 b); a 成立到 b 成立之間 c 都成立
a |-> b; // 像是 if (a) b 這樣， a 發生 b 必須發生
a |=> b; // a 發生後過1個 clk ， b 發生
@(posedge clk) $past(a,2) == 0; //posedge clk 後 前2個 clk a == 0;
@(posedge clk) a [*3]; // a 連續3個 clk 成立
@(posedge clk) a [1:3]; // a 在連續1-3個 clk 成立 (1,2,3 clk 成立都可以)
@(posedge clk) a [->3]; // a 在非連續3個 clk 成立 (a 發生 3 次 ，但不用連續)
    
$onehot(BUS)      ————BUS中有且只有1 bit是1，其他是0。
$onehot0(BUS)     ————BUS中有不超過1 bit是1，也允許全0。
$isunknown(BUS)   ————BUS中存在z或x。
$countones(BUS)==n ————BUS中有且只有n bits是1，其他是0。

### 結語
雖然語法概念不難，但有點雜，而且要真正練習寫才會越來越順手