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)、( eg x_2)均为文字(literal)
1.3 cube和clause
一个cube是若干literal的合取，形如(x_1land x_2land x_6land
eg x_3)
一个clause是若干literal的析取,形如(x_1lor x_3 lor
eg x_5)
根据德摩根率：对一个cube取非即可得到一个literal，即$
eg(x_1land x_3land
eg x_4) equiv
eg x_1 lor
eg x_3lor x_4 $
1.4 合取范式(conjunction normal form, CNF)
形如(clauseland clauselanddotsland 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_iLongrightarrow x_i', x_iin 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))， 记为(Smodels P(X));
称(P(X))是系统(S)的一个不变式（invariant）;
如果(P(X))不是不变式，则存在一个有限长度的状态序列（counterexample run）：$ s_0, s_1,dots,s_k(，且满足)s_0models I(X), s_k
vDash 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_imodels F_{i+1})
- (F_i(X)land T(Y, X, X')models F_{i+1}(X'))
- (F_imodels P, 0leq i<k)
2.1.1 得出目标归纳不变式
若程序运行中找出了一个序列(F_0,dots, F_i,F_{i+1},dots,F_k)，该序列满足以上条件。
再检查该序列，若有(F_i=F_{i+1}, 0leq i<k)，则找到目标归纳不变式(F_i) .
为甚么？
- 根据上述条件4和(F_i=F_{i+1})，可得到(F_iland T models F_i') ;
- 根据条件1和条件3，可得到(Imodels F_i);
- 根据条件5，可得到(F_imodels 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_0models P)是否成立(若成立，即is_sat(I & !P)不能够满足；反之，IC3验证失败），若(F_0models 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
eg P)可满足（is_sat(F[k] & !P)），等价于(F[k])表示的状态集合和(
eg 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（(
eg s)）就可以做到；
那么是不是只要添加(
eg s)就行呢？
答案是不一定的。
从每个frame中删除(s)（往其中添加(
eg s)）后，还需要考虑序列条件4是否依然能够保持（每个frame都需添加clause，所以除条件4以外的其余条件均可以保持）。
首先，考虑往(F[i])和(F[i-1])中添加( eg s)后如下条件4是否仍然成立：
因为在没添加( eg s)时，条件4已经成立，即(F[i-1] land T models F[i]')，所以上述条件4也可以写成：
- 添加(
eg s)后若上述条件4不成立，即
is_sat(F[i-1] & !s & T & s')可满足 。这说明在（(F[i-1] land eg s)）所表示的状态集合中，还有一部分状态(c)无法一步迁移到（(F[i]'land eg s')），c = get_predecessor(i-1, s')。这部分状态集合(c)则需要在(F[1],...,F[i-1])公式所对应的状态集合中被删除(blocking)，因此递归删除rec_block(c, i-1)。 - 添加(
eg s)后若上述条件4成立，可以根据条件3证明，对于(F[i])之前的每一个frame均有上述条件4成立，则可以将(
eg s)添加至(F[1],dots,F[i])中的所有frame（
generalize()函数可以将( eg s)中的若干文字(literal）去除掉之后得到( eg g),同时保证将所有frame添加( eg 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 cland Tland
eg c')等价于(F[i-1]land Tland
eg 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过程。