精選答案在計(jì)算機(jī)硬件(特別是集成電路)和軟件系統(tǒng)的設(shè)計(jì)過程中,形式驗(yàn)證的含義是根據(jù)某個(gè)或某些形式規(guī)范或?qū)傩裕褂脭?shù)學(xué)的方法證明其正確性或非正確性。
形式驗(yàn)證是一個(gè)系統(tǒng)性的過程,將使用數(shù)學(xué)推理來驗(yàn)證設(shè)計(jì)意圖(指標(biāo))在實(shí)現(xiàn)(RTL)中是否得以貫徹。形式驗(yàn)證可以克服所有3種仿真挑戰(zhàn),由于形式驗(yàn)證能夠從算法上窮盡檢查所有隨時(shí)間可能變化的輸進(jìn)值。