斷言采用形式語義進行編寫,可以通過使用軟件工具驗證其正確性。形式語義使得工程師能以簡單和精確的方式描述復雜的設計屬性,并檢測難以發現和邊界條件下的缺陷,從而減少了設計師對使用仿真工具檢查功能正確與否的依賴性。

驗證工程師在規范級創建斷言,而設計師在架構級創建斷言。如果設計用的是SystemVerilog,那么這些斷言可以用SystemVerilog Assertions編寫。當設計采用獨立的硬件描述語言(如VHDL或Verilog)時,斷言也可以用屬性規范語言(PSL)編寫。

可以使用仿真環境和形式環境來驗證斷言的正確性。當覆蓋了設計規范的所有要點時,設計人員就知道他們已經編寫了足夠的斷言。

建議

. 從測試計劃開始。計劃是由驗證環境的重要部分組成的一份文件。它能監視驗證過程的功能覆蓋,并提供對測試平臺和激勵信號質量的反饋。然后嘗試使用這些節省時間的技術:

1. 與編寫RTL代碼一起編寫斷言,因為這樣做有助于在任何其它形式的驗證之前識別缺陷。

2. 編寫簡單的斷言。越簡單越容易理解和調試。

3. 將斷言與要驗證的設計代碼盡量放在一起,以便明確使用斷言驗證的設計意圖。

4. 每個斷言都要邊開發邊測試,這樣可以縮短調試時間。

5. 給斷言命名。這樣可以減少與調試斷言條件故障相關的工作量。

6. 將相似的斷言歸類到斷言庫中以增加重復使用能力。當設計含有大量復用組件時這一點特別有用。

. 提高抽象等級以簡化驗證過程。

. 測量功能覆蓋率,它能讓你評估驗證工作的質量。功能覆蓋率工具將斷言規范作為其輸入,輸出有關檢查、情景和數據方面的信息。

. 歸檔已經認識的問題。已經識別出缺陷的歸檔技術可以提供驗證過程效率方面的有關信息供日后項目使用。

圖:合理使用斷言可削減驗證時間,加速設計周期。  

不建議

. 使用“活躍”屬性,因為對活躍屬性的仿真從來不會失敗,從而導致真正問題被錯漏的假陽性情況。活躍屬性在經過一段不定的時間后會變為真,或隨著時間的推移而不受控制。也就是說,如果證實了信號“req”,那么今后某個時間信號“ack”會被證實。

. 使用空的真斷言,這也會導致假陽性局面。例如,某個斷言是這樣寫的:如果A發生了,B就會發生。但如果設計中A從來不會觸發,那B就永遠不會被測試到。

. 綜合斷言。斷言不應該出現在綜合過的網表中。設計師可以將編譯指示(translate_off/translate_on)放在斷言旁邊,這樣綜合工具就能忽略掉斷言。設計師也可以使用“ifdef”宏來激活或去激活斷言。如果設計師使用了斷言庫,那么他或她應該將這個宏插入斷言庫以便減少工作量。

. 用斷言做重復檢查。避免為已經用其它驗證技術測試過的特性再增加斷言內容。

. 使用斷言驗證所有設計特性,因為這樣做會提高增加斷言帶來的總體成本。可以避免使用斷言的一些設計特性有:

1. 自動振蕩時鐘。

2. 毛刺檢測。

3. 重復RTL代碼的斷言代碼。無需為變化值為1的加法或減法計數器準備斷言。

4. 已知正確的元件,如D觸發器或2:1復用器。

作者:Vinima Aggarwal

應用工程師

Verific Design Automation公司