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_i\Longrightarrow x_i',\ x_i\in X\);
用對應的后繼變量替換X中的每個狀態變量，可得到 X' ;
Y相當於中間變量，不參與系統狀態組成 ;
遷移關系形如
一步遷移可以表示為：
其中，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)\)是一個歸納不變式；
則可推出\(P(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)\)歸納強化后的公式，則有
- \(I(X) \models F(X)\)
- \(F(X)\land T(Y, X, X')\models F(X')\)
- \(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
算法運行過程中，該序列須滿足的條件是：
- \(F_0 =I\)，即\(F_0(X) = I(X)\)的簡寫，以下均簡寫
- \(F_i\)是一個clause集合，即為一個合取范式（CNF）
- \(F_{i+1}\subseteq F_i\)，表示\(F_{i+1}\)中包含的clauses是\(F_i\)的子集，亦即\(F_i\models F_{i+1}\)
- \(F_i(X)\land T(Y, X, X')\models F_{i+1}(X')\)
- \(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\)成立，則初始序列滿足所有條件。
當構造了一個滿足所有條件的序列之后（例如上述構造的初始序列），接下來嘗試拓展該序列（增加一個frame）。但在那之前，我們還需要驗證公式\(F[k]\models P\)是否成立，若它成立，我們才能在\(F[k]\)之后再添加\(F[k+1]\)，這確保了在添加\(F[k+1]\)之后新序列還能夠滿足條件5；若它不成立，我們需要調整\(F[1],\dots,F[k]\)使它成立。
若\(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驗證失敗並返回。
從每個frame中刪除狀態集合\(s\)（cube表示），只需向每個frame中添加一個clause（\(\neg s\)）就可以做到；
那么是不是只要添加\(\neg s\)就行呢？
答案是不一定的。
從每個frame中刪除\(s\)（往其中添加\(\neg s\)）后，還需要考慮序列條件4是否依然能夠保持（每個frame都需添加clause，所以除條件4以外的其余條件均可以保持）。
首先，考慮往\(F[i]\)和\(F[i-1]\)中添加\(\neg s\)后如下條件4是否仍然成立：
因為在沒添加\(\neg s\)時，條件4已經成立，即\(F[i-1] \land T \models F[i]'\)，所以上述條件4也可以寫成：
- 添加\(\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)，因此遞歸刪除rec_block(c, i-1)。 - 添加\(\neg s\)后若上述條件4成立，可以根據條件3證明，對於\(F[i]\)之前的每一個frame均有上述條件4成立，則可以將\(\neg s\)添加至\(F[1],\dots,F[i]\)中的所有frame（
generalize()函數可以將\(\neg s\)中的若干文字(literal）去除掉之后得到\(\neg g\),同時保證將所有frame添加\(\neg g\)后，序列還能滿足條件4）。
經過上述處理，\(F[k]\models P\)已經成立。
跳出主函數IC3內層while循環，開始擴展frame。
增加一個frame：k = k + 1, F[k] = T。
此時，公式序列可以滿足序列條件，按理說，可以繼續進行blocking phase。
但是進一步考慮下列情況：
設\(c\)是CNF公式\(F[j]\)的一個clause，
假設\(F[i-1]\land T \models c'\)，（注意代碼中的\(F[i-1]\land c\land T\land \neg c'\)等價於\(F[i-1]\land T\land \neg c'\)）
根據條件4，我們有\(F[i-1]\land T \models F[i]'\)
因此可以得到\(F[i-1]\land T \models F[i]'\land c'\)
因此將clause \(c\)添加至\(F[i]\)，序列條件依然滿足，並且能夠進一步加強\(F[i]\)，得到更精確的目標歸納不變式。
同時，處理完一個frame \(F[i]\)之后，檢查這兩個相鄰的frame是否相等（\(F[i]\equiv F[i+1]\)）。若相等，則找到一個不動點(fixedpoint),\(F[i]\)，即目標的歸納不變式。
上述過程對應IC3主函數中的propagation過程。