Formal Verification(正規驗證)介紹和如何使用 SVA(System Verilog Assertion) 做驗證
(零)前提:
關於 Formal Verification，其實我也還不是很理解，而且資源也不是那麼多，尤其很多都只是觀念性的介紹，甚至寫得很艱澀難懂落落長，但沒實質提到該怎麼做 Formal Verification。
但據說驗證在 IC 設計上又是非常重要的，所以雖然這部分真的不好理解，還是硬著頭皮收集資料寫下這一篇，所以這篇也不會寫到太深，畢竟這整個要講起來是很專業領域的。
因此這篇適用於對 Formal Verification 完全不理解的人，希望可以幫助你入門。
(一)正文:
當我們完成一塊電路時，要怎麼確定功能跟預期的結果是一樣的？
1. 在軟體內跑 Waveform，比對預期結果和實際結果
(1) 有 GUI，淺顯易懂
(2) 新手友善
2. 寫 Testbench，比對預期結果和實際結果
(1) 許多參數要自己設定
(2) 需要下點功夫才能理解
上述方法都是把所有的 Case 會產生的結果用手寫出來，然後再用人眼去比對每個預期結果和實際結果是不是一樣。
但此時問題來了，但如果今天有上千個 Case，還是只能靠我們自己把這上千個 Case 列出來，然後一一用人眼比對嗎？
此時 Formal Verification 的功用就出來了！
簡單來說它就是把你電路該有的行為列成正規化的公式
然後再用一個檢查器去確認你的電路的行為總是會跟這個公式所描述的行為是一樣的
這部分對於一個新手來說可能真的會很 Hardcore
不過會了之後真的會變得很方便！
Functional Verification
把所有 Testcase 列出來然後作驗證。
Formal Verification
(二)實驗:
安裝:
yosys
symbiyosys
gtkwave
yices
sudo apt-get install autoconfig lubgmp3-dev (Ubuntu)
sudo yum install autoconfig lubgmp3-dev (CentOS，不過沒實際試過，只是猜測應該是這樣)
以上東西要怎麼裝，Google 就可以查到了
我本身的環境是使用 CentOS7，在安裝過程中也碰到蠻多坑的
(雖然後來還是自己裝好了，只是真的會蠻麻煩的，很考驗你對整個環境的熟悉度)
所以如果你也一直裝不好，或是你就是個懶人，
沒關係，直接裝免費的 OSS CAD Suite 就好了！
以上要裝的東西都已經裝好在裡面了
所以你只需要去下載網站找到對應的版本
下載下來解壓縮
然後設定好環境路徑就好了 (不會裝的可以參考最下面簡易教學)
而裝好後若要測試有沒有安裝成功
網站上也有提供 FIFO Buffer 使用範例
在你安裝下來的資料夾底下有個 examples/fifo
在該資料夾裡頭執行 sby fifo.sby 應該要可以成功跑起來並且 PASS 的
確認環境可以正常運行後，就可以開始熟悉語法了！
(四)語法介紹
這邊要介紹 SVA (SystemVerilog Assertion)
這部分真的沒那麼好懂
我也是每篇文章東湊西湊著參考才好不容易大概理解
並統整成以下內容
首先先對三個名詞有個概念
Assert: 特定狀態下，Output 一定會是這個答案
Assume: 限制輸入資料的可能性
Cover: Output 可以得到這個答案
Assert
然後先從 Assert 介紹起
Assertion 分為兩種
1. 立即性 (Immediatly) 的: 不管 clk 有沒有正緣觸發，持續地在 check 該 Assertion 必須成立
2. 時序性 (Concurrent) 的: 只在 clk 有正緣觸發的時候，才 check 該 Assertion 是否成立
(所以前者類似組合電路的概念，後者類似時序電路的概念)
立即性 Assertion
語法:
Assetion_Name: Assert(Condition)
(藍色部分可以自己定義)
範例:
A_IS_TRUE: Assert(A) //A 訊號在此電路中必須恆為真
B_EQUAL_TO_10: Assert(B==10) //B 訊號在此電路中必須恆等於 10
時序性 Assertion
語法:
1.
property PropertyName
@(posedge clk)
Event;
endproperty
AssertionName: assert property (PropertyName)
2.
sequence SequenceName
Event;
endsequence
property PropertyName
@(posedge clk)
SequenceName;
endproperty
AssertionName: assert property (PropertyName)
(藍色部分可以自己定義)
語法 2. 多了 Sequence 區塊
Sequence 是專門用來定義事件的
並且在每個時序都會檢查這個事件是否成立
當 Property 裡頭定義的 Event 很複雜的時候
我們可以把 Event 寫到 Sequence 區塊
幫助我們增加程式易讀性
語法1. 的範例:
property PROPERTY_A
@(posedge clk)
~A; // A 的內容再正緣觸發時皆為0
endproperty
ASSERT_A: assert(PROPERTY_A)
property PROPERTY_B
@(posedge clk)
//只要 Enable 為1，B 的內容在下一個正緣觸發時必須遞增
Enable |-> #1 B == $past(B) + 1;
endproperty
ASSERT_B: assert property PROPERTY_B
上面 B_INCREASE 範例中紅色的部分你可能看不懂
或是你已經從註解猜到那些符號是什麼意思了
但不管如何，等等會再詳細介紹這些語法
到這裡為止，你只需要先了解立即和時序的 assertion 的差別
並且大概知道該怎麼用文字描述你要檢查的 Condition 或 Event
語法2. 的範例:
sequence SEQUENCE_B
Enable |-> #1 B == $past(B) + 1; //只要 Enable 為1，B 的內容在下一個正緣觸發時必須遞增
endsequence
property PROPERTY_B
@(posedge clk) SEQUENCE_B;
endproperty
ASSERT_B: assert property PROPERTY_B
從上面觀察語法
立即性 Assertion 和時序性 Assertion 有個差別在於
立即性的電路不會有 property
有時序性的電路則會有 property
語法
延遲 N 個 clock cycle 時
##N
延遲 N~M 個 clock cycle 內
##[N:M]
Event A 發生的時候，Event B 必須成立
(overlapping implication)
(Event A) |-> (EventB)
包含當前 Cycle
Event A 發生的時候，在下個 Cycle，Event B 必須成立
(nonoverlapping implication)
(Event) |=> (Event)
不包含當前 Cycle
Event A 發生的時候，N 個 Cycle 後 Event B 必須成立
(Event A) |-> ##N (EventB)
(Event A) |=> ##N-1 (EventB)
(這兩個建議可以挑一種寫就好了，以維持程式的一致性，你自己也不會混亂)
Event A 發生的時候，N~M 的 Cycle 內 Event B 必須成立
(Event A) -> ##[N:M] (EventB)
訊號 A 為 High
$rose(A)
訊號 A 為 Low
$fall(A)
訊號 A 沒有改變
$stable(A)
前一個 Cycle 的 A
$past(A)
前 N 個 Cycle 的 A
$past(A,N)
看完這些語法，你大概迫不及待想要在你的 .sv 檔案裡頭試試看了
但是當你加上 property，執行 sby 時又會跟你說不認識這個語法
看了一下 examples 資料夾裡頭有用到的地方
原來是要在 sby 裡頭 script 區域加上 read -verific
重新執行 sby 時又跟你說 yosys 不支援 verific
查了一下，似乎只能購買他們付費 EDA 軟體才能支援
所以目前也還在找有沒有其他可以讓這些 property 語法跑起來的 tools
(五)附錄
參考資料:
A Gentle Introduction to Formal Verification
SymbiYosys (sby) Documentation
Very Basic Introduction to Formal Verification
環境路徑簡易教學 (CentOS7):
sudo vim ~/.bashrc (打開環境變數設定檔)
...檔案內容...
export OSSCAD=<your/path/to/oss-cad-suite> (導到你安裝該 TOOL 的路徑)
PATH = (Here is Origin Content):$OSSCAD/bin (在 PATH 後面加上 :$OSSCAD/bin)
.....................
source ~/.bashrc (使環境變數設定檔生效)
或是直接重開 Terminal 也可以
Error 處理:
執行 sby 時遇到問題
1. 有缺模組
解法: 上網找怎麼裝模組
2. File "<fstring>", line 1 SyntaxError: invalid syntax
解法: 安裝 python3.8 並用 python3.8 執行
(這是由於 3.6 和 3.7 不支援這樣的語法)
參考: PythonL: invalid syntax file "<fstring>", line 1
想要在 sv 檔案裡頭用 property 語法
於是在 sby 裡頭 script 區域加上 read -verific
(沒有加的話是無法執行的)
1. ERROR: Command syntax error: This version of Yosys is built without Verific support.
解法: 暫時沒有解法，官方給的解法是要購買他們的 EDA Tools
參考: https://github.com/YosysHQ/yosys/blob/master/frontends/verific/verific.cc (2567行)
留言
張貼留言