過(guò)度約束正式的財(cái)產(chǎn)驗(yàn)證（FPV）會(huì)有什么影響

正式性能驗(yàn)證（FPV）越來(lái)越多地用于補(bǔ)充片上系統(tǒng)（SoC）驗(yàn)證的仿真。將FPV添加到您的驗(yàn)證流程可以大大加快驗(yàn)證關(guān)閉并發(fā)現(xiàn)棘手的案例錯(cuò)誤，但了解這些技術(shù)之間的差異非常重要。主要區(qū)別在于FPV使用屬性，即斷言和約束，而不是測(cè)試平臺(tái)。斷言也用于模擬，但約束的作用是不同的。理解約束對(duì)于成功使用FPV是必要的。

約束

約束游戲在FPV中發(fā)揮核心作用。它們定義了對(duì)被測(cè)設(shè)計(jì)的法律刺激，即可以達(dá)到的狀態(tài)空間。斷言定義了DUT對(duì)法律激勵(lì)的期望行為。

約束描述了如何允許DUT的輸入表現(xiàn)，應(yīng)該采用什么值以及輸入之間的時(shí)間關(guān)系。約束可以被認(rèn)為是模擬中的刺激。在約束隨機(jī)模擬中，約束求解器為下一個(gè)周期生成滿(mǎn)足所有約束的輸入向量。它將繼續(xù)在刺激周期之后產(chǎn)生循環(huán)直到模擬結(jié)束，或直到它達(dá)到無(wú)法產(chǎn)生法律刺激的情況。

相比之下，形式驗(yàn)證的約束可以描述，例如，如何在給定的協(xié)議中合法溝通。

過(guò)度和不足約束

編寫(xiě)精確描述所有法律刺激的約束很難并且通常是不可取的。這意味著正式環(huán)境要么不受約束，要么過(guò)度約束。約束不足意味著對(duì)精確建模刺激所需的約束要少。這意味著一些潛在的非法輸入將被驅(qū)動(dòng)到被測(cè)設(shè)備（DUT）。過(guò)度約束意味著存在比所需更多的約束，并且不允許所有合法行為。

略微受限制的環(huán)境通常是最好的方法。許多設(shè)計(jì)可以處理規(guī)范中未定義的輸入和行為，如果使用的約束更少，則將驗(yàn)證設(shè)計(jì)中更大的狀態(tài)空間。約束不足的環(huán)境可能會(huì)導(dǎo)致斷言失敗，如果是這種情況，則需要添加其他約束。例如，假設(shè)我們有一個(gè)4位乘法器來(lái)驗(yàn)證：

規(guī)范說(shuō)它可以乘以正整數(shù)A和B> 0，但是驗(yàn)證工程師假定A和B> = 0.約束和檢查乘數(shù)的斷言很簡(jiǎn)單：

如果在這種情況下證明了該屬性 - 對(duì)于A和B中的任何一個(gè)或兩個(gè)都為零以及正整數(shù) - 那么顯然它將保持A和B僅大于零。約束允許其他行為，這意味著環(huán)境受到限制。較少的約束通常也會(huì)改善正式工具的運(yùn)行時(shí)間。如果屬性通過(guò)，我們不必再擔(dān)心欠約束情況了。

過(guò)度約束正式環(huán)境是一個(gè)更大的問(wèn)題，因?yàn)樗赡茈[藏設(shè)計(jì)中的錯(cuò)誤。實(shí)際上，您沒(méi)有像您認(rèn)為的那樣進(jìn)行驗(yàn)證。例如，假設(shè)乘數(shù)可以乘以正數(shù)和負(fù)數(shù)，但驗(yàn)證工程師誤解了規(guī)范并寫(xiě)入約束以將A和B限制為> = 0.假設(shè)乘數(shù)有效，則上面的屬性將通過(guò)，并且您認(rèn)為驗(yàn)證已完成，因?yàn)樗袑傩远家淹ㄟ^(guò)。

過(guò)度約束只是無(wú)意中的問(wèn)題。故意過(guò)度約束是將設(shè)計(jì)驗(yàn)證分解為案例的有用方法。一個(gè)例子是驗(yàn)證存儲(chǔ)器控制器。首先限制刺激只做寫(xiě)事務(wù)，然后限制它只做讀事務(wù)。這些情況中的每一種都明顯過(guò)度約束。

在第一種情況下，不允許讀取合法事務(wù)的事務(wù)，在第二種情況下，不允許寫(xiě)入事務(wù)。這不是問(wèn)題，因?yàn)檫@兩個(gè)案例共同涵蓋了所有法律刺激。在這種情況下，只有一個(gè)案例被行使而不是另一個(gè)案例，導(dǎo)致驗(yàn)證工程師認(rèn)為已經(jīng)完成了驗(yàn)證。故意過(guò)度約束的風(fēng)險(xiǎn)是錯(cuò)過(guò)了合法的輸入值，并且未驗(yàn)證諸如讀取后寫(xiě)入的序列（在存儲(chǔ)器控制器的情況下）。

沖突約束

約束限制了在正式屬性驗(yàn)證中探索的輸入集和狀態(tài)空間。如果驗(yàn)證環(huán)境具有相互沖突的約束或設(shè)計(jì)中的語(yǔ)句，則不可能有合法的輸入，并且設(shè)計(jì)中的任何狀態(tài)空間都不可訪問(wèn)。例如，下面的兩個(gè)約束可以單獨(dú)滿(mǎn)足，但它們一起產(chǎn)生沖突：

相等：假設(shè)屬性

沖突約束可以被視為過(guò)度約束環(huán)境的最極端形式，受到如此限制沒(méi)有合法的投入。這意味著沒(méi)有斷言可以失敗，實(shí)際上是因?yàn)闆](méi)有進(jìn)行檢查。這類(lèi)似于說(shuō)我的測(cè)試用例沒(méi)有在模擬中失敗，原因是你沒(méi)有執(zhí)行任何測(cè)試用例。該陳述是正確的，但它在驗(yàn)證完整性方面具有誤導(dǎo)性。