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

因為形式分析算法很難適應非常大的狀態(tài)空間，而計數(shù)器和存儲器都會引入很多的狀態(tài)空間和時序深度。針對這個問題，我們可以在不影響驗證完備性的條件下減小計數(shù)器和存儲器的大小或者用抽象模型替換。

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

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

下面是一個計數(shù)器示例

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