為處理器驗(yàn)證創(chuàng)建一個(gè)“瑞士奶酪模型”，以保證高效的驗(yàn)證品質(zhì)！

為處理器驗(yàn)證創(chuàng)建一個(gè)“瑞士奶酪模型”，以保證高效的驗(yàn)證品質(zhì)！

所有的處理器都有著很高的品質(zhì)要求，其可靠性是處理器驗(yàn)證團(tuán)隊(duì)的主要關(guān)切。提供一流質(zhì)量的產(chǎn)品需要一個(gè)戰(zhàn)略性的、勤勉的和徹底的方法去實(shí)現(xiàn)。因此，處理器驗(yàn)證發(fā)揮著重要作用，它需要結(jié)合所有行業(yè)標(biāo)準(zhǔn)技術(shù)--而這就有點(diǎn)像心理學(xué)上的的瑞士奶酪模型（又稱Reason模型）原則。

我們強(qiáng)烈需要一個(gè)強(qiáng)大的、分層的處理器驗(yàn)證策略！

我在之前曾經(jīng)說(shuō)過(guò)：處理器驗(yàn)證是一門微妙的藝術(shù)。我們需要考慮到所有的不確定性，這意味著在優(yōu)化資源的同時(shí)開(kāi)放驗(yàn)證范圍。一方面，我們要在最終交付前找到所有的關(guān)鍵漏洞。另一方面，我們必須有一個(gè)高效的驗(yàn)證策略來(lái)滿足上市時(shí)間的硬性要求。交付智能處理器驗(yàn)證意味著在產(chǎn)品開(kāi)發(fā)過(guò)程中盡可能有效地、盡早地找到有意義的bug。實(shí)現(xiàn)這一目標(biāo)的方法之一是結(jié)合所有行業(yè)標(biāo)準(zhǔn)的驗(yàn)證技術(shù)。而正是通過(guò)創(chuàng)建冗余，最終找到并擊敗所有關(guān)鍵bug。

不同類型的bug都有一個(gè)復(fù)雜性--或bug評(píng)分--這取決于觸發(fā)bug所需的事件數(shù)量和類型。有些可能是用覆蓋率發(fā)現(xiàn)的，而有些是用形式證明發(fā)現(xiàn)的。想象一下，如果將”瑞士奶酪模型”應(yīng)用于處理器驗(yàn)證。每一片奶酪都象征著一種驗(yàn)證技術(shù)，它有一些特定的優(yōu)勢(shì)來(lái)捕捉特定類型的bug。漏洞逃脫并進(jìn)入最終交付物的風(fēng)險(xiǎn)通過(guò)不同層次和類型的驗(yàn)證來(lái)減輕，而這些驗(yàn)證是相互分層的。

在應(yīng)用于處理器驗(yàn)證的瑞士奶酪模型中，其原理類似于航空業(yè)：如果有一條直接穿過(guò)所有切片的路徑，那么飛機(jī)就有墜毀的風(fēng)險(xiǎn)。這就是為什么航空業(yè)對(duì)程序、飛行檢查單和冗余系統(tǒng)要求嚴(yán)格？我們的目標(biāo)是增加更多的切片，減少每一個(gè)切片上的孔的大小，直至最后沒(méi)有任何縫隙可以穿過(guò)，此時(shí)一個(gè)高質(zhì)量的處理器正式完成。

應(yīng)用于處理器驗(yàn)證的瑞士奶酪模型原則

通過(guò)驗(yàn)證方法（以瑞士奶酪模型為例）：

首先需要?jiǎng)?chuàng)建冗余，以確保在其中一個(gè)layer上失敗時(shí)的連續(xù)性。

當(dāng)在開(kāi)發(fā)過(guò)程中發(fā)現(xiàn)bug時(shí)，表明漏洞出現(xiàn)在了其中的幾片奶酪上。因此，我們可以改進(jìn)幾種驗(yàn)證方法，以減少每片奶酪上的漏洞大小。利用這種方法，無(wú)論是簡(jiǎn)易簡(jiǎn)單的漏洞還是復(fù)雜的終極漏洞，都可以增加擊中bug的幾率。

最大限度地發(fā)揮每種驗(yàn)證技術(shù)的潛力。

每個(gè)分片上的孔就是驗(yàn)證方法中的一個(gè)洞?？自蕉嘣酱?，意味著越多的bug可以逃脫。如果設(shè)計(jì)的同一區(qū)域（奶酪片之間的重疊孔）中沒(méi)有被任何一種驗(yàn)證技術(shù)所覆蓋和測(cè)試，那么這個(gè)漏洞就會(huì)通過(guò)驗(yàn)證，并最終出現(xiàn)在交付產(chǎn)品中。

一種好的驗(yàn)證方法必須在每個(gè)切片上呈現(xiàn)盡可能少和小的孔。而這就要求驗(yàn)證團(tuán)隊(duì)有著扎實(shí)的策略、經(jīng)驗(yàn)和高效的溝通，這些品質(zhì)也是交付高質(zhì)量產(chǎn)品的重要因素。

在驗(yàn)證過(guò)程中，當(dāng)我們發(fā)現(xiàn)一個(gè)bug，或者一個(gè)切片上的孔時(shí)，及時(shí)修復(fù)并檢查其他切片是否有類似的漏洞。每一個(gè)切片都應(yīng)該找到前一個(gè)切片中的漏洞，并在繼續(xù)運(yùn)行之前解決掉它們。而實(shí)現(xiàn)這一目標(biāo)的有效方式是全面健全性檢查！

在應(yīng)用于處理器驗(yàn)證的瑞士奶酪模型原則中，如果一種技術(shù)有改進(jìn)的測(cè)試平臺(tái)、新的斷言等功能加持，那么在產(chǎn)品交付之前，該漏洞就會(huì)被及時(shí)發(fā)現(xiàn)和修復(fù)。所有的處理器驗(yàn)證技術(shù)都很重要，正是所有技術(shù)的結(jié)合才能使每種技術(shù)更有效率。

同時(shí)我們需要意識(shí)到一個(gè)單一的驗(yàn)證技術(shù)不可能完成所有的事情，是所有技術(shù)的綜合提高了驗(yàn)證和處理器設(shè)計(jì)的整體質(zhì)量。在產(chǎn)品的開(kāi)發(fā)過(guò)程中，可能會(huì)有意想不到的變化或因素，這些外部行為會(huì)影響某種技術(shù)的效率。例如，設(shè)計(jì)中的變化沒(méi)有很好的傳達(dá)給驗(yàn)證團(tuán)隊(duì)，或者出小差的周五下午的工作效率導(dǎo)致了人為錯(cuò)誤。這些因素都會(huì)增加切片上孔的大小，因此保持項(xiàng)目規(guī)范的及時(shí)更新以及設(shè)計(jì)者和驗(yàn)證工程師之間有效的定期溝通極其重要。此外在Codasip，實(shí)現(xiàn)這一目標(biāo)的另一個(gè)有效解決方案是執(zhí)行由其他團(tuán)隊(duì)成員進(jìn)行的代碼審查。

Codasip使用的驗(yàn)證技術(shù)和技巧，使我們能夠創(chuàng)建冗余，及時(shí)發(fā)現(xiàn)和修復(fù)漏洞并最終提供一流品質(zhì)的RISC-V處理器！

審核編輯 ：李倩