斷言是什么？
斷言是對設計違例的一種嚴查，能夠在違例時立刻報出錯誤。
為什么使用斷言，斷言的優勢又有那些呢？
1.斷言能夠縮短你的開發時間，斷言的代碼是比較簡單的，相比systemverilog能夠很好的處理信號的電平和邊沿變化的檢測。如systemverilog要想實現時鍾上升沿時如果FRAME_也是上升沿則2個時鍾后LDP_是下降沿有需要開發下圖的代碼，但是使用斷言則非常簡單，
property ldpcheck； @(posedge clk) $rose(FRAME_) |-> ##2 $fell(LDP_) ; endproperty assert property(ldpcheck);
2.斷言是可以觀測的，能夠通過斷言直接看到是哪里的bug；
3.斷言能夠提供覆蓋率收集；
還有很多優點如斷言支持CDC（clock domain crossing）、可重用性好、斷言在驗證和設計中是一直處於檢測狀態的等。
斷言需要添加在哪里？
1.rtl設計中，內部module，如非法狀態轉換、死鎖、fifo等
2.module接口intrerace中，內部模型接口中，如在req是0時ack不能是1。
3.芯片功能斷言
4.用來檢測芯片接口違例的斷言，如獨立的PCIX和AXI接口等
5.用來性能的斷言，如讀響應的最大時延不能超過5個clk；
斷言的類型
1.立即斷言（不支持formal 驗證）
用來檢測待測設計的信號值，可以理解為設計中的if。
2.並發斷言
存在edge采樣的檢測信號的斷言
立即斷言
立即斷言是一個程序塊中的簡單信號狀態檢測，可以直接理解為條件判定if。下面是一個簡單的狀態檢測，通過assert檢測b或c，條件成立打印時間和assert passed
並發斷言
一個簡單的並發斷言的例子，在clk上升沿時，cStart發生，則觸發斷言檢測，req和cStat同時發生並且2個clk后gnt發生。
其中cStat為antecedent，|->為implication operator，str1為consequent
inplication operator分為overlapping operattor（|->）和non-overlapping operattor（|=>）,分別就是overlapping operattor是consequent 要和antecedent同時發生，而non-overlapping operattor是consequent 要在antecedent下一個采樣時鍾發生，其實cStart |-> ##1 (req ##2 gnt) 等效於cStart |=> (req ##2 gnt)
並發斷言中常用的表達式和語法
| operator | description |
| $rose | 上升沿檢測，從0或x或z變為1 |
| $fell | 下降沿檢測，從1或x或z變為0 |
| $stable | 檢測當前邊沿采樣狀態和上一邊沿采樣狀態沒有發生變化 |
| $past | 追溯過去任意時鍾 |
| $onehot | 用於檢測表達式中只有1bit為1其他bit為0或高阻或X態 |
| $onehot0 | 檢測表達式中所有bit都為0或只有1bit為1 |
| $isunknown | 檢測信號為高阻態或者X態 |
| $countones | 統計表達式中bit為1的個數 |
| $asserton | 開啟斷言 |
| $assertoff | 關閉不處於活動狀態下斷言 |
| $assertkill | 殺死所有斷言 |
$rose
$rose,如下面使用在clk上升沿時intr存在從0或x態或高阻態變為1的過程，也就是在clk上一個上升沿時intr是0或x態或高阻態，在當前clk上升沿時是1，這時就滿足$rose的邊沿檢測屬性了。
$fell
$fell，$fell和$rose是相似的，只不過是用來檢測下降沿的,在clk上升沿時req存在從1或x態或高阻態變為0的過程，也就是在clk上一個上升沿時req是1或x態或高阻態，在當前clk上升沿時是0，這時就滿足$fell的邊沿檢測屬性了。
正好截圖中把$isunknown()帶上了,這里解釋下$isunknown()，是檢測信號為高阻態或為X態，加上not，即判定的結果相反，$fell(we_) |-> not ($isunknown(wData))意思是，在we_出現下降沿時 wData為0或1，不能是高阻態或者X態的檢測。
$stable
$stable,檢測當前時鍾邊沿的狀態和上一時鍾邊沿的狀態是一致的不發生改變則通過。
$past
$past,它可以讓你追溯過去任意時鍾，然后您可以檢查'表達式1'是否具有特定的值，在以前的時鍾數（嚴格地說是在時間點之前）。請注意，時鍾的數量是可選的。如果你沒有指定它，默認情況下是在過去的一個時鍾查找'表達式1'。
需要注意的另一個警告是當你在仿真的初始時間刻度中調用$past時，沒有足夠的時鍾去'過去'。例如，您可以指定'a | - > $ past（b）'，並且在時間'0'前提'a'為真。過去並沒有時鍾。在這種情況下，斷言將使用'b'的'初始'值。 'b'的初始值是多少？它不是'初始'塊中的那個，它是變量'b'被聲明的值（如'logic b = 1'b1;'）。在我們的例子中，如果'b'在其聲明中未被初始化，斷言將失敗。如果聲明初始值為1'b1，則斷言將通過.
$onehot
$onehot用於檢測表達式中只有1bit為1其他bit為0或高阻或X態不關心。
$onehot0用於檢測表達式中所有bit都為0或只有1bit為1。
$isunknown
檢測出高阻態Z或者是X態。
$countones
統計表達式中每bit是1的個數。
$asserton
開啟斷言
$assertoff
關閉斷言，處於活動狀態下的斷言不關閉。
$assertkill
殺死所有的斷言。
| operator | description |
| ##m | 延遲m個采樣時鍾 |
| ##[m:n] | 延遲m到n個采樣時鍾 |
| [*m] | 重復m次，不連續 |
| [*m:n] | 重復m到n次，不連續 |
| [=m] | 重復m次，連續 |
| [=m:n] | 重復m到n次，連續 |
| [->m] | 到達m次，不連續 |
| [->m:n] | 到達m到n次，不連續 |
| sig1 througnout seq1 | 在seq1整個中sig1要為真true |
| seq1 within seq2 | seq1一定要包含在seq2中 |
| seq1 intersect seq2 | seq1和seq2要同時開始同時結束 |
| seq1 and seq2 | seq1和seq2要同時開始， |
| seq1 or seq2 | seq1或者seq2任意一個succeeds就succeeds |
| first match | 第一次匹配 |
| not | 表達式結果取反 |
| if else |
##m
延遲m個采樣時鍾，m可以是0或0以上的正整數
##[m:n]
延遲m到n之間的任意一個采樣時鍾都可，m可為0或任意正整數，n可為0或任意正整數也可直接用$表示極大值。
[*m]
重復m次出現，a ##1 b[*2]等效於 啊 ##1 b ##1 b，m為0或0以上正整數但不能為極大值$
[*m:n]
重復m到n之間的任意數次均可
[=m]
b[=m] ##1 c 表示b進行m次，間隔不連續個采樣時鍾周期，c在b最后一次發生后最小間隔一個時鍾后發生。
[=m:n]
b[=m:n] ##1 c 表示b進行m到n之間任意數次，間隔不連續個采樣時鍾周期，c在b最后一次發生后最小間隔一個時鍾后發生。
在特殊情況下如果m=0，n=$,結果為下圖，b可不發生，b也可和c同事發生
[->m]
b [->m] ##1 c 表示b進行m次，間隔不連續個采樣時鍾周期，c在b最后一次發生后間隔一個時鍾后發生。
[->m:n]
b[=m:n] ##1 c 表示b進行m到n之間任意數次，間隔不連續個采樣時鍾周期，c在b最后一次發生后間隔一個時鍾后發生。
[=m]和[->m]、[=m:n]和 [->m:n]之間的區別
區別在於在使用[=m]、[->m]、[=m:n]、 [->m:n]后如果接一個##1 c，則c是在最小間隔一個時鍾還是正好間隔一個時鍾周期上。
sig1 throughout seq1
在sig1匹配的時間內seq1一定是匹配的。
seq1 within seq2
seq1一定發生的比seq2晚，結束的seq2早。處於seq2滿足的內部。
seq1 and seq2
seq1和seq2是同時發生的，在seq1和seq2全通過時斷言才是通過。
seq1 or seq2
seq1和seq2同時發生，只要seq1和seq2中的一個通過，則斷言通過。
seq1 intersect seq2
seq1和seq2一定是同時開始同時結束的，存在不匹配則斷言失敗。
first_match
第一次匹配事件。下圖的斷言為d發生后第一次發生bc事件的下一個時鍾周期a是上升沿則斷言通過。
not
對發生的事件結果取反。
if else
條件判定，用法和systemverilog相同。
驗證人員如何對dut內部信號進行斷言驗證
1.可使用層級關系 . 的方法引用dut的內部信號，如要想使用if_stage_i內部的instr_rvalid_i信號可以通過dut_wrap.cv32e40p_wrapper_i.core_i.if_stage_i.instr_rvalid_i，（不推薦，編譯存在層級關系而且一旦例化位置變化，驗證平台代碼也需作出調整）
2.定義一個斷言module，將dut的模塊和斷言module綁定，關鍵字為bind，其中
cv32e40p_wrapper ：是dut中的模塊名
uvma_obi_assert ：是驗證平台中的斷言模塊名
obi_data_assert_i ：是斷言模塊的例化名，
bind cv32e40p_wrapper uvma_obi_assert#( .ADDR_WIDTH(32), .DATA_WIDTH(32) ) obi_data_assert_i(.clk(clk_i), .reset_n(rst_ni), .req(data_req_o), .gnt(data_gnt_i), .addr(data_addr_o), .be(data_be_o), .we(data_we_o), .wdata(data_wdata_o), .rdata(data_rdata_i), .rvalid(data_rvalid_i), .rready(1'b1) );
斷言模塊使用范例
module uvma_obi_assert import uvm_pkg::*; #( parameter int ADDR_WIDTH=32, parameter int DATA_WIDTH=32 ) ( input clk, input reset_n, input req, input gnt, input [ADDR_WIDTH-1:0] addr, input we, input [DATA_WIDTH/8-1:0] be, input [DATA_WIDTH-1:0] wdata, input [DATA_WIDTH-1:0] rdata, input rvalid, input rready ); // --------------------------------------------------------------------------- // Local variables // --------------------------------------------------------------------------- string info_tag = "CV32E40P_OBI_ASSERT"; // --------------------------------------------------------------------------- // Clocking blocks // --------------------------------------------------------------------------- // Single clock, single reset design, use default clocking default clocking @(posedge clk); endclocking default disable iff !(reset_n); // --------------------------------------------------------------------------- // Begin module code // --------------------------------------------------------------------------- // R-3.1.1 : Address phase signals stable during address phase property p_addr_signal_stable(sig); req ##0 !gnt |=> $stable(sig); endproperty : p_addr_signal_stable a_addr_stable: assert property(p_addr_signal_stable(addr)) else `uvm_error(info_tag, "addr signal not stable in address phase") a_we_stable: assert property(p_addr_signal_stable(we)) else `uvm_error(info_tag, "we signal not stable in address phase") a_wdata_stable: assert property(p_addr_signal_stable(wdata)) else `uvm_error(info_tag, "wdata signal not stable in address phase") a_be_stable: assert property(p_addr_signal_stable(be)) else `uvm_error(info_tag, "be signal not stable in address phase") // R-3.1.2 : Req may not deassewrt until the gnt is asserted property p_req_until_gnt; req ##0 !gnt |=> req; endproperty : p_req_until_gnt a_req_until_gnt : assert property(p_req_until_gnt) else `uvm_error(info_tag, "req may not deassert until gnt asserted") // R-7 At least one byte enable must be set property p_be_not_zero; req |-> be != 0; endproperty : p_be_not_zero a_be_not_zero : assert property(p_be_not_zero) else `uvm_error(info_tag, "be was zero during an address cycle") // R-7 All ones must be contiguous in writes reg[3:0] contiguous_be[] = { 4'b0001, 4'b0011, 4'b0111, 4'b1111, 4'b0010, 4'b0110, 4'b1110, 4'b0100, 4'b1100, 4'b1000 }; bit be_inside_contiguous_be; always_comb begin be_inside_contiguous_be = be inside {contiguous_be}; end property p_be_contiguous; req |-> be_inside_contiguous_be; endproperty : p_be_contiguous a_be_contiguous : assert property(p_be_contiguous) else `uvm_error(info_tag, $sformatf("be of 0x%0x was not contiguous", $sampled(be))); // R-8 Data address LSBs must be consistent with byte enables on writes function bit [1:0] get_addr_lsb(bit[3:0] be); casex (be) 4'b???1: return 0; 4'b??10: return 1; 4'b?100: return 2; 4'b1000: return 3; endcase endfunction : get_addr_lsb property p_addr_be_consistent; req |-> addr[1:0] == get_addr_lsb(be); endproperty : p_addr_be_consistent a_addr_be_consistent: assert property(p_addr_be_consistent) else `uvm_error(info_tag, $sformatf("be of 0x%01x not consistent with addr 0x%08x", $sampled(be), $sampled(addr))); // Cover that grant is asserted when unrequested property p_unrequested_gnt; !req ##0 gnt; endproperty : p_unrequested_gnt c_unrequested_gnt: cover property(p_unrequested_gnt); endmodule : uvma_obi_assert