可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率嗎？

我們可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率，但是這個(gè)主要是通過減少Formal驗(yàn)證空間來實(shí)現(xiàn)的，很容易出現(xiàn)過約，導(dǎo)致bug遺漏。

簡化斷言以優(yōu)化Formal形式分析的主要挑戰(zhàn)是：

由于DUT一般是比較復(fù)雜的，所以工程師們都傾向于使用長而復(fù)雜的，甚至單行斷言來精確地編碼DUT的期望行為。但是對于Formal形式分析而言，斷言應(yīng)該盡可能簡單，斷言所涉及的時(shí)序邏輯深度應(yīng)該盡可能短，這樣才能更快地完成證明。

斷言簡化的關(guān)鍵在于將你需要驗(yàn)證的復(fù)雜行為“分解”為最基本的行為元素，注意分解前后的斷言一定要是等價(jià)的。

“相信”Formal形式工具能夠合理安排這些淺邏輯深度斷言的證明，下面是一個(gè)簡單的例子示意：假設(shè)你有一個(gè)錯(cuò)誤指示信號(hào)“error”，它的生成邏輯如下

assign error = err1 | err2;

其中“err1”和“err2”用于檢測兩種不同的錯(cuò)誤場景。下面的原始的斷言：斷言error永遠(yuǎn)不會(huì)發(fā)生。

當(dāng)其中“err1”或者“err2”后面的邏輯錐（COI）電路很大時(shí)，我們可能沒有辦法完成這個(gè)斷言的證明。我們可以分解原始的斷言，分別驗(yàn)證“err1“和“err2”。

如果“err1的邏輯錐比較小，“err2”的邏輯錐比較大，我們可能首先比較快地完成“err1”的斷言證明，后面再針對性地優(yōu)化“err2”的證明。

同樣，對于下面這個(gè)例子：

我們也可以對復(fù)雜斷言做簡化，簡化前后的斷言版本是等價(jià)的，但是Formal形式分析的效果會(huì)好很多。

因?yàn)閷τ贔ormal工具而言，邏輯錐小的斷言更容易完成證明，并且如果已經(jīng)完成了一個(gè)簡單斷言驗(yàn)證之后，F(xiàn)ormal工具會(huì)利用這個(gè)斷言驗(yàn)證的結(jié)果去證明其他的斷言。

審核編輯：劉清