過度約束正式的財產(chǎn)驗證（FPV）會有什么影響

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

約束

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

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

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

過度和不足約束

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

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

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

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

過度約束正式環(huán)境是一個更大的問題，因為它可能隱藏設(shè)計中的錯誤。實際上，您沒有像您認(rèn)為的那樣進(jìn)行驗證。例如，假設(shè)乘數(shù)可以乘以正數(shù)和負(fù)數(shù)，但驗證工程師誤解了規(guī)范并寫入約束以將A和B限制為> = 0.假設(shè)乘數(shù)有效，則上面的屬性將通過，并且您認(rèn)為驗證已完成，因為所有屬性都已通過。

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

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

沖突約束

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

相等：假設(shè)屬性

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