IC3演算法是一種形式化驗證方法。 在《Efficient Implementation of Property Directed Reachability》一文中，又將此方法命名為PDR。IC3在模型檢測競賽(HWMCC)中取得突出成績後引起廣泛重視。
參考文章：A. Griggio and M. Roveri, "Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 35, no. 6, pp. 1026-1039, June 2016, doi: 10.1109/TCAD.2015.2481869.

1 基礎(preliminaries)

1.1 布林變數(variables)

諸如$ x_1, x_2,...,x_n$這樣取值為真(1)或假(0)的變數

1.2 文字(literals)

一個literal是一個布林變數或者布林變數的非，即\(x_1\)、\(\neg(x_2)\)均為文字(literal)

1.3 cube和clause

一個cube是若干literal的合取，形如\(x_1\land x_2\land x_6\land \neg x_3\)
一個clause是若干literal的析取,形如\(x_1\lor x_3 \lor \neg x_5\)
根據德摩根率：對一個cube

取非即可得到一個literal，即$\neg(x_1\land x_3\land \neg x_4) \equiv \neg x_1 \lor\neg x_3\lor x_4 $

1.4 合取正規化(conjunction normal form, CNF)

形如\(clause\land clause\land\dots\land clause\)的邏輯表示式，cube即為合取正規化(CNF)
邏輯公式(formula，簡稱“公式”)一般用合取正規化(CNF)來表示。

1.5 遷移系統(Transition System)

一個遷移系統由三部分組成，分別是變數集合、初始狀態(公式)和遷移關係(公式)。

1.5.1 變數集合

包括兩部分：

• 狀態變數集合X：\(\{x_1, x_2,\dots, x_n\}\)（state variables）
• 初始輸入變數集合Y：\(\{ y_1,\dots,y_m\}\)（primary input variables）

1.5.2 系統狀態

可以用一個包含所有 狀態變數的cube來表示一個“系統狀態”，這樣的cube也叫miniterm；
可以用一個包含部分 狀態變數的cube來表示若干“系統狀態”的集合；
所有狀態變數的一種賦值為系統的一個狀態；
而當cube成真時，可以得到一種(或若干種)所有狀態變數的賦值

1.5.3 初始狀態(公式)

用公式\(I(X)\)表示初始狀態集合
初始狀態為 “使\(I(X)\)成真時，所有狀態變數的賦值的可能情況”

1.5.4 遷移關係(公式)

