當(dāng)前位置：首頁 > 编程资源 > 综合教程 >内容正文

综合教程

IC3算法简析

發(fā)布時(shí)間：2024/6/21 综合教程 30 生活家

生活随笔收集整理的這篇文章主要介紹了 IC3算法简析小編覺得挺不錯(cuò)的,現(xiàn)在分享給大家,幫大家做個(gè)參考.

目錄1 基礎(chǔ)(preliminaries)1.1 布爾變量(variables)1.2 文字(literals)1.3 cube和clause1.4 合取范式(conjunction normal form, CNF)1.5 遷移系統(tǒng)(Transition System)1.5.1 變量集合1.5.2 系統(tǒng)狀態(tài)1.5.3 初始狀態(tài)(公式)1.5.4 遷移關(guān)系(公式)1.6 不變式驗(yàn)證問題(invariant checking problem)1.7 歸納不變式(inductive invariant)1.8 歸納強(qiáng)化(inductive strengthening)1.9 相對(duì)歸納(inductive relative)2 IC3算法思想2.1 構(gòu)造歸納不變式2.1.1 得出目標(biāo)歸納不變式2.2 算法實(shí)現(xiàn)下載pdf
IC3算法是一種形式化驗(yàn)證方法。在《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 基礎(chǔ)(preliminaries)

1.1 布爾變量(variables)

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

1.2 文字(literals)

一個(gè)literal是一個(gè)布爾變量或者布爾變量的非，即(x_1)、(
eg x_2)均為文字(literal)

1.3 cube和clause

一個(gè)cube是若干literal的合取，形如(x_1land x_2land x_6land
eg x_3)
一個(gè)clause是若干literal的析取,形如(x_1lor x_3 lor
eg x_5)
根據(jù)德摩根率：對(duì)一個(gè)cube取非即可得到一個(gè)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)的邏輯表達(dá)式，
cube即為合取范式(CNF),
邏輯公式(formula，簡稱“公式”)一般用合取范式(CNF)來表示。

1.5 遷移系統(tǒng)(Transition System)

一個(gè)遷移系統(tǒng)由三部分組成，分別是變量集合、初始狀態(tài)(公式)和遷移關(guān)系(公式)。

1.5.1 變量集合

包括兩部分：

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

1.5.2 系統(tǒng)狀態(tài)

可以用一個(gè)包含所有 狀態(tài)變量的cube來表示一個(gè)“系統(tǒng)狀態(tài)”，這樣的cube也叫miniterm；
可以用一個(gè)包含部分 狀態(tài)變量的cube來表示若干“系統(tǒng)狀態(tài)”的集合；
所有狀態(tài)變量的一種賦值為系統(tǒng)的一個(gè)狀態(tài)；
而當(dāng)cube成真時(shí)，可以得到一種(或若干種)所有狀態(tài)變量的賦值

1.5.3 初始狀態(tài)(公式)

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

1.5.4 遷移關(guān)系(公式)

