當(dāng)計(jì)數(shù)器和內(nèi)存處于我們所需要證明斷言的邏輯錐中，它們可能是Formal無法完成證明的根本原因。

因?yàn)樾问椒治?a href="http://m.xsypw.cn/v/tag/2562/" target="_blank">算法很難適應(yīng)非常大的狀態(tài)空間，而計(jì)數(shù)器和存儲器都會引入很多的狀態(tài)空間和時(shí)序深度。針對這個(gè)問題，我們可以在不影響驗(yàn)證完備性的條件下減小計(jì)數(shù)器和存儲器的大小或者用抽象模型替換。

Formal驗(yàn)證中優(yōu)化大計(jì)數(shù)器的一種流行且有效的方法是將它們替換為小型的狀態(tài)機(jī)模型（狀態(tài)空間小），該模型僅考慮會觸發(fā)設(shè)計(jì)操作的計(jì)數(shù)器臨界值。例如，假設(shè)計(jì)數(shù)器的值“m”、“n-1”和“n”很關(guān)鍵。考慮以下狀態(tài)機(jī)作為替代：

為了用這個(gè)抽象模型替換原始計(jì)數(shù)器，我們首先繞過真實(shí)設(shè)計(jì)的驅(qū)動(dòng)邏輯（用cutpoint的方式“切割”原始計(jì)數(shù)器輸出信號，使其變成一個(gè)自由隨機(jī)變量，然后向其添加約束）

下面是一個(gè)計(jì)數(shù)器示例

這種辦法主要還是用于bug-hunting，而且如果RTL中的其他部分實(shí)際就需要計(jì)數(shù)器延遲特定周期，那么這個(gè)優(yōu)化方法就不適用了，所以說此時(shí)就沒法用作formal full prove。