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