一：初實assertion
斷言就是一段描述設計期望行為的代碼。 目前， 對斷言的使用主要在於仿真， 但斷言的能力不僅僅如此。 斷言是基於一些更加基礎的信息， 我們稱之為屬性 （ Ｐｒｏｐｅｒｔｙ）， 屬性可以用來作為斷言、 功能覆蓋點、 形式檢查和約束隨機激勵生成。
斷言可以嵌入到設計當中， 也可以在設計以外通過綁定鏈接到不同的設計點中。 斷言查找期望的特定事件序列， 或者說是在特定時鍾周期內的事件。 這些操作其實可以通過一個狀態機來實現， 設計工程師也可以通過硬件設計語言來實現， 但是這種方法不利實現，難以調試和維護。 因此， 為了提高斷言 的 效 率， 針 對 斷 言 描 述 的 標 准 語 言 （ 如 ＰＳＬ 和ＳＶＡ）， 被用戶廣泛采用。
斷言有一個重要的作用就是可以提高對設計的可見度。 它能夠幫助定位錯誤的根源， 以保證調試能更加容易和快速地進行。 這是因為斷言可以分布在設計
的各個重要部位， 能及時捕捉與設計屬性不一致的行為。 斷言可以應用在白盒調試或者黑盒調試兩種方式中， 一般情況下， 白盒調試會被設計工程師采用， 而黑盒調試會與驗證工程師比較相關。
那么， 我們有哪些方式可以支持斷言呢？ 第一， 我們可以采用預建的斷言庫， 如 ＯＶＬ； 第二， 用戶可以自定義斷言， 例如采用 ＳＶＡ 或者 ＰＳＬ。 在此， 我們優先推薦采用斷言庫， 而不建議用 戶學習斷言詳盡的語法， 從而自定義斷言。 為什么呢？
１） ＳＶＡ 和 ＰＳＬ 雖然是專門提供給用戶定義斷言的編程語言， 其優點是語法簡練； 其缺點是在簡練的語法下全面地表達特定的、 復雜的電路行為， 對語法或者電路行為理解不深刻的人， 很難寫出比較有實用價值的斷言。
２） 斷言是設計屬性的表現， 也就是采用 ＳＶＡ 和 ＰＳＬ 表示出來的是設計的意圖， 這就存在證明斷言代碼是否正確的過程； 斷言沒有辦法自我證明， 那么只能通過檢視 （ ｒｅｖｉｅｗ）和設計仿真過程中的相互驗證， 也就是在這個調試過程中， 可能是設計上的錯誤， 也可能是斷言寫錯了， 或許你大部分的時間不是在調試設計， 而是在調試斷言本身。
３） 驗證對於調試周期有很高的要求， 為了縮短驗證周期， 首先， 我們需要能更快地暴露錯誤的行為， 這個可以通過隨機激勵生成， 通過大量的隨機數據測試盡可能多地設計空間； 其次， 在錯誤暴露的時候， 我們如何定位到這個錯誤， 斷言就是在這個階段起作用，若我們能夠采用已經被驗證過的斷言庫， 我們就可以遵從驗證重用的思想， 做到實實在在的提高驗證效率。
綜上所述， 為了縮短調試周期， 我們要有采用斷言的思想， 而不是陷入在長篇累牘的斷言語法中。簡單來說，assertion用於更容易地debug
二：SVA的語法層次結構
1：最底層是布爾表達式， 這個和 verilog中沒有差別；
2：第二層是序列 （ ｓｅｑｕｅｎｃｅ）， 其中可以包含一些新的操作符， 如＃＃時隙延遲、 重復操作符、 序列操作符等， 序列是一個封裝格式， 采用序列封裝后可以在不同地方使用， 一個序列會被評估為真或者假；
3：第三層是屬性 （ ｐｒｏｐｅｒｔｙ）， 這是重要的封裝方式，其中最 重 要 的 特 點 是 屬 性 內 部 可 以 定 義 蘊 涵 操 作 符（ ｜ －＞ 、 ｜ ＝＞ ）。
4: 第四層是斷言指示層， 也就是采用 ａｓｓｅｒｔ對特定屬性或者序列做行為檢查， 或者采用assum或者采用 ｃｏｖｅｒ 做統計等。
5: 第五層是斷言的最后封裝， 只有通過最后封裝成一個單元的斷言才可以在不同的地方重用， 就如同一個可以例化模塊或者類， 通常這一層可以通過 ｍｏｄｕｌｅ 或者ｐｒｏｇｒａｍ、 ｉｎｔｅｒｆａｃｅ 來封裝
SVA包含兩種Assertion：立即斷言（Immediate Assertion），沒有任何時序概念的斷言為立即斷言，主要用於組合邏輯電路中。可調用$error,$fatal等
並行斷言（Concurrent Assertion），是基於周期采樣的，可跨時鍾周期的。我們下面主要介紹並行斷言
三：assertion里的重要名詞
1：SVA：SystemVerilog Assertion
2：ABV: Assertion Based Verification
3：CDV:Coverage Driving Verification
四：關鍵字
1：property：驗證設計意圖，內部可包含sequence
2：sequence：將一個序列做出來，包含很多場景，比如reset等
3：thread：事件相關的一個序列，可持續一拍或者多拍，每個thrad相互獨立。SVA在每個時鍾間隙進行asssert/assume/covered
4：##n
延遲n個周期
5：[m:n] /##[m:n]
[m:n] : m-n的任意一個周期
##[m:n] : ##m - ##n的任意一個周期
6：|->
首先對前置表達式做檢查，不成立則不激發后置表達式；成立，在同一個時鍾周期檢查后置表達式是否滿足要求。用於property
7：|=>
首先對前置表達式做檢查，不成立則不激發后置表達式；成立，在下一個時鍾周期檢查后置表達式是否滿足要求。用於property
|=>表示要延遲一個周期，相當於 |->##1
五：property
1：初識
可使用assert，assume，cover進行check；
可定義在module，interface，clocking block，package里；
2：格式舉例
property對設計進行描述，用assert進行check
波形
在clk上升沿，check信號request為1時（圖中標注request的T1處），clk的下一個周期處，check信號acknowledge是否拉高（圖中標注acknowledge的T1處），可知拉高，在clk的再下一個周期處，同理check信號data_enable是否拉高...可知T1成功，T2失敗。
3：assert/assume/cover
assert: check rtl
assume: check testbench
cover: coverage統計
如果a=2，disable 這個property，否則，執行 not @clk(b ##1 c);
4: implication (|-> |=>)
5: define
可對已經定義過的property進行define宏定義操作 ，再次使用時較為簡便。 ？？可是直接使用property的名字不是也可以嗎？
6：可使用not，or，and操作，可含有if else
7：可包含property，sequence，可遞歸
8：用於多時鍾
這里的##1是指當sig0=1時，clk0的下一拍后的clk1的上升沿
但是在跨時鍾時，當前拍只能操作一個時鍾，即一個thread里只能操作一個時鍾，如下
在clk0時鍾范圍內，當前拍又對clk1操作，這是不合法的操作。
六：sequence
1：初識
提供描述時序的一種方式，主要是線性順序；sequence內可嵌套sequence
2：例子
波形
3：sequence的其它關鍵字
##[0:$] : 0個周期到最后一個周期
[*n] : 續n次；例如：b[*3:4] 連續三次或者四次
[->n] : goto，連續重復 ； 例如
，b先拉低一拍，再拉高一拍,2次；再如：b[->2:10] b先拉第一拍，再拉高一拍，2次-10次皆可
[=n] :非連續重復；例如
，b先拉低一拍，再拉高一拍，重復兩次，最后以拉低結尾
$sample ：采樣值
$rose : 采下降沿
$fell : 采下降沿
$satble : 表達式沒變，返回1，改變，返回0；
$past : 采過去的前一個周期的值
and /intersect ：相當於與操作，但兩者有區別
or ：或操作
4：sequence函數
（1）first_match(t2) :第一次成功匹配t2
（2）throughout
橫跨多個周期，前置值都要滿足
主要塊要重復七拍，而burst_mode在拉低后的第六拍后即拉高，所以不滿足，fail。
（3）ended
在rule里，e1.ended先執行e1的末尾語句，##1 proc2，然后依次向前執行