<del id="aymay"></del> 無論是在芯片測試還是在系統研發的過程中，工程師都需要進行嚴謹的形式驗證。通過這一方式可以及時找出錯誤節點，對系統優化具有重要作用。然而，如何才能真正的讓形式驗證成為自己研發工作的重要助力？為什么平時的工作中驗證過程就如同走流程一般枯燥？本文將會通過兩個方面的介紹，幫助你找到合理利用形式驗證的秘訣。
有界結果和無界結果具有同等意義
大多數情況下，當檢驗器沒有達到決定性結果的時候，驗證工程師會問我們該怎么辦。一個形式工具，可以返回三種不同的狀態：Pass代表運行正常。Fail意味著形式工具發現了故障，用戶可以根據所提供的反例進行調試。這兩個都是決定性的結果。第三類的名稱根據所使用的形式工具不同而有所區別——探索，未確定，尚無定論，或終止。聽起來好像都是不好的結果，但這些結果都是有意義的。
這類的結果表示需要的周期比所記錄的證明約束的周期短的話，形式工具無法找到這樣的錯誤。如果工具返回并記錄到一個20個周期的有界證明的不確定狀態，則用戶知道在小于20周期的設計中沒有錯誤。
形式驗證的重要一步，是證明對于給定DUT所要求的證明深度是合格的。有一個明確的方法來跟蹤計算所需的證明界限。一旦用戶計算所需的證明深度，那么所有不確定的結果被分成兩組。首先檢驗器達到所需的證明深度。另一種是檢驗器還沒有達到所需的深度證明。例如，所需的證明深度是30，但在形式工具的分析中只達到了20個周期。在這一點上，用戶會尋找可以用來達到所要求的證明深度的技術。大多數情況下，有一些可用的方法，比如使用抽象模型。
如果檢驗器達到所需的證明深處，有界結果和無界結果一樣好。如果用戶沒有得到無界證明，這并不意味著其結果是沒有意義的。
實現形式符號指令需要一個合理的方法
形式符號指令意味著形式化技術被給予了與驗證流程中模擬相同的權重。在形式是唯一用于驗證DUT的技術的模塊中，形式工程師與設計和驗證工程師被賦予了同等的責任和義務，以確保在設計中沒有錯誤。
為了實現形式符號指令，我們需要一個合理的方法。這意味著形式化測試平臺需要所有的端對端檢驗器覆蓋完整的設計功能。約束必須有效，而不會過度約束。抽象模型和其他復雜的解決方法都可能會用到，以確保所有檢驗器達到所要求的證明深度。形式覆蓋將被要求用于證明形式驗證結果。缺乏的任何一部分都會使形式驗證工作不完整，不能夠實現符號指令。
在采用形式符號指令項目之前，形式工程師應該了解如何才能實現形式符號指令。要掌握實現方法必須牢記四個C跳—檢驗器（checkers）、約束（constraints）、復雜度（complexity）以及覆蓋（coverage）。
結語
工程師通過對符號指令的合理設置以及對有界結果、無界結果的分析利用，能夠順利的通過形式驗證發現系統設計中的缺陷和有待改進之處，從而能夠讓形式驗證真正成為自己研發過程中的有力幫手。
