（计算机系统结构专业论文）模型检验及其布尔可满足问题的研究.pdf

摘簧 作为形式瓣 正的爨疆方法，模型检狳 e v l s i s o c 设计的功能验i 磁中发挥着越涞越 港婺豹搀嚣。凝模墅竣验巾。设毒 被撼浆为有瑕状态转移模型( 或赣k r i p k e 结构) ， 糟蘼要骚霞蘸满褴霹簿态逻鬻襄袤逮，道过捡验模登燕餐褥食褥寒黥辩零溪程袋辫设 诗落行虢证。黠模型稔验两京，状态窒闷随获态变蠹瓣数秘戒捺数傣增长楚疆磷窕成 瓣弱王渣器豹襁奉霞鼹掰程。为了缓瓣蘩登宽骚这耱瓣橇，磺究入撼融经挺出了谗多 方法。比如，剃用二叉决策姻豹各种优化变神袋示模戮的转移羌系和状态空间 辩验 疆菠努转穗舞露謇霹瀵燕f - 3 遂( s a t ) ；弑黢懋嚣蘩饕鼙懑簿食逶魏接象强缝建等。 在该研究辩景下，本文所考察鲍荚镳问题魁：辩傅构建紧皴且离散的转移凝繇； 搬健快速提鞭檄小农尔不埘瀵足子式；惑瓣s a 譬的谓磷髅撼算法对绺散步长敏麟的润 题。锋对这壁阏题，零文徽趣睃更蘸鞠艇鞭燕翅下： 1 铃黠瓣号辏蘩检验中蠲籍莪建紧羧量离簸魏转穆募系藏题，捷凑了霹势黎觞 转移关系避静蘸新分鳃的静澈方法。转移袋系豹褐建髓将譬摸囊橙瓣躺霪簧环节，该 转组算法态分利耀了转穆装系套分割郝静支撑肉量所熟露的组蛱特熊，当转移凝黎静 辩势籍支撂弱激差爨誉夫瓣，簸葵宅裁努您一缝；努缀舞法戆撬赢髂凝在舞方舞；葜 ，蕤够稳建繁致藩转移美飘霆蓬辩蒸攥逮鼹集i s g a s 鹰9 孛褥台蒸摹孛戆实夔避静鼹 蜜验袭绢，转移关系戆大小能够减少约i o ，籁中转移芙累瀚大小楚由袭瀑它 的b d d 节点数嗣来衡誊。裁二，分组的隽h 察减少了求解状恣像盼遥算步骤。 2 ；舞怼魏褒捷蘧掇致缀小枣毒誉瑟潢是予蘧戆秘惩，搀窭了怼旗乎逮嚣予镯黪糠 溃提亵算法滤稼颈纛靛餐戆毪纯方寨。巍藻于舞蒙黎缀纯戆模攘捡簸串，鬟取禳套季 w 满足问题魑擞键。遍历予旬的算法遇过邂一判断每个子旬的墩禽涞求解极小不w 潲 避予式，本文德健方囊逶瀵瓣某些变畿遴褥预先赋餐，赫恁了粼蘸乎镩取会豹诗箨镁 务。鏊爨豢俸凝程嚣方覆；其一， 筝梵一聋孛爨鼗骞寰，缀褰了雾法效攀，：蛙s a t l i b 审 抟实秘遴嚣鹣实验表臻，程求鬃这些实藕薅，薄法篓遮簿对惩鼗簿簸褥约8 器嚣一l 盼减少。其二t 预先赋傣不影响在判瓤予镪淑含对掰产燮蠲蔻鹃可满怒性，这勰妈潦 来的遍历子句辫法相等价，因此能够获群糨同的子式。 3 ，簧对漆麟s 建弱憨疆蜜绩矮冀浚辩参数参狡羧鏊熬润蘧，探褥了渗装蓠霉法羧 耧窝藏率静彩瓣瓣律。辑诿莎长是捂簿坎遮代簇筏躐德辩变譬个数。避过霹s a t l i b 枣 蕊准蜜辍鞭避霉亍豹实验碟瓣潼爨，貔饕掺蕊静增援，辫法瓣鸯教瞧鞠散率葵现掇熊消 缓妖躺规律。谈规律为合煺利用该算法熊肖燕瑟舶参考协值。 荚键嚣； 搂鐾蔻羲，鸯器搂墅稔羧，毒嫠霉漠霪漆莲，蓑燮蕊攘蒙鬻囊臻，羧枣 研i 霹满是阀遴 酝0 d 琏黾l c 王芰鏊g k l n ga n 矜b 0 0 l e a ns a t l s f l a b i l i t y p r 0 牯l e m m i n gs h a o ( c o m p u t e ra r c h i t e c t u r e ) d i r e c t e db yp r o f x i a o w e il i a b s t r a c t l nt h ea r e ao fh a j 畦w 8 珊m o d e lc h e c k i n g t h eo r i g i n a ld e s i g ni sa b s t r a c t e d 氇sf i n i t e s t a t et r a n s i t i o ns y s t e no rk r i p k es t r u c t u r e ) w h i l et h ep r o p e r t yt ob ev e r i f i e di sr e p r e - s e n t e d 籍t e m p o r a ll o g i cl a n g u a g e i nt n sw a y , t h eo r i g i n a ld e s i g nw i l tb es m o o t h l yv e r i 一 矗缱t h r o u g hc h e c k i n gw h e t h e rt h em o d e ls a t i s f i e st h ep r o p e r t yc o n s i d e r e d o n et 酗o m e b o t t l e n e c kt op r o h i b i tt h em e t h o d o l o g yo fm o d e lc h e c k i n gf r o ma p p l y i n gt oi n d u s t r i a l a p p f i c a f i o n 拓t h ef a c tt h a tt h es i z eo ft h es t a t es p a c ei sg r o w i n ge x p o n e n t i a l l yw i t ht h e i n 娌e a s eo f 谯en u m b e ro ft h es t a t ev a r i a b l e s t h ed i f f i c u l t yl y i n gb e h i n di sh o wt or e r e s e n tt h et r a n s i t i o nr e l a t i o n s h i po ft h es t a t es p a c eo fm o d e le f f e c t i v e l y t oa l l e v i a t e o rc o n q u e rt h eb o t t l e n e c k ，r e s e 甜c h e mh a v ep r o p o s e dv 黼i o n si m p o r t a n ta p p r o a c h e s ，f o r i n s t a n c e s ，t h eo p t i m i z e dv a r i a n k so fb i r m r yd e c i s i o nd i a g r a m s b d d s ) ，a n dt r a n s f o r m i n g t h ev e r i f i c a t i o nt a s ki n t os o l v i n gt h eb o o l e a ns a i s f i a b i l i t y ( s a t ) p r o b l e m 。8 sw e l i 豁t h e v a r i o u sa b s t r a c t i o nr e f i n e m e n tm e t h o d s p e r f o r m e do nt h eo r i g i n a lm o d e l 。 u n d e rs u c hr e s e e x c hb 懿k g r o u n d s ，t h et h e g i s 勤g u 粥o nt h ef o l l o w i n gk e yp r o b l e m s ： h o wt ob u i l dac o m p a c ta n de f f i c i e n tt r a n s i t i o nr e l a t i o n ；h o wt oe f f i c i e n t l ye x t r a c tm i n i m a l u n s a t i s f i a b i e m u s u b - f o r m u l a ；t h ep r o b l e mo fs e a s i t i v i 够姆t h ep a r a m e t e rc a l l e ds t e p n u m b e rf o rt h es u r v e yp r o p a g a t i o n s p ) a l g o r i t h m a i m i n gt ot h e ep r o b l e m s ，t h et h e s i s o b t a i n e dt h e 姒l o w i n go r i g i n a li d e a sa n dc o n t r i b u t i o n s i + 疑臻s t r a t e 銎, f o r 魄澈甄壤t r a n s i t i o nr e l a t i o n s h i pi sp r o p o s e di ns y m b o l i cm o d e l c h e c k i n g i t 稔w e uk n o w nt h a tac o m p a c ta n de f f i c i e n tt r a n s i t i o ni sc r l t i c a li ni m a g e c o m p u t a t i o n 。t h er u l ep r o p o s e df o rg r o u p i n gt h ep a r t i t i o n e dt r a n s i t i o nr e l a t i o n s h i p i sb a s e do ns o f l l ec e r t a i nf e a t u r eo ft h es u p p o r to fe a c ht r a n s i t i o nr e l a t i o n s h i pp a r t 。 掣h em e r i t 螽t h i sa l g o r i t h m 法潲囊鬈挺黼拣鹑& v e l a t i o n s b 2 pi st w o - f c 连d 。o ut h e 奄鞋毽 h a n d ，t h i sm e t h o dc a ob u i l d8m o r ec o m p a c tt r a n s i t i o n ，t h ee x p e r i m e n t se x h i b i tt h a tt h e r e d u c t i o nf o rt h es i z er a n g e sf r o m3 0 t o1 0 。t h es i z ei sm e a s u r e db yt h en u m b e ro f t h en o d e si nt h eb d d r e p 撇e n t i n gt h et r a n s i t i o nr e l a t i o n s h i p ，o nt h eo t h e rh a n d t h e s t e pi ni m a g ec o m p u t a t i o ni sp a r t i m t y 糙d u e e di n 襄d 勰e 巍 模型榱竣艇其布尔可满鼠旧题的研究：麓文摘要 2 t h ep r e 删s i g n m e n ta l g o r i t h mf o ro p t i m i z a t i o no fe x a c t l ye x t r a c t i n gm us u b - f o r m u l ai sp r o p o s e db a s e do nt h ec l a u s et r a v e r s i n ga l g o r i t h m i nt h ea b s t r a c t i o na n d r e f i n e m e n tf r a m e w o r ko fs a t b a s e dm o d e lc h e c k i n g i ti sc r i t i c a lt oe x t r a c tm us u b - f o r m u l af o rt h es a t - b a s e dm o d e lc h e c k i n g f o rt h ec l a u s et r a v e r s i n ga p p r o a c h ，e a c h c l a u s ei sd e c i d e dt ob ed e l e t e do rn o tb ys o l v i n gas a t i s f i a b i l i 锣p r o b l e mr e s p e c t i v e l y 瓢# p r o p o s e do p t i m i z a t i o ni sp e r f o r m e dt h r o u g hm a k i n ga s s i g n m e n tf o rc e r t a i nv a r i a b l e si n a d v a n c e i nt h i sw a y ，t h ed e c i s i o nt a s kf o re a c hc l a u s ec a l lb er e d u c e d ，t h u st h ee f f i c i e n c y i s l a r g e l ye n h a n c e d t h ee x p e r i m e n t sc o n d u c t e do nt h ei n s t a n c e sf r o ms a t l i bs h o w t h a tt h er e d u c t i o nf o rc o m p u t a t i o nt i m er a n g e sf r o m6 0 t o1 0 ，m o r e o v e r s i n c e t h es a t i s f i a b i l i t yo fe a c hi m m e d i a t ep r o b l e mg e n e r a t e dw h e nv i s i t i n ge a c hc l a u s ec a l lb e k e p te v e na f t e rp r e 。a s s i g n i n gc e r t a i nv a r i a b l e s ，t h eo p t i m i z e da l g o r i t h ma n dt h ec l a u s e t r a v e r s i n go n ea r ee q u i v a l e n t t l 煳t h e yg e n e r a t et h ec o m m o nm us u b * f o r m u l a 。 3 ，f o rt h es e n s i t i v i t yo fs pa 涎o r i t h mo fs o l v i l _ l gs a tt ot h e s t e pn u m b e rp a r a m e t e r ， t h eo b s e r v a t i o n sa r eo b t a i n e dt h a tt h ep a r a m e t e rv a nh e n r i l ya f f e c tt h ev a l i d i t ya n dt h e e f f i c i e n c yo ft h ea l g o r i t h m t h ee x p e r i m e n t sw e r ec o n d u c t e do nt h eb e n c h m a r k ss e r i e s u fi ns a t l i b ，w h i c he x h i b i t e dt h a tw i t ht h es t e pn u m b e rv a r y i n g ，t h ev a l i d i t ya n dt h e e f f i c i e n c ys h o wa c u t e l yc o n v e r s et r e n d sr e s p e c t i v e l y s u c ho b s e r v a t i o n sc a i nh e l pu s et h i s a l g o r i t h me f f i c i e n t l yb yt u n i n gt h ep a r a m e t e ri np r a c t i c e 。 k e yw c l r d s ： m o d e lc h e c k i n g ，b o u n d e dm o d e lc h e c k i n g ，b o o l e a ns a t i s f i a b i l i t y p r o b l e m ，m o d e 主a b s t r a c t i o na n dr e f i n e m e n t ，m i n i m a lu a s a t i s f i a b t ep r o b l e m 插图目录 2 - 1 二位计数器的状态转移模型 1 2 2 - 2c t l 基本运算公式 1 5 2 3 布尔函数的真值表、二叉树、二叉决策图的表示 2 0 2 4b d d 的存储节点与支撑向量 2 2 2 - 5 转移关系各部分的分组算法 2 2 2 - 6 转移关系各分割部分的分组 2 3 2 7 分组策略与其它方法比较 2 4 3 - 1 对状态转移关系展开2 次口能的状态转移图 2 6 3 2 长度有界的路径，包含环路与不包含环路的情形 2 7 3 - 3 两个互斥进程模型的状态转移图 3 0 孓4 反例制导的抽象细化 3 4 3 - 5 模型的状态抽象例子 3 6 3 - 6 识别伪反例的分离路径算法。 4 l 4 - l 合取范式与它的接口图的例子 4 8 4 2 合取范式的诱导宽度 4 9 4 - 3 利用单位子句进行搜索空间裁剪 5 l 4 - 4d p l l 算法的迭代描述 5 1 4 - 5 割边集合与添加的子句， 5 5 4 - 6 合取范式0 l + 旺2 ) ( 现+ z 3 + 一z 4 ) ( ，z l + x 4 ) 的因子图表示 5 7 4 - 7 调查传播算法流程 5 7 4 - 8f i 种概率迭代关系的例子 5 9 4 9 步长对算法效率影响的模拟实验a 6 3 4 - 1 0 步长对算法效率影响的校拟实验b 6 3 4 - 1 1 步长对算法有效性影响的模拟实验 6 4 4 - 1 2 针对基准实例u f 集合的算法效率影响实验 6 4 4 - 1 3 针对可满足的基准实例u f 集合的算法有效性实验 6 5 5 - 1 利用分解进行简化的算法 6 9 5 - 2 识别亏数为l 算法中的分解简化过程举例。 7 0 一一竺塑苎墨夏至旦：! 墨塑望竺里塞! 堑望旦墨 5 - 3 予句分解依赖关系 5 4 冲突图b 依赖于冲突圈a 的剀r 孓5 冲突图与证据图( 虚线包围的子图) 的关系 5 - 6 利用于句的依赖关系近似提取m u 的算法误差 5 7 a m u s e 算法例子 5 - 8 实验数据 5 - 9 算法性能对比。 6 - l 端口序故障例子 6 - 2 初始向量例子 6 - 3 基丁s a t 的端日序故障的测试生成 6 4 自动产生端口序故障测试向量的算法流程 良5 对于2 阶端口序的实验数据 ；2粥竹四跎鼹鼯 s；g；g；会； 声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得 的研究成果。就我所知，除了文中特别加以标注和致谢的地方外，论文中 不包含其他人已经发表或撰写过的研究成果。与我一同工作的同志对本研 究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 作者孙研卅 日期：埘 1 科j 1 4 关于论文使用授权的说明 中国科学院计算技术研究所有权处理、保留送交论文的复印件，允许 论文被查阅和借阅；并可以公布论文的全部或部分内容，可以采用影印、 缩印或其它复制手段保存该论文。 作者鲐研1 9 翩张御啉p 嘲日 第一章引言 怎样确保集成电路芯片的设计是正确的? 这对任何涉足该领域的人们都构成了挑 战一方面，为了满足客户日益多样化的需求，芯片所要胜任的功能日新月异，这就 需要芯片的设计越来越复杂；另一方面，芯片设计厂商为了获取利润最大化，就必须 在众多竞争者中脱颖而出，到达早日上市的目标，这就迫使芯片的设计制造周期足 够短芯片的日益复杂势必会给设计带来挑战，就更有可能导致设计中的错误例 如b e n t l e y 在2 0 0 1 年设计自动化会议( d a c ) 上报告。p e n t i u m i v 的设计中被检测出 的“臭虫( b u g ) ”的数日，相比p e n t i u m p r o 增长了3 5 0 【1 ，2 】芯片设计的任何层 次的细微差错都有可能给用户和公司带来严重的后果甚至灾难。用“千里之堤，毁于蚁 穴”来形容并不为过例如，1 9 9 4 年，因为p e n t i u m 处理器浮点除法部件( f d i v ) 设 计的一个“臭虫”+ 。i n t e l 公司损失达4 7 5 亿美元 确保设计可靠性必不可少的方法是在集成电路设计过程的各个层次进行充分的、 可信的验证与测试事实上，目前在整个设计流程中，验证已经成为制约产品上市 周期的瓶颈例如【3 】列举了这样的比例，从事验证和设计的工程师人数的数目比例 为3 ：1 ，整个芯片设计流程中超过一半的工作量花费在对设计进行验证上验证的重 要性由此可见一斑用确定或者随机的方法自动产生测试向量来对设计进行模拟验证 仍然是工业界采用主流方法但是就现在集成电路的复杂功能行为，模拟的方法已经 远远不能完全覆盖设计的所有行为这就有必要采用形式的方法进行验证譬如， 在p e n t i u m i v ，以及a m d k 7 芯片中就大规模地用了形式验证f 2 ，5 ，6 】。尽管就目前 而言，形式验证的商业工具所处理的规模仍不足以对整个芯片设计进行验证但是在 对浮点运算部件以及指令译码逻辑等局部设计中，形式验证发挥了不可替代的作用 像b e n t l e y 列举的高质量的“臭虫”中，浮点乘法设计错误就是典型的案例，如果采用 纯粹随机的模拟运算来命中这个错误的概率是1 ( 5 l o ) ，如果不采用形式验证的方 法，这样的许多设计错误利用模拟验证手段几乎不能够被发现【2 】。 1 1 形式化验证方法 形式验证提出于2 0 世纪9 0 年代，被认为是一种有前途的验证方法按照【7 】的描 述，形式验证的涵义是：用形式的方法来确立设计的实现( i m p l e m e n t a t i o n ，i m p ) 满 足规范( s p e c i f i c a t i o n ，s p e c ) 的要求所谓的实现是指硬件在任何不同抽象层次的设 计，不仅仅指最终的物理版图，例如系统级，寄存器传输级，逻辑门级，晶体管级等 等。所谓的规范是指设计所要期望的并被认为是“正确”的属性，通常用形式化的方 该。臭虫。表现为【4 】；当计算浮点除法叫，时，变量取值在4 1 9 5 8 3 3 0sz 4 1 9 5 8 3 6 4 ，3 1 4 5 7 2 5 7 掣3 1 4 5 7 2 8 4 范围内t 有两个三角形区域中的2 厅的结果在小数点第5 个 育效位之后出现了计算错误 中国科学院博士学位论文：模型检验殛其布尔可满足问题的研究 法来描述 形式验证的任务是提供证明，以便确立实现满足规范的要求，证明采取形式化 的，数学的严格证明。目前主要方法包括【7 】： 定理证明将实现满足规范的关系看作是用逻辑描述的定理，而规范提供了证明 过程要利用的公理以及假设，验证的过程即证明演算的过程。 模型检验把规范表示为逻辑公式，而把实现抽象成语义模型，规范的正确性通 过这些语义模型来确立 等价性检验实现和规范抽象成逻辑公式，以及自动机的形式，用来确立实现与 规范之问的等价性关系 语言包含将实现和规范抽象成为语言，通过检验前者的语言包含在后者的语言之 中 不管采用何种方法，形式验证的最终目标是确立实现( i m p ) 和规范( 印e c ) 成立下面 的关系之一【7 】： ( 1 ) 实现与规范等价：i m p 兰勖e c ； ( 2 ) 实现蕴涵规范：i m p 辛s p e c ； ( 3 ) 实现抽象为状态转移模型，例如有限自动机，k 啷k e 结构等而规范描述为时 态逻辑，例如计算树逻辑，线性时态逻辑等该模型上的所有可能的行为满足规范的 要求：i m p s p e c 形式验证方法在其它领域也获得了成功应用，例如对机械制造系统的验证1 8 】利 用模型检验的工具s p i n 能够对一个制造系统进行安全性和活性验证又例如，在 化学工业处理领域的序列控制器系统【9 】中，也采用了形式化的验证方法它们 与v l s i s o c 的设计领域有个共同的特点就是，它们工作时候的时序行为能够抽象成有 限状态系统，而这些制造系统的合法的以及非法的操作可以借助时态逻辑中的安全性 以及活性来描述，因此在抽象的层面上看，可以用形式验证的方法来对这些系统进行 验证就是极为自然的事情。 1 2 本文研究背景及相关工作 1 2 1 符号模型检验 模型检验一词( m o d e lc h e c k i n g ) 最初在1 9 8 0 年代早期c l a r k e 和e m e r s o n 提出 【1 0 】它足一种自动化程度很高的形式验证方法它把要验证的设计抽象为状态转移 系统的模型，例如有限状态机( f i n i t es t a t em a c h i n e ) 或者k r i p k e 结构对于所要验 证的设计，模型检验所关心的是动态的、随着时间变化的行为属性，在描述这种属性 第一童引言 时，要用到时态逻辑( t e m p o r a ll o g i c ) 时态逻辑的概念最初是哲学家们在研究自然 语言中时间如何使用中引入的时态逻辑有许多种类，比较有代表意义的包括【1 1 1 ： ( 1 ) 线性时态逻辑( l i n e a rt i m el o g i c ，l t l ) ； ( 2 ) 计算树逻辑( c o m p u t a t i o n t r e el o g i c ，c t l ) ； ( 3 ) 带有路径量词的计算树逻辑c t l ；( 4 ) 命题肛一演算以及 ( 5 ) 轨迹公式( t r a j e c t o r yf o r m u l a s ) 等这些时态逻辑的表达能力各有不同，并且 所要完成的验证任务的复杂度与所采用的时态逻辑密切相关实际上在很多验证任务 中，需要在公正( f a i r n e s s ) 的假设下进行安全性( s a f e t y ) 、活性( l i v e n e s s ) 以及不 变性( i n v a r i a n t ) 的检查就能够获得比较充分的验证 最初模型检验工具的雏形采用了显式方法，用邻接表来表示模型的状态转移图 ( s t a t et r a n s i t o ng r a p h ) ，这其实是逐一枚举了系统可能到达的状态，并以此来判断 系统的行为是否满足规范中所规定的属性要求因此，早期的模型检验工具的处理能 力仅仅局限于1 0 4 一1 0 5 的状态数目的规模f 1 2 1 人们通常把这种因为模型的状态数日 随着状态变量数目的增长成指数倍膨胀，而导致内存不能容纳的现象形象地称为“状 态爆炸”或者“内存爆炸” 如何采用紧致的方法来有效的处理。状态爆炸”问题一直是模型检验的研究历 程中要克服的瓶颈。第一次突破是二叉决策图( b i n a r yd e c i s i o nd i g r a m ，b d d ) 的引 入。为了克服因为显式的方法带来的。状态爆炸”的问题，在1 9 8 7 年的秋天，卡耐基 美隆大学的m c m i u a n 【1 2 ，1 4 l 把= 叉决策图引入到模型检验中来，通过蕴含的办法，用 二叉决策图来表示模型检验中转移关系、可达状态集合，以此来进行状态像、不动点 的计算，这就是符号模型检验( s y m b o l i cm o d e lc h e c k i n g ) 的概念在同期，利用二 又决策图作为基本的数据结构，c o u d e r t 以及p i x l e y 等人提出了对确定型的有限状态机 的等价性进行检验的方法 二又决策图的想法起源于用有向无环图的方式来表示函数，这种想法最初是 由l e e 和a k e r s 提出的f , 5 1 1 9 8 6 年，b r y a n t 提出了具有正则性( c a n o n i c i t y ) 的有序二 叉决策图以及在该数据结构上的有效的算法【1 6 ，1 7 1 二叉决策图是一种表示布尔函数 的有效方法，这体现在：其一，它是一种紧致的数据结构；其二，体现在该数据结构 上的运算效率在二叉决策图上有两类节点，一种是标记为变量的内部节点，另外是 两个末端节点，标记为布尔值。真”和。假”在有序的二叉决策图的任何一条路径 上，每个变量的标记节点最多出现一次。有序二叉判定图的一个重要特点是它表示布 尔函数的正则性所谓正则性的含义是指，一旦给定布尔函数变量的某个顺序，表示 该函数的二叉决策图在同构的意义上是唯一的在二叉决策图上，布尔运算的时问复 杂度与图的规模成比例关系具体说来，对于两个二叉决策图 和，2 ， 和，2 之间的布 尔运算复杂度是l ，l i i ，2 l ，i ，i 表示给定变量的固定的顺序关系后，二又决策图，的节点 个数所以一旦能够把布尔函数用二叉决策图表示出来，通过它来进行布尔函数的运 算是效率可观的必须注意到，二叉决策图的节点数目对变量顺序非常敏感，不同的 变量顺序，对它大小的影响是显著的 3 中国科学院博士学位论文：模型检验及其布尔可满足问题的研究 征模型检验的历史上，由于引入了二叉决策图的表示方法，在验证同步时序系统 的时候，处理能力突破了1 0 2 0 的状态数量【1 3 而通过采用各种优化的方法，符号模型 检验能够处理包含几百个状态变量的系统并且利用符号模型检验的方法，对高性能 计算机中的总线协议进行了模型检验【1 8 1 这是模型检验在工业界中的典型应用 尽管符号模型检验极大地拓展了所要验证的系统的规模，在验证某些领域的系统 的时候，例如异步时序系统以及通讯系统的协议，人们却经常观察到显式的模型检验 却胜过符号模型检验，这是因为【1 5 ，1 9 i ： ( 1 ) 符号模型检验采用二又决策图的数据结构方式是用“空间”来交换“时 间”，会遇到二叉决策图的节点数目过大而无法表示的情形。几乎所有的布尔函数都 需要指数倍的存储空间，另外要使得二叉决策图的节点数目足够小，这要求变量有一 定的合适排序，而获取这样的变量顺序，要么采取各种非常耗时间启发式算法，或者 需要凭借经验的手工干预 ( 2 ) 在进行可达状态遍历的时候，符号模型检验采用的是广度优先的算法，而传 统的显式的模型检验采取深度优先的算法，往往更容易发现反例。 ( 3 ) 符号模型检验采用的是全局的搜索方式，当在进行状态原像的计算时候，不 能够避免实际上并不可达的状态 除了二叉决策图外，用图的方式来表达布尔函数有许多方法【5 2 1 。布尔 表达图( b o o l e a ne x p r e s s i o nd i a g r a m ，b e d ) 就是其中的一种【5 2 ，5 3 l ，在1 9 9 7 年 l 扫a n d e r s e n 和h u l g a a r d 提出，也是一种表示，处理布尔函数的运算数据结构。该结 构拓展了= 叉决策图，其节点除了二叉决策图中固有的末端节点以及标记为变量的节 点外，还增加了表示布尔运算的节点，它能够在线性的空间中表达任何逻辑电路并 且能够保留电路的许多有用的拓扑连接的结构属性，这对于提高运算的效率很有帮 助布尔表达图可以看作是从逻辑电路到二叉决策图之间的过渡表示方法，当在验证 中进行重言式以及可满足性检查的时候，可以把布尔表达图快速转化为二叉决策图进 行判定，这在缓解二叉决策图的“内存爆炸”问题很有帮助。 符号轨迹评估( s y m b o l i ct r a j e c t o r ye v a l u a t i o n ，s t e ) 是一种基于格论采用符号模 拟方法的模型检验，它所验证的属性用轨迹公式来描述。轨迹公式只采用了逻辑运 算。合取”( ) ，以及时态运算。下一个时刻”( x ) 最初的s t e 工具是由c a r l s e g e r 和r a n d yb r y a n t 于1 9 9 5 年开发1 5 0 ，5 1 1 i n t e l 公司将符号轨迹评估作为其形式验 证工具f o r t e 的引擎，获得了很大成功【6 】。相对于其它符号模型检验方法，它比较容 易使用。并且因为对验证完备性的妥协，而部分地缓解了。内存爆炸”问题，它不事 先对电路进行模型的抽象在s t e 运行中，所要涉及的b d d 的变量个数仅仅与所要验 证的断言有关，而与所验证的电路没有关系因此它可以处理更大规模的电路，但是 另一方面，它所能够验证的内容有限，经过扩展的符号轨迹评估能够验证安全性的属 性，而对于活性验证，符号轨迹评估还不能对此进行验证 第一章引言 1 2 2 模型检验与布尔可满足问题 1 2 2 1 有界模型检验 为了缓解或者解决符号模型检验中因为采用二叉决策图而导致的“内存爆炸”问 题，在1 9 9 9 年的d a c 会议上，b i e r e 提出了怎样在模型检验中，将求解可满足问题的求 解算法( 例如s t g l m a r k 以及d a v i s p u t n a m 的方法) 取代二又决策图的方法，这种方 法往往能够更快地找到反例，这在很大程度上加快了验证的速度很显然，有界模型 检验的出色性能得益f 位于底层的可满足问题引擎的性能现在已经涌现了众多优秀 的，性能卓越的求解可满足问题的程序，例如g r a s p 2 0 i ，s a t o 2 1 1 ，z c h a f f c h a f f 2 2 1 ， b e r k m i n 2 3 1 等由于这种模型检验在有界的状态空问中，并且局限于对线性时态逻辑 进行检验，该方法所涉及的从初始状态出发的状态路径，其长度不超过事先给定的界 限，所以把这种模型检验方法称为有界模型检验( b o u n d e dm o d e lc h e c k i n g ) 1 2 4 。 该验证方式把系统在有界的状态路径空间上的时序属性转换为布尔合取范式，通过可 满足问题的求解程序判断该公式是否满足，如果是可满足的，则相应的赋值就对应着 一个状态组成的路径，构成了所要验证属性的反例。否则表明在有界的状态路径空问 中，没有找到反例 利用该方法进行验证时，需要用户事先指定界限转移关系在指定的界限范围内 进行展开，若在这样有界的状态空间中找不到反例，那么用户就要逐步增加指定的界 限然而，并没有办法预先知道用多大的界限，转移关系在此范围内展开就能够覆盖 整个状态空间所以这种验证方式不能确保完全性。换言之，当设计的属性符合规范 的时候有界模型检验不能给出证明能够看出，在寻找规范反例的时候，有界模型检 验能够找到状态轨迹路径最短的反例，这是一种很好的特点，路径短往往意味着反例 不复杂，易于使用者分析 能够保证验证完全性的界限被称为完全性阈值，或者系统的状态半径理论上。 有界模型检验算法的复杂度存在着更坏于传统的模型检验的指数倍差距这是因为阈 值的大小与状态变量的数目成指数倍关系 6 6 1 ，因此对应的合取范式中变量数日也成 指数倍增长另一方面，有界模型检验不存储已经访问过的状态集合，对于每一个可 迭状态，有界模型检验可能访问指数倍的次数，而对于两个可达状态之间的任何路径 都有可能走过但是在实际应用中，有界模型检验反而有着更好的性能，这是因为， 有界模型检验是在寻找反例，并非证明不存在反例，而且它找到的反例对应得状态路 径最短，对应的合取范式的变量数目往往不是指数倍的但在实际应用中的可满足问 题的求解引擎往往并不对变量的数目敏感。 有界模型检验已经在学术界和工业界获得了认可，例如，下面就是这种验证方法 成功应用的范例。 1 以s a t o 和g r a s p 作为主要的可满足问题引擎，m o t o r a l a 的p o w e r p c 微处理 器的安全性通过有界模型检验的方法获得验证 2 7 1 中国科学院博士学位论文：模型检验及其布尔可满足问题的研究 2 在对c o m p a q 的a l p h a 的微处理器的模型检验中，“利用基于可满足问题的方 法( 有界模型检验) ，发现某些。臭虫”的时间从几天缩小至几分钟”在该工具中 应用的s a t 引擎是g r a s p 和p r o v e rf 2 8 1 3 t h u n d e r 和f o r e c a s t 是i n t e l 公司进行有界模型检验的工具前者t h u n d e r 基于 求解可满足问题得引擎s i m o ，而后者基于二叉决策图。前者应用于p e n t i u mi v 的 实际的设计验证中经过实验对比，前者因使用了求解可满足问题的引擎，对于验 证p e n t i u m i v 设计时，在生产量( c a p a c i t y ) 和生产率( p r o d u c t i v i t y ) 两方面明显优越 于后者f o r e c a s t 2 9 1 1 2 2 2 求解布尔可满足问题 作为经典的p 完全问题，可满足问题( b o o l e a n p r o p o s i t i o n a ls a t i s f i a b i l i t yp r o b - l e m ，s a t ) 也是处理布尔函数的一种常用方法，它指的是，给定一个布尔函数，问是 否存在对它变量的某种赋值使得函数的值为真，或者给出证明，对于变量的任何赋 值，该函数的值恒为假称前者情况为可满足的( s a t i s f i a b l e ) ，而称后者为不可满 足的( u n s a t i s f i a b l e ) 在人类对大规模计算问题寻求高效率的算法的努力中，可满 足问题扮演了极为重要的角色，例如2 0 0 2 年科学杂志列举的可满足问题的种种应用， 包括规划调度，对光纤的布线，寻找蛋白质的折叠态，以及对计算机芯片进行验证 等 3 0 1 。 可满足问题一般采用合取范式的方式，合取范式是一些子句的“与”，而子句是 一些字的“并”，而字是布尔变量的否定或者肯定的形式采用合取范式的表示方法 简洁而有效，并且表示布尔函数的其它方式都可以通过引入辅助变量在多项式时间内 转化为合取范式给定某个布尔函数用合取范式来表示它的方法不是唯一的，即它不 是一种正则的表示方法，这种表示方法不会像二叉决策图那样，其节点数目随布尔变 量的数目成指数倍增长 能够用求解可满足问题的引擎来解决模型检验中的问题得益于近十几年来该研 究领域的进展可满足问题并非新鲜事物，早在上2 0 世纪的6 0 年代，d a v i s ，p u t n a m e ， l o n g e m a n n ，l o v e l a n d 等人就对解决该问题进行了研究，人们综合称他们的基本算法 为d p l l ，可以说这是一种最为常用的算法。作为a l p - 完全问题的原型，可满足问题在 理论界也被广为关注，尽管被认为不可能存在多项式范围内求解它的算法，但是并不 能排除针对各个特定领域出现的各类可满足问题有很高效率的算法综述【3 1 l 把求解 可满足问题的算法分为完全算法和不完全算法两类给定一个可满足问题，完全算法 要么求出它的一组可满足的解，要么能够证明不存在这样的解使得它满足。而不完全 算法通常采用