用公式(T(Y,X,X'))表示遷移關(guān)系。
X中每個(gè)狀態(tài)變量對(duì)應(yīng)一個(gè)后繼變量，即(x_iLongrightarrow x_i', x_iin X);
用對(duì)應(yīng)的后繼變量替換X中的每個(gè)狀態(tài)變量，可得到 X' ;
Y相當(dāng)于中間變量，不參與系統(tǒng)狀態(tài)組成 ;
遷移關(guān)系形如

[ x_1' = au_1(Y, X) land x_2' = au_2(Y, X)landdotsland x_n' = au_n (Y, X)
]

一步遷移可以表示為：

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

其中，cube (s(X))表示狀態(tài)；
該蘊(yùn)含式可以理解為在系統(tǒng)(M)中，給定輸入變量集合(Y)的賦值，經(jīng)過一步遷移可以從(s_{i-1})到達(dá)(s_i)

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

公式(P(X))表示安全狀態(tài)集合（a set of good states）;
若系統(tǒng)(S)中的所有可達(dá)狀態(tài)都在安全狀態(tài)集合里，則稱系統(tǒng)(S)滿足公式(P(X))，記為(Smodels P(X));
稱(P(X))是系統(tǒng)(S)的一個(gè)不變式（invariant）;
如果(P(X))不是不變式，則存在一個(gè)有限長度的狀態(tài)序列（counterexample run）：$ s_0, s_1,dots,s_k(，且滿足)s_0models I(X), s_k
vDash P$

1.7 歸納不變式(inductive invariant)

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

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

1.8 歸納強(qiáng)化(inductive strengthening)

通常待驗(yàn)證性質(zhì)(P(X))可能是不變式，但通常不會(huì)是歸納不變式。
這時(shí)需要找到性質(zhì)(P(X))的一個(gè)歸納強(qiáng)化——公式(R(X));
使得(P(X))歸納強(qiáng)化后的公式(P(X)land R(X))是一個(gè)歸納不變式；
則可推出(P(X))是一個(gè)不變式。

1.9 相對(duì)歸納(inductive relative)

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

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

2 IC3算法思想

驗(yàn)證性質(zhì)(P(X))是系統(tǒng)(S = (I(X), T(Y,X,X')))一個(gè)安全性質(zhì)（不變式）
IC3算法嘗試構(gòu)造一個(gè)歸納不變式(F(X))
使得(F(X))是性質(zhì)(P(X))歸納強(qiáng)化后的公式，則有

(I(X) models F(X))
(F(X)land T(Y, X, X')models F(X'))
(F(X)models P(X))
可得出性質(zhì)(P(X))是系統(tǒng)(S)的一個(gè)安全性質(zhì)。

2.1 構(gòu)造歸納不變式

IC3算法中主要維護(hù)一個(gè)公式序列(F_0(X), F_1(X),dots,F_k(X))（歸納不變式若存在，則從這序列中產(chǎn)生）
該序列中每一項(xiàng)（(F_i(X))）是一個(gè)frame
算法運(yùn)行過程中，該序列須滿足的條件是：

(F_0 =I)，即(F_0(X) = I(X))的簡寫，以下均簡寫
(F_i)是一個(gè)clause集合，即為一個(gè)合取范式（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 得出目標(biāo)歸納不變式

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

根據(jù)上述條件4和(F_i=F_{i+1})，可得到(F_iland T models F_i') ;
根據(jù)條件1和條件3，可得到(Imodels F_i);
根據(jù)條件5，可得到(F_imodels P) ；
故(F_i)是目標(biāo)歸納不變式。

2.2 算法實(shí)現(xiàn)

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要生成一個(gè)公式序列(F_0,dots, F_k)，并確保該公式序列滿足2.1節(jié)列出的條件（以下“條件”特指2.1節(jié)所列條件，用條件i代表第幾項(xiàng)條件）。

首先構(gòu)造初始序列(F[0] = I, F[k] =T, k=1)（(F[k]=T)相當(dāng)于不包含任何clause），并檢查了(F_0models P)是否成立(若成立，即is_sat(I & !P)不能夠滿足；反之，IC3驗(yàn)證失敗），若(F_0models P)成立，則初始序列滿足所有條件。

當(dāng)構(gòu)造了一個(gè)滿足所有條件的序列之后（例如上述構(gòu)造的初始序列），接下來嘗試拓展該序列（增加一個(gè)frame）。但在那之前，我們還需要驗(yàn)證公式(F[k]models P)是否成立，若它成立，我們才能在(F[k])之后再添加(F[k+1])，這確保了在添加(F[k+1])之后新序列還能夠滿足條件5；若它不成立，我們需要調(diào)整(F[1],dots,F[k])使它成立。

若(F[k]models P)不成立，等價(jià)于(F[k]land
eg P)可滿足（is_sat(F[k] & !P)），等價(jià)于(F[k])表示的狀態(tài)集合和(
eg P)表示的壞態(tài)集合有交集，用c（一個(gè)cube ）表示該交集（c = get_state(F[k] & !P)）。函數(shù)rec_block(c, k)的目的是將該交集c從(F[1], dots, F[k])這些公式對(duì)應(yīng)的狀態(tài)集合中刪除（blocking）——即調(diào)整(F[0],dots, F[k])的過程。

(c, k)（亦即(s, i)）被稱為一個(gè)證明義務(wù)（proof obligation），其中c是一個(gè)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，即初始狀態(tài)集合（(F[0]=I)）和壞態(tài)集合存在交集。根據(jù)序列條件，(F[0])是固定不變的，無法從(F[0])中刪除更多狀態(tài)，故IC3驗(yàn)證失敗并返回。

從每個(gè)frame中刪除狀態(tài)集合(s)（cube表示），只需向每個(gè)frame中添加一個(gè)clause（(
eg s)）就可以做到；
那么是不是只要添加(
eg s)就行呢？
答案是不一定的。
從每個(gè)frame中刪除(s)（往其中添加(
eg s)）后，還需要考慮序列條件4是否依然能夠保持（每個(gè)frame都需添加clause，所以除條件4以外的其余條件均可以保持）。

首先，考慮往(F[i])和(F[i-1])中添加(
eg s)后如下條件4是否仍然成立：

[ F[i-1]land
eg s land T models F[i]' land
eg s'
]

因?yàn)樵跊]添加(
eg s)時(shí)，條件4已經(jīng)成立，即(F[i-1] land T models F[i]')，所以上述條件4也可以寫成：

[ F[i-1]land
eg s land T models
eg s'
]

添加(
eg s)后若上述條件4不成立，即is_sat(F[i-1] & !s & T & s')可滿足。這說明在（(F[i-1] land
eg s)）所表示的狀態(tài)集合中，還有一部分狀態(tài)(c)無法一步遷移到（(F[i]'land
eg s')），c = get_predecessor(i-1, s')。這部分狀態(tài)集合(c)則需要在(F[1],...,F[i-1])公式所對(duì)應(yīng)的狀態(tài)集合中被刪除(blocking)，因此遞歸刪除rec_block(c, i-1)。
添加(
eg s)后若上述條件4成立，可以根據(jù)條件3證明，對(duì)于(F[i])之前的每一個(gè)frame均有上述條件4成立，則可以將(
eg s)添加至(F[1],dots,F[i])中的所有frame（generalize()函數(shù)可以將(
eg s)中的若干文字(literal）去除掉之后得到(
eg g),同時(shí)保證將所有frame添加(
eg g)后，序列還能滿足條件4）。

經(jīng)過上述處理，(F[k]models P)已經(jīng)成立。
跳出主函數(shù)IC3內(nèi)層while循環(huán)，開始擴(kuò)展frame。
增加一個(gè)frame：k = k + 1, F[k] = T。
此時(shí)，公式序列可以滿足序列條件，按理說，可以繼續(xù)進(jìn)行blocking phase。
但是進(jìn)一步考慮下列情況：
設(shè)(c)是CNF公式(F[j])的一個(gè)clause，
假設(shè)(F[i-1]land T models c')，（注意代碼中的(F[i-1]land cland Tland
eg c')等價(jià)于(F[i-1]land Tland
eg c')）
根據(jù)條件4，我們有(F[i-1]land T models F[i]')
因此可以得到(F[i-1]land T models F[i]'land c')
因此將clause (c)添加至(F[i])，序列條件依然滿足，并且能夠進(jìn)一步加強(qiáng)(F[i])，得到更精確的目標(biāo)歸納不變式。
同時(shí)，處理完一個(gè)frame (F[i])之后，檢查這兩個(gè)相鄰的frame是否相等（(F[i]equiv F[i+1])）。若相等，則找到一個(gè)不動(dòng)點(diǎn)(fixedpoint),(F[i])，即目標(biāo)的歸納不變式。
上述過程對(duì)應(yīng)IC3主函數(shù)中的propagation過程。

下載pdf

IC3.pdf

總結(jié)

以上是生活随笔為你收集整理的IC3算法简析的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。

算法