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