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

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

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

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

斷言簡化的關鍵在于將你需要驗證的復雜行為“分解”為最基本的行為元素，注意分解前后的斷言一定要是等價的。

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

assign error = err1 | err2;

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

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

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

同樣，對于下面這個例子：

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

因為對于Formal工具而言，邏輯錐小的斷言更容易完成證明，并且如果已經完成了一個簡單斷言驗證之后，F(xiàn)ormal工具會利用這個斷言驗證的結果去證明其他的斷言。

審核編輯：劉清