ot;display: block;">硬件設(shè)計(jì)師和驗(yàn)證工程師都習(xí)慣使用斷言。斷言是從形式上規(guī)定設(shè)計(jì)意圖行為的一種方式,在設(shè)計(jì)過程中必須保持為真。斷言可以通過縮短驗(yàn)證時(shí)間而有效地提高整體設(shè)計(jì)產(chǎn)能。現(xiàn)在,工程師無(wú)需像傳統(tǒng)驗(yàn)證流程那樣,需要回到之前的仿真跟蹤和邏輯模塊中去確定錯(cuò)誤的真正原因,傳統(tǒng)的設(shè)計(jì)驗(yàn)證是在設(shè)計(jì)實(shí)現(xiàn)后進(jìn)行的。

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

驗(yàn)證工程師在規(guī)范級(jí)創(chuàng)建斷言,而設(shè)計(jì)師在架構(gòu)級(jí)創(chuàng)建斷言。如果設(shè)計(jì)用的是SystemVerilog,那么這些斷言可以用SystemVerilog Assertions編寫。當(dāng)設(shè)計(jì)采用獨(dú)立的硬件描述語(yǔ)言(如VHDL或Verilog)時(shí),斷言也可以用屬性規(guī)范語(yǔ)言(PSL)編寫。

可以使用仿真環(huán)境和形式環(huán)境來(lái)驗(yàn)證斷言的正確性。當(dāng)覆蓋了設(shè)計(jì)規(guī)范的所有要點(diǎn)時(shí),設(shè)計(jì)人員就知道他們已經(jīng)編寫了足夠的斷言。

建議

. 從測(cè)試計(jì)劃開始。計(jì)劃是由驗(yàn)證環(huán)境的重要部分組成的一份文件。它能監(jiān)視驗(yàn)證過程的功能覆蓋,并提供對(duì)測(cè)試平臺(tái)和激勵(lì)信號(hào)質(zhì)量的反饋。然后嘗試使用這些節(jié)省時(shí)間的技術(shù):

1. 與編寫RTL代碼一起編寫斷言,因?yàn)檫@樣做有助于在任何其它形式的驗(yàn)證之前識(shí)別缺陷。

2. 編寫簡(jiǎn)單的斷言。越簡(jiǎn)單越容易理解和調(diào)試。

3. 將斷言與要驗(yàn)證的設(shè)計(jì)代碼盡量放在一起,以便明確使用斷言驗(yàn)證的設(shè)計(jì)意圖。

4. 每個(gè)斷言都要邊開發(fā)邊測(cè)試,這樣可以縮短調(diào)試時(shí)間。

5. 給斷言命名。這樣可以減少與調(diào)試斷言條件故障相關(guān)的工作量。

6. 將相似的斷言歸類到斷言庫(kù)中以增加重復(fù)使用能力。當(dāng)設(shè)計(jì)含有大量復(fù)用組件時(shí)這一點(diǎn)特別有用。

. 提高抽象等級(jí)以簡(jiǎn)化驗(yàn)證過程。

. 測(cè)量功能覆蓋率,它能讓你評(píng)估驗(yàn)證工作的質(zhì)量。功能覆蓋率工具將斷言規(guī)范作為其輸入,輸出有關(guān)檢查、情景和數(shù)據(jù)方面的信息。

. 歸檔已經(jīng)認(rèn)識(shí)的問題。已經(jīng)識(shí)別出缺陷的歸檔技術(shù)可以提供驗(yàn)證過程效率方面的有關(guān)信息供日后項(xiàng)目使用。

圖:合理使用斷言可削減驗(yàn)證時(shí)間,加速設(shè)計(jì)周期。  

不建議

. 使用“活躍”屬性,因?yàn)閷?duì)活躍屬性的仿真從來(lái)不會(huì)失敗,從而導(dǎo)致真正問題被錯(cuò)漏的假陽(yáng)性情況。活躍屬性在經(jīng)過一段不定的時(shí)間后會(huì)變?yōu)檎?或隨著時(shí)間的推移而不受控制。也就是說(shuō),如果證實(shí)了信號(hào)“req”,那么今后某個(gè)時(shí)間信號(hào)“ack”會(huì)被證實(shí)。

. 使用空的真斷言,這也會(huì)導(dǎo)致假陽(yáng)性局面。例如,某個(gè)斷言是這樣寫的:如果A發(fā)生了,B就會(huì)發(fā)生。但如果設(shè)計(jì)中A從來(lái)不會(huì)觸發(fā),那B就永遠(yuǎn)不會(huì)被測(cè)試到。

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

. 用斷言做重復(fù)檢查。避免為已經(jīng)用其它驗(yàn)證技術(shù)測(cè)試過的特性再增加斷言內(nèi)容。

. 使用斷言驗(yàn)證所有設(shè)計(jì)特性,因?yàn)檫@樣做會(huì)提高增加斷言帶來(lái)的總體成本。可以避免使用斷言的一些設(shè)計(jì)特性有:

1. 自動(dòng)振蕩時(shí)鐘。

2. 毛刺檢測(cè)。

3. 重復(fù)RTL代碼的斷言代碼。無(wú)需為變化值為1的加法或減法計(jì)數(shù)器準(zhǔn)備斷言。

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

作者:Vinima Aggarwal

應(yīng)用工程師

Verific Design Automation公司