現(xiàn)代集成電路之中，verification 所占用的時(shí)間可達(dá)到60%-70%左右。其中一種驗(yàn)證就是功能驗(yàn)證，指的是不考慮綜合、電路布線之后所帶來的電路延遲等等現(xiàn)象，只考慮系統(tǒng)的邏輯正確性的一種驗(yàn)證方式。

目前業(yè)界主流的驗(yàn)證方法主要是以UVM（Universal Verification Methodology）為代表的驗(yàn)證方法學(xué)，通常使用隨機(jī)約束的方式，在電路仿真中自動(dòng)產(chǎn)生受控的隨機(jī)輸入，從而驅(qū)動(dòng)驗(yàn)證電路并完成驗(yàn)證功能。隨著UVM的發(fā)展和廣泛使用，特別是其中SystemVerilog語言加入了面向?qū)ο?、功能覆蓋、隨機(jī)約束等更加類似軟件開發(fā)的特性，使得驗(yàn)證平臺間模塊重用的效率得到提升，編程結(jié)構(gòu)化變好，代碼更加靈活。（from https://zhuanlan.zhihu.com/p/35411326）

由于VLSI的復(fù)雜性，目前存在meltdown和spectre 現(xiàn)象的出現(xiàn)。

形式化驗(yàn)證和基于電路仿真的驗(yàn)證方法的最根本不同在于，形式化驗(yàn)證并不基于某些給定的輸入向量，而是通過數(shù)學(xué)方法分析、推導(dǎo)并證明某個(gè)邏輯功能在給出的邊界范圍內(nèi)是否與設(shè)計(jì)規(guī)約完全吻合，若不吻合則會(huì)給出一個(gè)反例。在上面舉的例子中，形式化驗(yàn)證可以從給定的復(fù)位狀態(tài)開始，用數(shù)學(xué)方法自動(dòng)探索并覆蓋整個(gè)狀態(tài)空間