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

約束

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

約束描述了如何允許DUT的輸入表現，應該采用什么值以及輸入之間的時間關系。約束可以被認為是模擬中的刺激。在約束隨機模擬中，約束求解器為下一個周期生成滿足所有約束的輸入向量。它將繼續在刺激周期之后產生循環直到模擬結束，或直到它達到無法產生法律刺激的情況。

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

過度和不足約束

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

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

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

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

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

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

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

沖突約束

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

相等：假設屬性

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