無論是在芯片測試還是在系統(tǒng)研發(fā)的過程中，工程師都需要進(jìn)行嚴(yán)謹(jǐn)?shù)男问津?yàn)證。通過這一方式可以及時(shí)找出錯誤節(jié)點(diǎn)，對系統(tǒng)優(yōu)化具有重要作用。然而，如何才能真正的讓形式驗(yàn)證成為自己研發(fā)工作的重要助力？為什么平時(shí)的工作中驗(yàn)證過程就如同走流程一般枯燥？本文將會通過兩個(gè)方面的介紹，幫助你找到合理利用形式驗(yàn)證的秘訣。

有界結(jié)果和無界結(jié)果具有同等意義

大多數(shù)情況下，當(dāng)檢驗(yàn)器沒有達(dá)到?jīng)Q定性結(jié)果的時(shí)候，驗(yàn)證工程師會問我們該怎么辦。一個(gè)形式工具，可以返回三種不同的狀態(tài)：Pass代表運(yùn)行正常。Fail意味著形式工具發(fā)現(xiàn)了故障，用戶可以根據(jù)所提供的反例進(jìn)行調(diào)試。這兩個(gè)都是決定性的結(jié)果。第三類的名稱根據(jù)所使用的形式工具不同而有所區(qū)別——探索，未確定，尚無定論，或終止。聽起來好像都是不好的結(jié)果，但這些結(jié)果都是有意義的。

這類的結(jié)果表示需要的周期比所記錄的證明約束的周期短的話，形式工具無法找到這樣的錯誤。如果工具返回并記錄到一個(gè)20個(gè)周期的有界證明的不確定狀態(tài)，則用戶知道在小于20周期的設(shè)計(jì)中沒有錯誤。

形式驗(yàn)證的重要一步，是證明對于給定DUT所要求的證明深度是合格的。有一個(gè)明確的方法來跟蹤計(jì)算所需的證明界限。一旦用戶計(jì)算所需的證明深度，那么所有不確定的結(jié)果被分成兩組。首先檢驗(yàn)器達(dá)到所需的證明深度。另一種是檢驗(yàn)器還沒有達(dá)到所需的深度證明。例如，所需的證明深度是30，但在形式工具的分析中只達(dá)到了20個(gè)周期。在這一點(diǎn)上，用戶會尋找可以用來達(dá)到所要求的證明深度的技術(shù)。大多數(shù)情況下，有一些可用的方法，比如使用抽象模型。

如果檢驗(yàn)器達(dá)到所需的證明深處，有界結(jié)果和無界結(jié)果一樣好。如果用戶沒有得到無界證明，這并不意味著其結(jié)果是沒有意義的。

實(shí)現(xiàn)形式符號指令需要一個(gè)合理的方法

形式符號指令意味著形式化技術(shù)被給予了與驗(yàn)證流程中模擬相同的權(quán)重。在形式是唯一用于驗(yàn)證DUT的技術(shù)的模塊中，形式工程師與設(shè)計(jì)和驗(yàn)證工程師被賦予了同等的責(zé)任和義務(wù)，以確保在設(shè)計(jì)中沒有錯誤。

為了實(shí)現(xiàn)形式符號指令，我們需要一個(gè)合理的方法。這意味著形式化測試平臺需要所有的端對端檢驗(yàn)器覆蓋完整的設(shè)計(jì)功能。約束必須有效，而不會過度約束。抽象模型和其他復(fù)雜的解決方法都可能會用到，以確保所有檢驗(yàn)器達(dá)到所要求的證明深度。形式覆蓋將被要求用于證明形式驗(yàn)證結(jié)果。缺乏的任何一部分都會使形式驗(yàn)證工作不完整，不能夠?qū)崿F(xiàn)符號指令。

在采用形式符號指令項(xiàng)目之前，形式工程師應(yīng)該了解如何才能實(shí)現(xiàn)形式符號指令。要掌握實(shí)現(xiàn)方法必須牢記四個(gè)C跳—檢驗(yàn)器（checkers）、約束（constraints）、復(fù)雜度（complexity）以及覆蓋（coverage）。

結(jié)語

工程師通過對符號指令的合理設(shè)置以及對有界結(jié)果、無界結(jié)果的分析利用，能夠順利的通過形式驗(yàn)證發(fā)現(xiàn)系統(tǒng)設(shè)計(jì)中的缺陷和有待改進(jìn)之處，從而能夠讓形式驗(yàn)證真正成為自己研發(fā)過程中的有力幫手。