第一性原理和芯片驗(yàn)證
[導(dǎo)讀]亞里士多德說(shuō)：“任何一個(gè)系統(tǒng)都有自己的第一性原理，它是一個(gè)根基性命題或假設(shè)，不能被缺省，也不能被違反。”《第一性原理》第一性原理，好比樹木的根基，沒(méi)有人會(huì)看到繁茂枝干下的樹根，但它決定了樹的一切。本文將“第一性原理”的思想引入芯片驗(yàn)證中的幾個(gè)場(chǎng)景，以理清一些驗(yàn)證問(wèn)題的本質(zhì)，直達(dá)本...
亞里士多德說(shuō)：“任何一個(gè)系統(tǒng)都有自己的第一性原理，它是一個(gè)根基性命題或假設(shè)，不能被缺省，也不能被違反。”第一性原理，好比樹木的根基，沒(méi)有人會(huì)看到繁茂枝干下的樹根，但它決定了樹的一切。本文將“第一性原理”的思想引入芯片驗(yàn)證中的幾個(gè)場(chǎng)景，以理清一些驗(yàn)證問(wèn)題的本質(zhì)，直達(dá)本源。我們常問(wèn)，未來(lái)十年什么會(huì)變化？這個(gè)問(wèn)題很重要，但更重要的問(wèn)題可能是，未來(lái)十年什么不變？如果能找到不變的，把所有的資源和精力，毫無(wú)保留地投入在不變的事物上，其力量不可同日而語(yǔ)。
《第一性原理》
“歸納法是通過(guò)實(shí)踐推導(dǎo)結(jié)論，把連續(xù)性的經(jīng)驗(yàn)推廣到一切時(shí)空。然而，并非所有事物都有連續(xù)性，固有的思維會(huì)讓你陷入“歸納法謬誤”。打破認(rèn)知邊界，實(shí)現(xiàn)第二曲線創(chuàng)新，你需要全新的思維模式——演繹法。但是演繹法必須有一個(gè)基石，一個(gè)來(lái)自系統(tǒng)之外、能夠邏輯自洽的元起點(diǎn)。這個(gè)元起點(diǎn)既可以稱為第一前提、邏輯奇點(diǎn)，也可以稱為第一性原理。”《第一性原理》歸納法等同于芯片驗(yàn)證中simulation,當(dāng)你在某個(gè)場(chǎng)景下連續(xù)采樣一個(gè)接口100遍甚至1000遍，發(fā)現(xiàn)這個(gè)接口保持不變，就可以認(rèn)為這個(gè)接口保持不變么？
1、你永遠(yuǎn)無(wú)法保證其中偶爾會(huì)出現(xiàn)的一兩次跳變；2、你永遠(yuǎn)無(wú)法從根本上證明這個(gè)接口保持不變這一特性，特別是在這些場(chǎng)景的邊界往往會(huì)超出我們預(yù)知的邊界。?接口會(huì)保持連續(xù)性的隱含假設(shè)其實(shí)也是我們驗(yàn)證過(guò)程中一種check不完備或者激勵(lì)過(guò)約的一種體現(xiàn)，存在遺留bug的風(fēng)險(xiǎn)。?雖然在科學(xué)領(lǐng)域中，歸納法以所謂的“獨(dú)立可重復(fù)性”作為標(biāo)準(zhǔn)，從而確保實(shí)驗(yàn)結(jié)果的有效性，但這并不意味著，我們通過(guò)歸納法總結(jié)出來(lái)的規(guī)律就一定是真實(shí)的。也就是說(shuō)，這能證偽不能證明。
從驗(yàn)證的角度，我們需要從根本上進(jìn)行演繹推理證明在該場(chǎng)景下接口保持不變這一feature。可以利用斷言，這個(gè)接口在這期間的每一拍保持不變。
這樣就可以從根本上證明這個(gè)特性。?在驗(yàn)證過(guò)程中“從基石和結(jié)構(gòu)切入，不要從內(nèi)容入手”。如果我們需要驗(yàn)證A-C：1、在RTL中實(shí)現(xiàn)是A ->B(RTL內(nèi)部信號(hào)) ->C，這個(gè)時(shí)候我們一定需要保證我們整個(gè)驗(yàn)證環(huán)路的正確性，僅僅能夠證明B->C是不可信的，依賴RTL內(nèi)部信號(hào)的任何檢查都是賭博，哦不，是賭命。
2、如果驗(yàn)證的feature是A B=C，而RTL由于各種PPA的考慮，RTL的實(shí)現(xiàn)是A B B-B=C。功能性驗(yàn)證就應(yīng)該直達(dá)本源，不要看實(shí)現(xiàn)的表象，關(guān)注這個(gè)feature本身，避免參考模型和設(shè)計(jì)錯(cuò)到一起。?對(duì)于驗(yàn)證，驗(yàn)證邏輯的比檢查更加真實(shí)。也就是說(shuō)，我們從A推導(dǎo)出B，中間的過(guò)程必須符合正確的邏輯。甚至古希臘人認(rèn)為從A事物到B事物之間的邏輯才是實(shí)體，而A、B這兩個(gè)事物不一定是實(shí)體。
?
下載文檔
