（计算机软件与理论专业论文）基于断言的仿真算法与实现.pdf

基于断言的仿真算法与实现 摘要 v e r i l o g 是当前应用最为广泛的硬件设计语言之一，它可以用于硬件系统各种 级别的设计、综合、仿真。p s l 是一种标准的描述硬件和嵌入式系统规范的语言 ( i e e e 一1 8 5 0 ) 。p s l 的简单子集p 虹“咄是指满足单调时序步进的p s l 语言子集， 较易被模拟仿真。本文主要研究了基于p s l 断言的v e r i l o g 仿真算法和实现技术。 本文首先研究了作用在有限长字符串上的p s l 公式满足强度，然后分别对 p s l 强满足、弱满足和强违背提出了在有限字符串上的组合定律，由此本文定义 了检测p s l s 删- e 公式强满足、未决和强违背的条件。本文使用自动机作为p 趾”吣 动态验证器的验证引擎。虽然交替式自动机( a f a ) 在表示线性时态逻辑时具有线 性空间复杂度，但是p s l 是带循环的语言，a f a 也不支持同步p s l 。长度匹配 语句”的所有分支，所以本文提出了局部变量增强的交替式自动机( l a f a ) ，解 决分支同步和循环计数的问题。 本文也重点讨论了基于断言的仿真器实现方法。我们使用有向无环图表示 l a f a 的运行轨迹，并用符号化的方法编码状态和局部变量。该编码方式允许对 状态和局部变量多重赋值，状态的不同值代表l a f a 不同的执行结果。通过以上 方法，我们能够维持验证在时间和空间上的线性复杂度。 在本文的最后我们考察了v e r i l o g 仿真参考模型，在开源项目i c a r u sv e r i l o g 和g t k w a v e 的基础上开发了p s l s o 础v e r i l o g 动态验证器原型，并给出了一个完 整的实例。 关键字：仿真器，动态验证，基于断言的验证，自动机构造，性质规范语言 基于所言的仿真算法与实现 a b s t r a c t v e r i l o gi s aw i d e l yu s e dh a r d w a r ed e s c r i p t i o nl a n g u a g e ( h d l ) t od e s i g n , s y n t h e s i z e ，a n ds i m u l a t eh a r d w a r es y s t e m i nd i f f e r e n tl e v e lp s li sas t a n d a r d s p e c i f i c a t i o nl a n g u a g e ( i e e e 一1 8 5 0 ) f o rh a f d w a r a n de m b e d d e ds y s t e m s t h es i m p l e s u b s e to fp s l 妒s d ”c o n f o r m st ot h en o t i o no fm o n o t o n i ca d v a n c e m e n to ft i m e w h i c hi nt u r ne n s l h t st h a tf o r m u l a sw i t h i nt h es u b s e t 啪b es i m u l a t e de a s i l y i nt h i sp a p e r , w ew o r ko nt h et h e o r i e sa n dm e t h o d sf o rd e s i g no fd y n a m i c v e r i f i e r sf o tp s e 啾w ef i r s ts t u d yt h ef o r m a l i s m 妇乜池f o r m u l as a r i s f a c t i o no v o r f i n i t ew o r d s t h e n , w ee x p l o r et h ec o m b i n a t i o n a ll a w so ff i n i t ew o r d sw i t hr e s p e c tt o s t r o n gs a t i s f a c t i o n , w e a ks a t i s f a c t i o na n ds t r o n gv i o l a t i o n i tc o n t r i b u t e sa c c e p t a n c e c o n d i t i o n sf o ra u t o m a t at or e c o g n i z cn o tj u s tv i o l a t i n g , b u ta l s os t r o n g l ys a t i s f y i n g a n dp e n d i n gw o r d sl 帆越p s d 啾s t l u c t u r o $ w e 、坞ea u t o m a t aa st h ev e r i f i c a t i o n e n g i n e a l t e r n a t i n g f i n i t ea u t o m a t a ( a f a ) h a sl i n e a r s p a c ec o m p l e x i t y i n r e p r e s e n t i n gl i n e a r - t i m et e m p o r a ll o g i c s b u tp s l i sn o ta s t a r - f r e e l a n g u a g ea n d a f ai sn o tc a p a b l ef o rs y n c h r o n i z i n gb r a n c h so f s e q u e n c el e n g h - m a t c ho p e r a t i o n , s o w ep r o p o s ot h el o c a l v a r i a b l e - e n h a n c e da l t e r n a t i n gf i n i t ca u t o m a t a ( u 心a ) 勰t h e r u n t i m e c h e c k e r f o r p s e 哪t h es i z e o f a l 蛋a 毡、i n e a r t o t h es i z e o f i t s p s e 唧k f o r m u l a i nt h i sp a p e r , w ea l s op r o v i d ei m p l e m e n t a t i o nm e t h o d sf o ri a f ar a n g i n gf r o m s t a t i cr e p r e s e n t a t i o nt or i m - t i m ev e r i f i c a t i o ne n g i n e s w ei i s cd i r e c t e da e y c l i cg r a p h s ( d a g ) t or e p r e s e n ta l lp o s s i b l er u n so fal a f a m o r e o v e r , w ee n c o d es t a t e sa n d l o c a lv a r i a b l e sb ys y m b o l i ca p p r o a c h e s t h ee n c o d i n ga l l o w sm u l t i p l ea s s i g n m e n t st o s t a t e sa n dl o c a lv a r i a b l e si nac o n f i g u r a t i o n d i f f e r e n tv a l u e so fas t a t eo rv a r i a b l e s t a l l df o rd i f f e r e n te x e c u t i o nr e s u l t so fal a f a b yt h e s em e t h o d s w ea 砧a b l et o m a i n t a i nt h el i n e a rc o m p l e x i t yo f v e r i f i c a t i o ni nb o t hs p a c ca n dt i m e i nt h ee n d , w es t u d yt h er e f e r e n c em o d e lo fv e r i l o gs i m u l a t i o na n dd e v e l o p8 p r o t o t y p eo fp s l 5 u a * _ v e r i l o gd y n a m i cv e r i f i e ri ns u p p o r to fi c a r u sv e t l o g a n d g t k w a v e ac o m p l e t ee x a m p l ei sa l s oi n c l u d e di nt h el a s ts e c t i o n k e y w o r d s ：s i m u l a t o r , d y i l a m i cv e r i f i c a t i o n , a s s e r t i o n b a s e dv e r i f i c a t i o n , a u t o m a t ac o n s t r u c t i o n , p r o p e r t ys p e c i f i c a t i o nl a n g u a g e 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及 取得的研究成果。据我所知，除文中已经注明引用的内容外，本论 文不包含其他个人已经发表或撰写过的研究成果。对本文的研究做 出重要贡献的个人和集体，均已在文中作了明确说明并表示谢意。 作者签名：立丝选交皿日期：# 毕 学位论文授权使用声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版。有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆被查阅。有权将学位论文的内容编入有关数据库进 行检索。有权将学位论文的标题和摘要汇编出版。保密的学位论文在 解密后适用本规定。 学位论文作者签名：知心崩曳蔼 日期：血弘l 基于断言的仿真算法与实现 1 1 背景 第1 章概述 自从半导体工艺跨入亚微米时代，一颗芯片通常可容纳百万以上的晶体管门 电路，从而使具备完整系统结构与功能的片上系统( s y s t e mo i lc h i p ，s o c ) 有了实 现的可能。s o c 技术可将执行控制，运算或信号处理功能的处理器、存储器、周 边电路及特制逻辑电路( i n t e l l e c t u a lp r o p e r t yc o r e s ，i p 核) 整合到一块芯片中。但是 一块有缺陷的芯片不仅当其返工时增加设计费用，而且会拖延其上市时间，冲击 产品收益，缩小市场份额，使公司陷于穷于应付的困境。这促进了电子设计自动 化( e l e c o n i cd e s i g na u t o m a t i o n 简称e d a ) 的迅猛发展。e d a 技术是以计算机为 工具，设计者在e d a 软件平台上，用硬件描述语言h d l 完成设计，然后由计算 机自动地完成逻辑编译、化简、分割、综合、优化、布局、布线和仿真，直至对 于特定目标芯片的适配编译、逻辑映射和编程下载等工作。e d a 技术的出现， 极大地提高了电路设计的效率和可靠性，减轻了设计者的劳动强度。 在电子设计自动化流程中，设计验证是必不可少的。验证作为集成电路设计 的重要组成部分，伴随着集成电路设计的每个阶段，贯穿整个设计过程始终 过去对系统的功能规范说明都是采用自然语言，这种说明形式一般都是比较 含糊的，因此工业界和学术界涌现出多种为芯片设计开发的规范语言，如m m 的s u g a r 语言，i n t e l 的f o r s p e c 语言和m o t o r o l a 的c v b 语言等。但各机构各自 为战的局面不利于芯片验证工具链的整合。这促使了以制定片上系统标准为己任 的a c c e l l e r a 委员会在2 0 0 0 年成立。a c c e n e r a 委员会中的成员大多来自于诸如 h t e l , c a d e n c e ，i b m ，f r e e s c a l e ，s y n o p s y s 等知名芯片制造商和电子设计自动化工 具公司。a c c e l l e r a 形式化验证子委员会在同年启动了性质规范语言p s l ( p r o p e r t y s p e c i f i c a t i o nl a n g u a g e ) 的定制工作，2 0 0 5 年9 月，p s l 已正式成为i e e e - 1 8 5 0 标准。面向p s l 语言的研究在西方国家得到了普遍的重视。欧盟在2 0 0 4 年开始 赞助意法半导体公司，德国i n f m e o n 公司领导的p r o s y d 计划 3 5 】。该计划的目 标是通过建立标准的、集成的、面向性质的电子系统设计流程将欧洲芯片工业的 生产力提高3 0 。该计划的核心是围绕p s l 语言建设高可信芯片设计验证平台。 可见p s l 语言在欧美芯片设计与制造业受到了普遍藿视 本文的研究目标是以形式语义，模型检验和自动机理论为依据，提出一套切 实可行的算法，为功能仿真添加断言机制，同时根据这套算法实现相关工具软件。 基于断言的仿真算法与实现 1 2 芯片设计验证技术 设计过程是根据系统规范编码实现的过程。在规范层次上，规范指明设计所 执行的功能但并不涉及如何执行。根据规范的编码给出了功能实现的细节。规范 与实现方案是在不同层次上描述系统行为的一种形式。芯片设计描述可以分为多 个层次：功能性规范、算法描述、寄存器传输级( r e g i s t e rt r a n s f e rl e v e lr t l ) 、 门级喇表、晶体管级网表和物理布图。规范的抽象层次要比实现方案的抽象层次 高。 设计验证从一个实现方案开始，并且确认该实现方案是否满足设计规范。于 是在设计的每一步骤都有验证步骤与之对应。例如，把功能规范转换为算法实现 的设计步骤要求有验证的步骤，以确保其算法能执行规范中的功能。与此类似， 在物理层从门级嘲表生成的布图也需要验证以确保布图与门级嘲表的一致。总之 芯片设计验证包含许多方面，比如，功能验证、时序验证、布图验证和物理验证 等。 图1 1 芯片设计与验证流程 如图1 - 1 所示，功能验证是设计验证的核心内容，覆盖前端设计的所有阶段。 是验证中最复杂，工作量最大同时也是最灵活的部分，包括系统级验证、行为级 基于断言的仿真算法与实现 验证和r t l 级功能验证。对于验证系统面言，逻辑设计是验证对象，称为d u v ( d e s i g nu n d e rv e r i f i c a t i o n ) 。如果将d u v 看作是一个箱子，那么根据验证系统对 箱中内容知道的多少，可以将验证分为黑盒验证、白盒验证和灰盒验证。黑盒验 证不涉及d u v 内部结构和实现方法，d u v 内部对验证是不可见的，即使找到了 错误也不能确定错误产生的根源。这种验证方法与设计实现方式无关。白盒验证 对d u v 内部有完全的了解和控制，在这类验证中所采取的验证方法与设计实现 方式紧密相关。 1 2 1 仿真 传统的功能验证方法主要是仿真。它的流程是将激励信号施加于d u v 的输 入端，经过仿真器的分析计算，然后在监视器上观测输出结果，并且与预期的输 出结果相比对，从而确认设计的正确。仿真一般采用t e s t b e n c h 和d u v 相结合的 体系结构，包含三个环节：测试向量生成、仿真计算和结果分析。用于仿真的激 励称作测试向量，执行一次仿真所施加的一组测试向量称为测试向量集。测试向 量集可以是由人工完成的也可以是自动生成的。对d u v 施加测试向量后，仿真 器根据设计模型分析运算。 仿真器可以是由事件驱动的软件，基于周期的软件，也可以是硬件模拟器 1 事件驱动的仿真器 每当一个门的输入或者对值的变化敏感的语句块检测到变量值发生改变时， 事件模拟器就对门或者对这个语句块求值。一个值的变化称为事件事件驱动的 仿真器是时钟域抽象的。异步电路不涉及时钟而不需要明确定义时钟域，因此这 类仿真器可以用来仿真异步电路。 2 基于周期的仿真器 基于周期的仿真器依据时钟域来分割电路，并在每次时钟跳变边沿时对该时 钟域的分支电路进行一次求值。对于一个要进行基于周期仿真的电路，必需完整 地定义电路中的时钟域。因此这类仿真器可以仿真同步系统。 3 硬件仿真罂 硬件仿真器使用现场可编程门阵列( f p ( i a ) 的硬件单元建立电路模型来模拟 设计中的门。这样硬件的运行结果就是设计的仿真结果。当仿真器求出中间结果 给出输出波形后，把输出结果与预期进行比对，当发现非预期的输出时，必需与 设计者沟通并修复错误。仿真验证的典型流程参见图l - 2 。 基于断言的仿真算法与实现 硬件模拟加速 基于周期的仿真 基于事件的仿真 验 证 效 塞 图1 - 2 仿真验证流程 设计复杂度 图1 3s o c 验证与设计的巨大鸿沟 仿真的缺点是在设计早期出现的功能错误，往往在整个仿真结束后才能发 现。而且，在输出出现错误时，很难在错综复杂的信号里抓取所要的信号序列， 需要耗费大量的调试时间来判断到底是哪个环节出现了问题。虽然现在大多数仿 真工具都支持代码覆盖率检查，但即使是达到1 0 0 的代码覆盖率，也不能保证 1 0 0 的功能覆盖率。更为重要的是随着芯片复杂程度的增加，芯片的验证要花 费越来越多的时间，即使使用f p g a 硬件加速，仿真的验证效率也在不断下降， 基于断言的仿真算法与实现 而同时验证的复杂度在不断上升，单纯的基于测试向量的仿真已经难以满足s o c 验证的要求。 1 2 2 形式化验证 由于仿真存在局限性，所以人们开始研究形式化验证。形式验证从数学上证 明系统是否实现了设计者的意图。这意味着首先要用某种语言和逻辑构造系统的 数学模型，然后运用严格的数学推理来证明设计的正确性。与仿真不同，形式验 证不需要生成测试向量。形式化验证最早可追溯到6 0 年代，f l o y d , h o a r e ，d i j s t r a 是该领域研究的先驱。他们倡导用数学方法研究程序的行为，并提议用断言 ( a s s c r t i o n ) 来描述程序的行为特性。p n u l i 在7 0 年代晚期提出了时态逻辑 ( t e m p o r a ll o # c ) 理论。在时态逻辑的支持下，工程师可以用通俗的语言描述信号 变化的时序关系。基于时态逻辑的工具研究是由c l a r k e ，e m e r s o n 等开创的。他 们将计算树逻辑与有限状态机模型相结合来考察并发系统的行为。8 0 年代早期， 二叉判定图( b d d ) 的诞生解决了c l a r k e 与e m e r s o n 算法中的状态爆炸问题，并出 现了状态数可达1 0 2 0 的模型检验算法。到9 0 年代中期，形式化方法已能处理可 达状态规模为l o 啪的系统的验证问题。 形式化验证技术分为三类：等价性验证、性质检验和定理证明。 i 等价性验证 等价性验证是把两个电路转换为范式( c a n o n i c a lr e p r e s e n t a t i o n s ) ，并比较它 们它的特点在于，两个逻辑功能等价当且仅当它们的范式是同构( i s o m o r p h i c ) 的。简化的有序二叉判定图( o b d d ) 就是一种范式。两个等价电路的有序二叉判 定图是同构的。等价性验证广泛应用于确保一个布图和r t l 版本的一致。这是 通过抽取布图布线的晶体管网表并与其r t l 版本的晶体管网表进行比较完成的。 如果等价性验证失败，检验程序将生成输入向量序列，当该向量序列被仿真时将 显示两个电路之间的差别。 2 性质检验 另一种形式化验证是性质检验。“性质”是指系统预期行为的组合。它表示 了布尔表达式、序列表达式和其他性质之间的逻辑和时态关系。这些表达式共同 表达了特定的系统行为。性质可以分为安全性质( s a f e t yp r o p e r t y ) 、活性性质 ( 1 i v c n c s sp r o p e r t y ) 和公平性质( f a i r n e s s ) 。安全性质说明了在任何时刻没有坏的事 情发生，所以在任何采样时刻，安全性质都必需满足。活性性质说明了好的事情 最终将一定发生。例如性质。当客户端发出r e q 请求信号，服务器定会最终返 回一个a c k 确认信号”就是活性性质。公平性质描述的是某事件必需无限经常地 发生。性质检验的思想是在整个状态空间中搜索不符合性质的点。若发现这种点， 基于断言的仿真算祛与实现 则性质不满足，该点就成为一个反例。根据这个反例可以导出波形，用户排除缺 骼。否则，性质就是满足的。 3 定理证明 第三种形式化验证方法是定理证明。它利用演绎推理的方法，在证明过程中， 把性质表述为数学命题，把设计表述为数学实体。并把数学实体作为若干个公理。 其目标是。确定命题是否可以从公理中演绎得到。如果可以，性质就得到证明。 目前最常用的是由剑桥大学研发的高阶逻辑定理证明系统h o l ( h i g ho r d e r l o g i c ) 。h o l 通过元语言m l ( m e t a - l a n g u a g e ) 与用户交互，由用户选择推理规 则，h o l 应用这些规则。h o l 已成为验证复杂系统的有力工具。目前h o l 已 有庞大的研究团体和用户群。 形式化验证的典型流程如图1 _ 4 所示。 图1 4 形式化验证流程 仿真与形式化验证的主要差别在于，前者需要输入向量而后者不需要。仿真 的基本思想是首先生成输入向量，然后产生参考输出。形式验证的思维过程正好 相反，用户首先说明所期望的d u v 输出行为，然后用形式验证工具检验是否能 够证明或反驳。 形式化验证的主要优点是完备性。但是形式化验证工具对使用者有较高的数 学技能和经验上的要求，如定理证明需要人工指导。另外形式化验证存在状态空 间爆炸问题。因此，形式化验证目前还不能取代仿真，两者各有优势，互为补充。 基于断言的仿真算珐与实现 1 2 3 基于断言的半形式化验证 由于仿真和形式化验证各有优缺点，半形式化验证在工业设计实践中有广泛 的应用，比如基于断言的验证技术。 “断言”是由一组语句组成的结构，是系统设计期间对信号或者变量的条件 检测的一个任务或者是一个函数，如果违反条件，仿真器将发出一个能识别其出 现位置的出错信息。举一个断言的例子：每当低电平有效信号w r 为低电平时芯 片选择c s 为高电平。如果不满足此要求，则断言失败并发出一条出错信息。断 言可以用v e f i l o g 语言书写为： 、i f d e fa s s e r t i o n i f ( ( w r = = 1 b 0 c s = = i b 1 ) 一1 b 0 ) s d i s p l a y ( ”e r r o r ：a s s e r t i o nf a i l ” ； e n d i f 断言描述设计的性质，将此断言嵌在设计中，或放在一个单独的外部文件中， 在仿真或形式验证的过程中，断言将被仿真工具或形式验证工具检查，设计者就 能够知道设计是否满足所描述的功能行为。如果设计不满足性质则断言失败并发 出一条出错消息。这种验证方法就是基于断言的验证( a s s e r t i o n - b a s e d v e r i f i c a t i o n ，简称a b 。 有两种方法定义断言。可以从规范开始并推断系统设计的某些行为或者性质 必需成立，这些行为或性质称为肯定断言( a f f i r m a t i v ea s s e r t i o n ) ，或者可以从设计 错误或者某些特征或未指定的行为开始，推导那些表示出现异常时遇到的条件， 并且断言这些条件必定不能满足，我们称这些断言为矛盾断言( r e p u d i a 6 v e a s s e r t i o n ) 。肯定断言与矛盾断言均来源于并整理为测试规划中的条目。测试条目 阐述需要验证的功能和特征，断言则把这些目标转换为可测量的信号和变量。因 此，在建立一个健壮的断言规划之前，应当先有一份详实的测试规划。 基于断言的验证技术优势： 1 增强对错误的可观察性和可调试性 断言可以插入在d u v 的任意位置，以便立即检测设计错误。如果不使用断 言，就必需用原始输出来探测错误，这些错误经常在发生之后许多周期才显示出 来，从而使调试变得困难。因此使用断言的一大好处是能增强对错误的可观察性 和可调试性。 2 通过口使用正确性检查提升i p 集成的有效性 断言可以精确地描述口接口规范，这有利于其他设计者对口的理解和更改， 因此保证了m 使用的正确性，减少维护费用，简化了可重用口核的验证。 3 可作为无歧义的文档增进代码理解 基于断言的仿真算法与实现 封装在r t l 中的断言是一种非常好的文档记载形式。其他工程师能够根容 易理解r t l 代码块的作用及代码块之间的连系。 由于断言可以简结地使用时态逻辑描述系统的性质，它已作为设计工程师和 验证工程师之间沟通的桥梁。一些断言标准如o p e nv e r i f i c a t i o nl i b t a r y ( o v l ) 、 p r o p e r t ys p e c i f i c a t i o nl a n g u a g e ( p s l ) 、s y s t e mv e r i l o ga s s e r t i o n s ( s v a ) 被欧美一 些专业芯片验证工具开发公司所采纳，例如c a d e n c e 的i n c i s i v e ，m e n t o rg r a p h i c s 公司的q u e s t a ，s y n o p s y s 公司的v c s 等己支持s v a ，而m e n t o rg r a p h i c s 的 m o d e l s i m ，c a d a l o e 的i n c i s i v e ，s y n o p s y s 的m a g e l l a n 等都将p s l 融入到自身 的验证工具中。 1 3 相关工作 1 3 1 基于断言的验证工具 a b a r b a n e l 等【1 】研究了f o c s ( f o r m a lc h e c k e r s ) 框架( 图1 5 ) 。f o c s 是i b m 形 式化验证工具集r u l e b a s e 中的一个独立组件，f o c s 框架可以从r c t l 规范生成 性质检查器( 用v h d l 描述) 。检查器被整合入设计d u v 中。在仿真时，检查器 监视设计的运行路径，识别性质断言的成败。f o c s 把r c t l 转换成v h d l 的方 法是：首先把每一条性质转换成非确定性自动机n f a 和一个简单的a g ( p ) 公式， p 是布尔表达式。n f a 含有一组不同的错误状态，a g 0 ) 公式指出n f a 永远不会 走到这组错误状态。如果n f a 转移到这组错误状态，那就表示d u v 与规范不匹 配。由于目前的仿真器不支持非确定性，所以非确定性自动机n f a 必需转换为 确定性自动机d f a 。d f a 随后被翻译成v h d l 线程r c s 检查器。a g p ) 公 式被转换成v h d la s s e r t s ) 语句。仿真器在运行时检查s 嘶) 语句并输出断言 结果。 图1 - 5 f o c s 框架 甲 基于断言的仿真算法与实现 1 3 2 在有限长路径上的时态逻辑语义 性质表述了待验证系统运行过程中应该具有的时态性质或功能。三种经常需 验证的性质是：安全性质、活性性质和公平性质。a l p e r n 和s c h n e i d e r 3 认为所 有的性质都是安全性质和活性性质的交。安全性质说明了有限的执行路径而活性 性质说明了无限的执行路径。 动态验证器检查无限执行路径的有限前缀。l t l 的语义定义在无限长路径 上，所以我们无法使用l t l 的无限长语义验证在有限长路径上的公式。e i s n e r 等【6 】【7 】【8 】研究了在有限长路径上的时态逻辑的拓扑特性，给出了l t l 弱满足和 强满足的定义。使用 仁5 磙示模型w 满足伊，其中s 如果是。一”表示弱满足， 。+ ”表示强满足。他们还在【7 】中讨论了l t l 有限长语义的特性。在【8 】中采用 了上和t 定义时态逻辑操作语义。 1 3 3 自动机非空性分析与规范子句的正确性验证方法 在形式验证中，使用m , s o l = f 表示模型m 在状态s o 满足规范子句 如果能 够为给定的模型m 找到一个起始点s o 使得，成立，那么规范子句。r 就是可实现的 一个规范子句是可实现的，当且仅当与该语句等价的自动机所接受的语言是 非空的。基于自动机非空性分析方法的时态表达式子句验证由两个步骤组成：1 ) 规范到自动机的编译，2 ) 自动机非空性分析。将时态表达式翻译到何种自动机是 由非空性分析方法决定的。 我们知道对c t l 、l t l 、s e r e 等多种信号时态表达式的自动机编译及相应 的验证算法研究已经有了丰硕的成果，( 见图1 - 6 ) 。 图1 - 6 自动机非空性分析的计算复杂度 1 v a r d i 2 4 指出将u l 编译为b f i c h i a u t o m a t a ( b a ) 的空间复杂度是指数式 的，b a 非空性检查的时间复杂度是线性的。将l t l 编译为l i n e a r w e a k a l t e r n a t i n g a u t o m a t a ( l w a a ) 的空间复杂度是线性的，l w a a 非空性检查的时间复杂度是指 数式的。 2 v a r d i 3 1 进一步指出将c t l 编译为w e a ka l t e r n a t i n gt r e ea u t o m a t a 基于断言的仿真算法与实现 ( w a t a ) 的空间复杂度是线性的，而w a t a 非空性检查的时间复杂废是指数式的 3 f i s m a n 4 1 则指出将s e r e 到编译到n o n - d e t c r m i n i s f i cf i n i 把a u t o m a t a ( n f a ) 的空间复杂度是指数式的，将s e r e 编译到a l t e r n a t i n ga u t o m a t a ( a a ) 的空 间复杂度是线性的。 近年，自动机转换与非空性检查的算法研究是形式化验证领域的热点。g a s t i n 和o d d o x 1 2 给出了l t l 到b a 的最有效算法；r o v e r i 4 2 给出了在f i s h e r 和 n o e l 4 1 1 的s i m p l i f i e dn o r m a lf o r m ( s n v ) 的基础上用命题可满足性( s a t ) 算法验 证l t l 非空性的方法，并开发了以l t l 为规范语言的需求分析工具r a t ：中科 院软件所张文辉教授 4 3 1 用自动机空间分割方法以加速非空性验证。m e r t z 和 s e z g i n 4 4 1 给出了l w a a 的非空性验证方法，和精确的算法复杂度指标。 p s l 许多规范子句不是单纯的c t l ，l t l 或s e r e 。而是以l t l s e r e 和 c t l s e r e 的混合形式出现的。不同类型自动机的组合与其非空性检验也是重要 的研究课题。 1 3 4p s l 到自动机的转换技术 根据a b a r b a n e l 的方法，p i d a n d 5 等提出了动态验证p s l 公式的优化算法。 该算法首先把p s l 公式转换成非确定性有限自动机( n f a ) ，然后用离散转移系统 ( d i s e r e t e t r a n s i t i o n s y s t e m ，d t s ) 实现n i a ，最后把d t s 转换v e r i l o g h d l 代码。 转换流程如图1 7 ： 图1 7 d t s 转换流程 f i s m a n 等【4 】定义了p s l 的核心逻辑，称为l t lw r 。它包含l t l 和正则表 达式。他们假设每一个l t lw r 公式- r 都存在一个非确定的b f i c h i 自动机( n b a ) ， 因为路径长度匹配操作，；的存在，s e r e 编译到n b a 的空间复杂度是2 p ”， 其中月是s e r e 公式的大小。在这样大的状态空间下，使用自动机非空性验证是 非常难实现的。因为n f a 是n b a 的一部分。p i d a n 的算法和f i s m a n 的算法具有 相同复杂度。 交替式自动机( a l t e r n a t i n gf i n i ma u t o m a t a , a f a ) 4 在表达时态逻辑时比n f a 简洁。a f a 的大小与，的大小保持线性关系。f e i l 【b e i n e r 和s i p m a 2 3 提出了3 个 算法检查实时系统运行时是否满足l t l 规范。这些算法用深度优先法、广度优 先法和逆向搜索法遍历自动机。 f i s m a n 等也同样使用a f a 作为中间形式把l 1 乙w r 转换为n f a 。因为交 基于断言的仿真算法与实现 替意味着自动机的运行可能在同一时刻不同的分支包含接受状态和违背状态。所 以传统的a f a 对路径长度匹配操作嘲没有设接受状态。所以不可能把 出i 和其它公式顺序连接。所以f i s m a n 的a f a 转换算法未对路径长度匹配操 作进行转换。 1 4 本文研究内容与贡献 正如前面所述，随着集成电路制造技术和计算机技术的飞速发展，验证在芯 片设计过程中已是必不可少。本文重点研究基于断言的动态仿真验证技术，着重 探讨了基于断言的仿真算法与实现。 相比其他科研机构的工作，我们通过为a f a 添加局部变量的方法解决了 f i s m a a 的问题【2 6 】。所有由脱 睥正则表达式转换而得的自动机都有接受状态。 所以我们的动态验证器支持所有的尸龇“肚公式，并且自动机的状态数与公式的 大小保持线性。因此本文的研究工作是比较新颖和及时的。 1 4 1 研究内容 本文的研究内容包含： 1 可验证p s l 的语法和语义子集 性质规范语言是验证的关键要素，选取合适的语言子集是建设前端工具平台 的第一步。芯片设计验证可分为动态验证和静态验证。动态验证类似于仿真技术， 通过观察被测设计在外界激励下的行为，来检验设计的正确性。静态验证又称为 模型检查，它遍历设计的状态空间，无需测试用例即可验证设计的正确性。i e e e 在制定p s l 规范时定义了较宽的描述范围，使得该语言既可以使用在动态验证 中也可以使用在静态验证中。对于动态验证，p s l 规范定义了一个适用于仿真的 语言子集p s l , i 帅。本文详细的考察了它的语法和语义。 2 p s l 满足在有限长字符串上的组合定律 p s l 是由时态逻辑和s e r e 构成的带循环的语言，p s l 的许多规范子句不 是单纯的c t l 、m 或s e r e ，而是l t l s e r e 和c t l s e r e 的混合形式出现。 基于断言的动态仿真器的输入是有限长字符串。我们使用e i s n e r 等提出的拓扑理 论，并把它运用在有限字符串上的组合定律。所以我们可以通过先验证p s l 的 子公式进而得到其父公式的验证结果。 3 p s l 断言与v e r i i o g 仿真引擎相结合机制 我们使用自动机作为p s l 断言验证的引擎，考察了非确定性自动机、b f i c h i 自动机和交替式自动机，并提出了带有局部变量的交替式自动机。针对p s l 的 基于断言的仿真算法与实现 时态逻辑部分和s e r e 部分，我们提出了对应的自动机转换算法。我们研究了 v e r i l o g i e e e1 3 6 4 - 2 0 0 1 规范中定义的仿真参考模型，明确了v e r i l o g 的仿真语义， 确定了p s l 验证引擎和v e r i l o g 仿真算法相结合机制。 4 p s l 蛐- v e r i l o g 动态验证器的实现技术 本文在开源项目的基础上开发了p s l 动态验证器，研究了动态验证器的实 现机制。设计了高模块化和高开放式的系统架构，具备高健壮性，可维护的，结 构好的特点。 1 4 2 本文贡献 综上所述，本文的贡献在于： 1 把e i s n e r 等提出的拓扑理论运用在有限字符串上的组合定律。 2 提出了局部变量增强的交替式自动机( l o c a l v a r i a b l e - e n h a n c e d 朋认，i 。a f a ) ， 并把它作为朋r ”“公式动态检查器的验证引擎。l a f a 的状态数与咫l l ”“ 公式的大小保持线性，克服了在传统的基于n f a 或b a 方法中，因为状态空 间爆炸而产生的技术瓶颈。 3 用有向无环图表示l a f a 的运行路径。只有u n i v e r s a l 分支的成功同步才能使 u n i v e r s a l 分支选择达到接受状态。 4 用符号化的方法编码状态和局部变量。这种编码允许对状态和局部变量多重 赋值，每次赋值都表示l a f a 不同的运行路径。 5 开发了只i l o 帕v e r i l o g 动态验证器的原型，并给出了一系列完整的测试用例。 1 4 3 论文结构安捧 本文以后的内容是如下安排的： 在第二部分里我们完整的介绍了p s l 语言的语法和语义，并且给出了p s l 简单子集p s ”呻的定义。在这一部分中，我们探讨了p 疆”。公式在有限长字 符串上的组合定律，因此动态仿真器可以从p s f f 舭公式的子公式判定强满足或 强违背。 在第三部分，我们先考察了b f i e h i 自动机和交替式自动机a f a 。虽然交替式 自动机( a f a ) 在表示线性时态逻辑时具有线性空间复杂度，但是p s l 是带循环的 m 语言，a f a 也未能同步p s l 长度匹配语句的所有分支，所以本文提出了局部变 量增强的交替式自动机( l a f a ) ，解决分支同步和循环计数的问题。在第三部分 中我们还提出用符号化的方法编码状态和局部变量。该编码方式允许对状态和局 部变量多重赋值，状态的不同值代表l a f a 不同的执行结果。通过以上方法，我 基于断言的仿真算法与实现 们能够维持验证在时间和空间上的线性复杂度。 第四部分着重讨论了v e r i l o g 的仿真语义和仿真器的实现。我们扩展了开源 软件i e a m s v e r i l o g 和g t k w a v e ，并开发了交替式自动机生成工具a a m a k e l 。整 套工具可以解析p 蚪帅“语法，生成交替式自动机汇编代码，并在仿真时动态验 证性质的满足与违背，以图形化方式显示v e r i l o g 设计波形和憨r ”忡性质验证 结果。 本文在第五部分作了总结并提出了未来的研究方向和工作。 1s - 基于断言的仿真算法与实现 第2 章性质规范语言p s l a c c e l l e r a 在2 0 0 2 年启动统一的性质规范语言( p r o p e r t ys p e c i f i c a t i o n l a n g u a g e ，p s l l 的制定工作。2 0 0 5 年9 月，p s l 已正式成为i e e e - 1 8 5 0 标准 1 3 ， 2 1 。p s l 在兼具c t l 与l t l 两种时态逻辑的同时，在语言构造中引入了顺序扩 展正则表达式( s e q u e n t i a le x t e n d e dr e g u l a re x p r e s s i o n , s e r e ) 。这些新特性使p s l 成为灵活，精确和强大的规范语言。p s l 的简单子集腕o 是指满足单调时序 步进的p s l 语言子集，即在体现冈果关系的规范子句中，“原冈”的发生时间总是 出现在“结果”前，它对操作数的类型作了限制，较易被模拟仿真。 2 1p s l 的文法层次 p s l 从4 方面考察性质：布尔层，时态层、建模层和验证层。布尔层由布尔 表达式组成，时态层描述布尔表达式在时序上的关系，建模层描述建模系统输入 输出问复杂的关系，验证层描述了在验证时如何使用性质。 布尔层由设计模型中变量构成。例如，如果要表示。信号e n l 和信号e n 2 互 斥”，那么我们可以用以下的p s l 表示：! ( e n l e n 2 ) 。但是我们没有在布尔层说 明这两个信号在什么时候互斥，是在时刻0 ，还是在任意时刻。 时