用公式\(T(Y,X,X')\)表示遷移關係。
X中每個狀態變數對應一個後繼變數，即\(x_1 \Longrightarrow x_1'\);
用對應後繼變數替換X中的每個狀態變數，可得到 X' ;
Y相當於中間變數，不參與系統狀態組成 ;
遷移關係形如

\[ x_1' = \tau_1(Y, X) \land x_2' = \tau_2(Y, X)\land\dots\land x_n' = \tau_n (Y, X) \]

一步遷移可以表示為：

\[ s_{i-1}(X)\land T(Y, X, X') \models s_i(X') \]

其中，cube \(s(X)\)表示狀態；
該蘊含式可以理解為在系統\(M\)中，給定輸入變數集合\(Y\)的賦值，經過一步遷移可以從\(s_{i-1}\)到達\(s_i\)

1.6 不變式驗證問題(invariant checking problem)

公式\(P(X)\)表示安全狀態集合（a set of good states）;
若系統\(S\)中的所有可達狀態都在安全狀態集合裡，則稱系統\(S\)滿足公式\(P(X)\)， 記為\(S\models P(X)\);
稱\(P(X)\)是系統\(S\)的一個不變式（invariant）;
如果\(P(X)\)不是不變式，則存在一個有限長度的狀態序列（counterexample run）：$ s_0, s_1,\dots,s_k\(，且滿足\)s_0\models I(X),\ s_k\nvDash P$

1.7 歸納不變式(inductive invariant)

歸納不變式\(F(X)\)滿足兩個條件：

• \(I(X)\models F(X)\)
• \(F(X)\land T(Y, X, X') \models F(X')\)
  若\(F(X)\)為歸納不變式，則根據定義，\(F(X)\)也為不變式

1.8 歸納強化(inductive strengthening)

通常待驗證性質\(P(X)\)不會是歸納不變式。
這時需要找到性質\(P(X)\)的一個歸納強化——公式\(R(X)\);
使得\(P(X)\)歸納強化後的公式\(P(X)\land R(X)\)是一個歸納不變式

1.9 相對歸納(inductive relative)

公式\(F(X)\)相對歸納於(is inductive relative to)公式\(G(X, X')\)，則有

• \(I(X) \models F(X)\)，每個初始狀態都滿足\(F\)
• \(G(X,X')\land F(X)\land T(Y, X, X')\models F(X')\)，在給定前提\(G(X,X')\)成立的情況下，\(F(X)\)的歸納是成立的。

2 IC3演算法思想

驗證性質\(P(X)\)是系統\(S = (I(X), T(Y,X,X'))\)一個安全性質（不變式）
IC3演算法嘗試構造一個歸納不變式\(F(X)\)
使得\(F(X)\)是性質\(P(X)\)歸納強化後的公式，則有

1. \(I(X) \models F(X)\)
2. \(F(X)\land T(Y, X, X')\models F(X')\)
3. \(F(X)\models P(X)\)
   可得出性質\(P(X)\)是系統\(S\)的一個安全性質。

2.1 構造歸納不變式

IC3演算法中主要維護一個公式序列\(F_0(X), F_1(X),\dots,F_k(X)\)（歸納不變式若存在，則從這序列中產生）
該序列中每一項（\(F_i(X)\)）是一個frame
演算法執行過程中，該序列須滿足的條件是：

1. \(F_0 =I\)，即\(F_0(X) = I(X)\)的簡寫，以下均簡寫
2. \(F_i\)是一個clause集合，即為一個合取正規化（CNF）
3. \(F_{i+1}\subseteq F_i\)，表示\(F_{i+1}\)中包含的clauses是\(F_i\)的子集，亦即\(F_i\models F_{i+1}\)
4. \(F_i(X)\land T(Y, X, X')\models F_{i+1}(X')\)
5. \(F_i\models P,\ 0\leq i<k\)

2.1.1 得出目標歸納不變式

若程式執行中找出了一個序列\(F_0,\dots, F_i,F_{i+1},\dots,F_k\)，該序列滿足以上條件。
再檢查該序列，若有\(F_i=F_{i+1},\ 0\leq i<k\)，則找到目標歸納不變式\(F_i\) .
為甚麼？

• 根據上述條件4和\(F_i=F_{i+1}\)，可得到\(F_i\land T \models F_i'\) ;
• 根據條件1和條件3，可得到\(I\models F_i\);
• 根據條件5，可得到\(F_i\models P\) ；
  故\(F_i\)是目標歸納不變式。

2.2 演算法實現

bool IC3(I, T, P):
	if is_sat(I & !P): return False
	F[0] = I  # first element of trace is init-formula
	k = 1, F[k] = T  # add a new frame to the trace
	while True:
		# blocking phase
		while is_sat(F[k] & !P):
			c = get_state(F[k] & !P)  # c => F[k] & !P, c is a cube
			if not rec_block(c, k):
				return False  # counterexample found
				
		# propagation phase
		k = k + 1, F[k] = T
		for i = 1 to k-1:
			for each clause c in F[i]:
				if not is_sat(F[i] & c & T & !c'):
					add c to F[i+1]
			if F[i] == F[i+1]: return True  # property proved

主函式IC3的作用是生成一個公式序列\(F_0,\dots, F_k\)，並確保該公式序列滿足2.1節列出的條件（以下“條件”特指2.1節所列條件，用條件i代表第幾項條件）。


首先構造初始序列\(F[0] = I, F[k] =T, k=1\)（$F[k]=T \(相當於不包含任何clause），並檢查了\)F_0 \models P\(是否成立(若成立，即`is_sat(I & !P)`不能夠滿足；反之，IC3驗證失敗），若\)F_0 \models P\(成立，則初始序列滿足所有條件。 <br> 當構造了一個滿足所有條件的序列之後（例如上述構造的初始序列），接下來嘗試拓展該序列（增加一個frame）。但在那之前，我們還需要驗證公式\)F[k]\models P\(是否成立，若它成立，我們才能在\)F[k]\(之後再新增\)F[k+1]\(，這確保了在新增\)F[k+1]\(之後新序列還能夠滿足條件5；若它不成立，我們需要調整\)F[1],\dots, F[k]\(使它成立。 <br> 若\)F[k]\models P\(不成立，等價於\)F[k] \land \neg P\(可滿足（`is_sat(F[k] & !P)`），等價於\)F[k]\(表示的狀態集合和\)\neg P\(表示的壞態集合有交集，用`c`（一個*cube* ）表示該交集（`c = get_state(F[k] & !P)`）。函式`rec_block(c, k)`的目的是將該交集`c`從\)F[1], \dots, F[k]\(這些公式對應的狀態集合中刪除（blocking）——即調整\)F[0],\dots, F[k]$的過程。


(c, k)（亦即(s, i)）被稱為一個證明義務（proof obligation），其中c是一個CTI（counterexample to induction），用cube表示。

# simplified recursive blocking
bool rec_block(s, i):
	if i == 0: return False  # reach initial states
	while is_sat(F[i-1] & !s & T & s'):
		c = get_predecessor(i-1, s')
		if not rec_block(c, i-1): return False
	g = generalize(!s, i)
	add g to F[1],...,F[i]
	return True

若i==0，即初始狀態集合（\(F[0]=I\)）和壞態集合存在交集。根據序列條件，\(F[0]\)是固定不變的，無法從\(F[0]\)中刪除更多狀態，故IC3驗證失敗並返回。


從\(F[i]\)刪除狀態集合\(s\)（cube表示），只需向\(F[i]\)新增一個clause——\(\neg s\)就可以做到；
那麼對於\(F[i]\)之前的frame是不是也只要新增\(\neg s\)就行呢？
答案是不一定的。
從\(F[i]\)之前的frame中刪除\(s\)（新增\(\neg s\)）時，還需要考慮序列條件4是否依然能夠保持（每個frame都需新增clause，所以除條件4以外的其餘條件均可以保持）。


例如，往\(F[i-1]\)中新增\(\neg s\)需要考慮如下條件4是否仍然成立：

\[ F[i-1]\land \neg s \land T \models F[i]' \land \neg s' \]

因為在沒新增\(\neg s\)時，條件4已經成立，即\(F[i-1] \land T \models F[i]'\)，所以上述條件4也可以寫成：

\[ F[i-1]\land \neg s \land T \models \neg s \]

1. 新增\(\neg s\)後若上述條件4不成立，即is_sat(F[i-1] & !s & T & s')可滿足 。這說明在（\(F[i-1] \land \neg s\)）所表示的狀態集合中，還有一部分狀態\(c\)無法一步遷移到（\(F[i]\land \neg s\)），c = get_predecessor(i-1, s')。這部分狀態集合\(c\)則也需要在\(F[1],...,F[i-1]\)公式所對應的狀態集合中被刪除(blocking)，以確保條件4的成立，因此遞迴刪除rec_block(c, i-1)。
2. 新增\(\neg s\)後若上述條件4成立，可以根據條件3證明，對於\(F[i]\)之前的每一個frame均有上述條件4成立，則可以將\(\neg s\)新增至\(F[1],\dots,F[i]\)中的每一箇中。

經過上述處理，$F[k]\models P$已經成立。 跳出主函式IC3內層while迴圈，開始擴充套件`frame`。 增加一個`frame`：`k = k + 1, F[k] = T`。 此時，公式序列可以滿足序列條件，按理說，可以繼續進行*blocking phase*。 但是進一步考慮下列情況： 設$c$是CNF公式$F[j]$的一個*clause*， 假設$F[j]\land T \models c'$，（注意程式碼中的$F[i-1]\land c\land T\land \neg c'$等價於$F[i-1]\land T\land \neg c'$） 根據條件4，我們有$F[j]\land T \models F[j+1]'$ 因此可以得到$F[j]\land T \models F[j+1]'\land c'$ 因此將*clause* $c$新增至$F[j+1]$，序列條件依然滿足，並且能夠進一步加強$F[j+1]$，得到更精確的目標歸納不變式。 同時，處理完一個*frame* $F[i]$之後，檢查這兩個相鄰的*frame*是否相等（$F[i]\equiv F[i+1]$）。 上述過程對應IC3主函式中的*propagation*過程。