《PSL逻辑及验证技术研究进展与展望.doc》由会员分享，可在线阅读，更多相关《PSL逻辑及验证技术研究进展与展望.doc（19页珍藏版）》请在三一文库上搜索。
1、PSL逻辑及验证技术研究进展与展望doi:10.3969/j.issn.1001-3695.2010.07.004 PSL logic and its verification technologies YU Lei1,2,ZHAO Zong-tao2 (1.School of Computer, National University of Defense Technology, Changsha 410073, China;2.Dept. of Computer Science, Second Artillery Engineering College, Xian 710025, Chin
2、a) Abstract:After the descriptions of the PSL hierarchical structure and its syntax & semantics, this paper reviewed in detail the recent PSL verification application technologies and finally pointed out some issues to be further studied. Key words:PSL(property specification language); ABV(assertion
3、 based verification); formal verification; run-time verification 不同时序逻辑就语法、语义、表达能力和相应验证问题的复杂度四方面都有较大的区别。应用于规约的不同时序逻辑的不兼容性加剧了不同工具之间数据转换的复杂程度。工业领域对验证问题不断增长的研究兴趣,导致了人们对实现规约逻辑标准化目标的更多努力。其中,由Accellera组织提出并于2005年确定为IEEE工业标准的PSL就是一种重要的应用于硬件验证的标准化属性规约语言。PSL主要有三大用途:形式化验证、动态验证仿真和功能规约描述(作为功能规约文档)。由于PSL易于读写、语法精
4、简、语义清晰、表达能力强,能直接使用于高效的模拟和形式化验证算法,它作为一种功能描述语言得到了广泛的应用。 1 PSL的分层结构及语法与语义 1.1 PSL的分层结构 PSL是一种分层语言,包括四层(图1):a)布尔层(boolean layer),用于构造实现单个状态内评估的布尔表达式,是构筑时序表达式的基础;b)时序层(temporal layer),是语言的核心层,用于实现语言的主要功能,即描述设计模块的多个状态的时序属性;c)验证层(verification layer),是与验证工具紧密结合的语言层,用于指示验证工具验证时序层所描述的模型属性规约;d)建模层(modeling lay
5、er),为验证 过程所需的测试输入模块或辅助硬件模块建模。验证层的主要验证指示词以及建模层的内建函数和建模指示词的功能和定义见文献1。图2用PSL表达的验证实例体现了PSL的分层结构。其中,assert是验证层的验证指示词,用于指示验证工具验证时序层always(reqnext(ack)时序属性;assign是建模层的赋值指示词,为定义的输入变量req赋值。 作为PSL核心的时序层可分为FL(foundation language,基础语言)和OBE(optional branching extension,可选分支扩展)两部分。FL如同LTL,是线性时序逻辑,而OBE就是分支时序逻辑CTL(
6、computation tree logic)2。时序层的FL包含命题操作子、LTL操作子、定义时间粒度的时钟操作子、连续扩展正规表达式(sequential extended regular expressions,SEREs)以及abort操作子。FL公式还具有时钟声明的功能表示,具有时钟声明的公式很容易改写成非时钟公式(改写规则见文献1)。 1.2 PSL的语法与语义1 1.2.1 PSL语法 定义1 连续扩展正规表达式(sequential extended regular expression,SERE)。每个布尔表达式b是一个SERE;如果r、r1、r2是SEREs,则以下各项都是
7、SERE: •r •r1;r2 •r1:r2 •r1|r2 •r1&r2 •*0 •r* 定义2 基础语言公式(foundation language formulas,FL formulas)。如果b是布尔表达式,则b和b!都是FL公式;如果和是FL公式,r是SERE,b是布尔表达式,则以下各项都是FL公式: •() • • •r! •r •X! •• abort b•r| 定义3 可选分支扩展公式(o
8、ptional branching extension formulas,OBE formulas)。每个布尔表达式是一个OBE公式;如果f、 f1、 f2是OBE公式,则以下各项都是OBE公式: •(f) •EXf •f •Ef1f2 •f1f2 •EG f 定义4 Accellera PSL公式。每个FL公式都是一个Accellera PSL公式;每个OBE公式都是一个Accellera PSL公式。 1.2.2 PSL的语义 1)非时钟SEREs语义 wr表示w紧满足(tightly satisfies)r。其中,w
9、是定义在=2p,上的有穷字,表示满足任意命题公式的状态,表示不满足任意命题公式的状态。原子命题pAP,b为布尔表达式,r、r1、r2是非时钟SEREs,则: (1)wrwr (2)wb|w|=1且w0b (3)wr1;r2?讵?w1,w2,s.t.w=w1w2,w1r1且w2r2 (4)wr1:r2?讵?w1,w2,l,s.t.w=w1lw2,w1lr1且lw2r2 (5)wr1|r2wr1或wr2 (6)w*0w= (7)wr1&r2wr1且wr2 (8)wr*w*0或 w1,w2,s.t.w1,w=w1w2,w1r且w2r* 2)非时钟FL公式语义 式w?b表示w满足。其中,w是一个有穷或
10、无穷字,b是布尔表达式,r是非时钟SERE,和是非时钟FL公式,则 (1)w?b() w?b (2)w?b?讴?w?b (3)w?bw?b且w?b (4)w?bb!|w|0且w0b (5)w?bb|w|=0或w0b (6)w?br!?讵?j1且w1.?b (9)w?b?讵?k 2.2.1 PSL与定理证明 定理证明是在验证者的引导下,以形式逻辑的公理和推理规则为基础,不断对公理和已证明的定理施加推理规则,产生新的定理,直至推导出需要的定理的过程。文献18介绍了已开发的使用设计断言的半自动定理证明的验证系统PROVERIFIC,构建了一种统一建模框架UFM将命题逻辑形式化地对应设计及其断言,定义
11、了能捕捉PSL断言语义和Verilog表示的UFM语法子集的一般谓词模板。在验证过程中,PROVERIFIC使用这些模板自动地提取一个设计(Verilog表示)的形式化模型以及其属性(PSL表示),并将它们转换成PVS定理证明器的更高阶逻辑,PVS能进一步验证属性的正确性。 高阶逻辑(higher order logic)是在一阶命题演算逻辑基础上扩展形成的,已开发的HOL定理证明器支持高阶逻辑的定理证明。文献19详细给出了与PSL每个操作算子相关的HOL系统的表示形式,即给出了如何将PSL嵌入HOL系统的过程。PSL嵌入HOL的目的在于:a)调试和证明元定理;b)获得机器可处理的语义,高阶逻
12、辑广泛地应用在各种形式化工具中,一旦具有高阶逻辑的表示形式就能容易地转换为其他工具可执行的表达;c)结合了定理证明和检验功能,PSL和高阶逻辑结合后具有更强的表达能力,此时的定理证明器可以实现执行、检验和定理证明的功能。在此基础上,文献20说明了HOL定理证明器是验证PSL语义合法性的强有力工具。文献21研究了如何利用HOL定理证明器元语言ML编码证明脚本执行PSL形式化语义的方法。HOL系统提供了一个ML函数Eval用于证明定理t=t。其中t是项t的评估结果,Eval可以调用显示地添加在上下文中的等式和决策断言。若考虑执行带时钟的PSL形式语义则首先需要执行时钟删除重写规则,而后再用Eval
13、函数评估非时钟PSL语义。 2.2.2 PSL的模型检验实现 模型检验是通过遍历系统所有状态空间,对有穷状态系统进行自动验证,确定系统模型是否具有某种性质,并自动构造不满足验证性质的反例的技术。Tuerk等人22给出了利用HOL的定理证明器和模型检验器SMV实现PSL的模型检验的算法,利用改进的正确性转换定理构筑建立在标准的PSL形式化语义基础上的PSL执行结构。应用方面,此执行结构借助IBM的RuleBase CTL模型检验器,实现了一种能检验PSL执行正确性的工具,可以检测执行时钟abort操作子下的bug。文献22方法的优势在于可以处理时钟PSL公式,前提是将时钟视为“语法糖衣”并进一步
14、使用重写规则删除时钟操作子;不足在于只适用于PSL的子集,特别是还未扩展到PSL的正规表达式部分,因此只能处理一类特殊的PSL问题。 Pnueli等人23借助公平离散系统(JDS)构建测试器实现了PSL的模型检验。用JDS分别构建系统计算模型D和待验证属性的测试器T。构造T的计算复杂度为O(2n),n为PSL的公式长度;当SERE限定在三种操作子:连接(;)、交叠连接(:)和闭包(*)集合时,T的变量个数与长度呈线性关系。由于测试器能用符号表达,可以方便地应用在符号化模型检验中。模型检验过程采用传统的自动机理论方法:a)对D和T执行同步并发组合计算D|T,即结果的初始状态和结束条件为相应断言的
15、合取形式,结果的迁移关系为系统D和测试器T迁移关系的合取式;b)检验D|T是否有公平计算路径,若存在,则D不满足属性。此方法构造的测试器不同于自动机,具有高度的组合性,这对充分利用PSL的上下文起到了独到的作用。 文献24提出了PSL的有界模型检验方法及其算法框架。首先,定义PSL逻辑的有界语义,而后将有界语义进一步简化为SAT(可满足性问题),分别将PSL性质规约公式、系统M的状态迁移关系转换为命题公式Mk和M,sk,最后验证命题公式M,skMk的可满足性,这样就将时序逻辑PSL的存在模型检验转换为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行?程。 2.2.3 软件的
16、模型检验 随着硬件形式化验证技术的不断成熟,开发软件的形式化验证技术也提上了议事日程。RuleBase是由IBM Haifa研究实验室开发的一种应用PSL实现形式化验证的工具。IBM Haifa研究实验室在RuleBase的基础上开发了一种用于跟踪并发C程序bug的模型检验器Wolf4,Wolf能自动产生模型和规约,在采用BDD(二进制决策图)的符号化方法基础上显式地完成软件模型检验。Wolf主要包括三个组成部分:C-to-model转换器、集成于RuleBasePE的软件验证算法以及用于显示bug路径的GUI-vet。其中,C-to-model转换器接收并发C程序并将其转换为有穷模型,产生“
17、hints”和“guides”以引导软件模型检验器发现bug。软件模行检验器主要采用偏序析取分割的符号化BDD算法实现软件验证以及采用动态BDD重排序算法缩减BDD重排序时间,并且采用偏序精简技术枝剪遍历的分支。Wolf能处理指针的删除和资源的动态分配等工作,但其不足是很难处理由非确定输入带来的非确定行为。 文献5在借助c2edl工具的基础上将ANSI-C代码转换为RuleBase的输入语言EDL,提出使用RuleBase实现C描述程序的碎片收集机制的模型检验方法。RuleBase的核心SMV使用BDD作为其基本数据结构。若一个将来使用的BDD收集在碎片堆中,则结果是一个悬摆参考,也即此BDD
18、潜在地包含在碎片集中;若一个将来不使用的BDD仍不删除,则结果导致内存泄漏。论文分别应用表达悬摆参考和内存泄漏的PSL公式实现SMV碎片收集机制的模型检验。文献5的软件模型检验方法具有的特点是:a)通过自动产生抽象模型的方式,将模型检验方法直接应用于源代码;b)c2edl的使用无须人工干预,即实现是完全自动的且为RuleBase创建了有穷状态模型;c)只检验时序逻辑表达的属性,对时序逻辑的嵌套层次给予了人工限制。 文献6使用RuleBase模型检验器建模和形式化验证一个软件高速缓存器的算法,其建模过程采用由C代码直接产生的超详细度模型,从而取代先前使用高级抽象模型的方式。超详细模型建立了真实软
19、件结构与实现代码之间的一一对应关系。与文献5的抽象模型比较,其优势在于详细建模算法比抽象级建模算法更加简便;其次它排除了建立抽象模型遇到的一些问题,如虚假否定、虚假肯定等。最后,一些研究如文献25均实现了超详细模型的成功应用,这都可以作为上述软件模型检验的借鉴方法。 2.2.4 与形式化验证相关的技术 1)PSL构造自动机技术 自动机是许多形式化规约、验证方法的基础模型,是一种可用于模型检验等验证技术的验证形式,在验证技术领域中有着广泛的应用。Bustan等人26将PSL的核心逻辑定义为LTL_WR,即在LTL的基础上再定义正规表达式REs,并且证明每个LTL_WR公式f都存在一个非确定的Bc
20、hi自动机(NBA),复杂度是f的双指数。在表达时序逻辑方面,交换自动机(AFA)比非确定自动机(NFA)复杂度呈指数形式精简。因此为构造NFA,Bustan等人先构造LTL_WR的AFA。但是,由于交换自动机只能产生每个分支都可接受的运行,而事实上,运行遍历的状态既包括可接受也包括不可接受。基于这种情况,文献26进一步将AFA转换为NFA。文献27介绍了将PSL转换为非确定Bchi自动机的传统方法:将PSL中的SEREs首先转换为最小NFA,而后NFA组织在一起,将PSL公式转变为交换Bchi自动机ABA,最后使用Miyano-Hayashi(MH)方法28将ABA转换为NBA。文献29指出
21、这种方法就是基于SAT的有界模型检验,前提是弱交换自动机;文献30提出一种基于MH,由PSL属性构造ABA而后转换为对应的NBA的符号化编码方法。文献29,30提出的两种方法都试图限制编码大小,但它们都依赖一个旨在最小化ABA并执行优化方法的库,ABA最小化代价高,即便是对于中等长度的PSL规约,这两种方法都不能在可接收时间内完成转换任务。文献31提出将PSL转换为符号化表示的NBA的直接编码,主要基于SONF(suffix operator normal form,后缀操作符范式),实验表明SONF结构是一种快速构造NBA的有效方法。文献32给出了将PSL的一个包含安全属性的子集safety
22、PSLdet直接转换为co-universal自动机的方法。由于有穷自动机能发现违反安全属性的反例,此时的模型检验可简化成不变式“自动机A不处于接收状态”的验证过程。不变式检验不但简单,而且许多模拟工具在不变式中会执行得更好;缺点是虽然safetyPSLdet的大部分操作子都能建立相应的非确定CUA,但弱正规表达式r建立的自动机必须先确定化,这样明显地增加了构建自动机的复杂性。 2)模型检验的简化设计技术 模型检验为验证逻辑设计是否满足指定属性提供了一种有效的途径。模型检验器穷尽地检验所有可能的输入序列,或穷尽遍历和搜索所有的可达设计状态。为更有效地执行上述过程,人们常借助一些简化手段将设计转
23、换为逻辑上等价的另一简易设计,这种简化后的设计更方便穷尽开发。文献33提出两种简化方法,即重定时简化和量词简化,并讨论了各种实现问题,检验了这两种方法的有效性。实验证明,量词简化方法在缩减模型检验时间的情况下显示了突出优势,但其自身的执行过程却相当费时;而重定时简化方法只针对部分问题?行? 3)综合技术 综合是指从指定规约中自动产生设计,同时形式化地验证规约的可实现性并获取实现证据的处理技术。文献34描述了基于PSL属性的综合技术,在给定PSL线性时间片断表达的规约的前提下,此技术自动综合生成硬件设计,主要包括三种不同的方法:a)非确定方法,是一种基于PSL模型检验时采用的自动机的方法,此方法
24、只能综合PSL的一个子集,但是综合效率很高;不足在于适用面较窄,最适用于部分执行实现系统的综合问题。在合理的消耗下,部分执行实现系统能有效地修补失效系统。b)广义反应规约综合方法,适用于综合更丰富类型的规约,特别是能更精确地综合在使用广义反应接受条件下表达的属性规约。其思想是:将规约转换成能应用三层嵌套的不动点算法的特殊形式,实验证明,在综合大规模规约集合时,其实现复杂度也是可接受的。c)完全方法,应用于采用PSL完整线性时间片断的情形,其实现复杂度为双指数时间。上述三种综合方法优势互补,它们能以不同的计算复杂度综合PSL不同子集表达的属性规约。PSL片断涵盖越全面则综合的代价越高,因此在采用
25、综合方法时特别要考虑表达能力与代价之间的折中问题。 电路设计的综合处理方法不需要手写代码,使从规约中快速构造原型系统成为可能。文献35应用自动高层综合方法直接产生PSL描述的规约的结构修正(correct by construction)门级实现。首先对PSL属性执行综合处理,此时将PSL公式的实现问题简化为介于系统与环境之间的2选手无穷博弈问题;而后构造系统变量和环境变量的BDD结构;最后给出了将BDD转换为硬件电路的算法。该方法的优势在于可以获得设计PSL规约的一致性和完整性,并且自动综合方法最适用于产生控制电路,未来可考虑将手动编码的数据路径与自动综合产生的控制电路结合的问题;不足在于产
26、生的门级输出较为复杂且不易手动修正,有些电路的规约不能直接描述,并且常常伴随着一个递归处理的过程。文献36提出了基于自动机的PSL属性断言验证器的综合方法。 2.3 软件的运行时验证 最近几年,嵌入式系统的设计复杂度越来越高,随之带来的验证问题也越困难,在此基础上,人们寻求软件在更高抽象层次上验证规约的方法。文献7给出一种将PSL绑定到C语言上的过程,实现了一个对程序PSL逻辑属性执行运行时验证的工具。具体算法如下: 1)数据模型的建立 输入:sPSL源文件、C源文件以及C源文件的调试信息。 输出:数据模型至评估引擎。 a)用一个脚本处理sPSL源文件,为每个属性创建一个标记条目; b)为C源
27、文件的每个变量和函数建立标签; c)编译C源文件,产生详细的调试信息; d)通过编译工具如OBJDUMP将c)的调试信息抽取到一个文本文件中。 2)数据信息的评估 输入:步骤1)输出的数据模型以及地址信息、寄存器分配、存储器容量信息。 输出:true或false或undefined。 a)实时系统通知Giano模拟器有关C源程序的名字及地址信息; b)评估引擎依据程序名搜索相应的数据模型文件,作语法分析且创建相应的PTree; c)若一个指定属性满足活性(liveness),则评估引擎创建并初始化属性的一棵评估树ETree(evaluation tree),监控功能开始启动。 其中步骤2)中c
28、)的evaluation tree通过深度优先和左子树优先的方式实现遍历,每个分支至多带两片叶子,叶子可以是操作算子或变量数值。评估的结果为一个三值逻辑,即true(T),false(F)和undefined(Z)。例如评估一个属性always(a=1 next b=1)until(c=1),其对应的评估树如图3所示。节点a=1是逻辑树的首节点,在下一事件未能判断操作算子next是否满足时,逻辑树返回Z;当b=1满足时,next操作子返回T,否则返回F;一旦until操作算子接收到左子数返回的T值时,它就开始监控右子树表示的释放节点(release point),即c=1;在c=1未满足时,逻
29、辑树返回Z,一旦c=1和a=1 next b=1同时满足时,until操作子向父节点always返回T。此方法的优点是:a)在验证过程中无须改动执行程序和代码,增强了验证处理的可信度;b)原型系统结果产生功能调用和变量变化的执行路径,这对程序员理解程序错误行为的发生原因是大有裨益的;c)工具同时支持实时规约,可应用于性能验证之中;d)sPSL语言和评估引擎不依赖于使用的特定语言,它们可应用于堆栈寄存器结果执行的任何块结构语言中。不足是当前的原型系统不支持SEREs。 3 结束语 PSL是由EDA界的标准化组织Accellera提出,并于2005年确定为IEEE工业标准(IEEE-1850)的用
30、于描述并发系统的属性规约语言。本文在简要介绍PSL的语法、语义和分层结构基础上,综述了PSL的验证技术的研究现状及各种技术、方法的优缺点,今后有待进一步研究和改进的工作包括: a)基于断言的验证技术。PSL的ABV技术把传统的设计处理从具有粗糙的功能规约文档的非形式化RTL编码方式推向了更高层面的处理过程:对设计决策、设计属性和设计假设进行功能规约描述;在模拟过程中简化功能覆盖率分析以检验边角情况;简化用于验证结果正确性的测试平台参考模型的设计等。(a)为方便执行基于ABV的模拟技术,以往的文献常采用PSL的简单子集sPSL描述待验证的断言的方法,这势必影响了对复杂设计行为的表达能力,今后考虑
31、将正规表达式等逻辑描述扩充到ABV技术中,不断拓展ABV技术的应用范围;(b)将设计故障诊断技术和调试技术集成到ABV技术中;(c)对ABV的PSL断言施加一些重写规则,使用定理证明器如HOL或PVS形式化地证明规则的正确性;(d)考虑将动态验证与形式化验证结合的混合验证方法实现ABV技术,也是今后可以尝试研究的方向。 b)软件的模型检验技术。应用PSL的软件模型检验技术的研究目前尚处于研究的初级阶段,已有的一些文献46都只是实现解决针对特定问题的PSL的软件模型检验方法,基本上都借助了IBM的RuleBase工具。今后需要考虑拓展的内容包括:(a)重点研究如何将PSL的软件模型检验技术应用于
32、更一般的实际问题,改进工具的算法,使其对更一般的问题提供技术支持;(b)软件的模型检验的一个重要问题是内存容量,如何应用如无限状态技术37解决限定堆栈长度的问题将是一个亟待研究的方向;(c)“影响锥”简化方法是一种针对硬件设计的有效简化方法,针对软件设计的特点,需要开发一种专门适用于软件的简化技术,其中需要结合程序切片和静态分析技术;(d)实现对复杂数据类型如结构、指针和联合的自动编码技术;(e)研究直接支持软件的路径产生技术,RuleBase的图形化路径显示技术源于硬件设计,对于软件,提供给用户一个类似于图形化调式器的窗口更有意义,以支持单步前进和后退,同时自动产生readme文件帮助实现路
33、径的自动解释。 c)PSL构造自动机。符号化模型验证技术在硬件设计中显示了极其高效的验证能力,为进行模型检验,PSL公式需要转换为一种可验证形式,通常是自动机。从目前已有的文献26,27,31,32,PSL的模型检验的研究成果主要是采用自动机理论,通过构造PSL的自动机来实现自动验证。今后的研究主要关注于:(a)完成PSL自动机的构造后,通常会采用符号化模型检验算法,因此可以充分利用自动机结构信息定义一种较好的BDD变量排序形式,以提高模型检验算法的效率;(b)考虑将活性简化为安全性检验的应用技术,以产生更短的反例路径,特别是在实现公平环路检测时将显示应用价值;(c)使用一些简化技术如双向模拟
34、最小化技术以产生等价的规模更小的自动机,缩小搜索?占洹? d)程序的运行时验证技术。基于程序的时序逻辑PSL的安全关键性质运行时,验证需要依据通过监控器收集的程序整个运行过程的信息,以此来验证是否满足时序性质的要求,但可能占用资源多。基于此原因,拟采取以下措施:(a)考虑研究如何把PSL时序逻辑公式表示的性质分解为与其等价的一组断言,插装到程序的适当位置,根据断言的违反情况即可判断出性质的满足情况;(b)运行时验证既要考虑可终止的程序也要考虑类似反应式系统这样的非终止程序,此时在任何时刻只能获得当前执行的一个有穷状态前缀,需要对时序逻辑的语义进行适当的修改,变为针对有穷路径,同时与基于无穷路径
35、的时序逻辑公式语义相一致;(c)根据修改后的语义生成接收有穷序列的自动机(验证器),该自动机接收当前执行的有穷前缀,输出相应的验证结果,使得在存在软件缺陷的情况下尽可能早地检测到该缺陷。在基于当前信息能够验证给定性质规约时,及早终止对程序的进一步?觳狻? e)PSL的模型检验和可满足性问题的计算复杂度。PSL的重要应用是对并行系统进行形式化验证,模型检验是其中的技术之一;同时,理论上也已证明许多难解的问题都可从多项式变换为可满足性问题。可满足性问题是研究时序逻辑的核心问题之一,并已成为程序验证的一种有力工具。基于这两方面的考虑,研究时序逻辑PSL的模型检验和可满足性问题的计算复杂度将是今后PSL理论和实际应用研究的方向,这为解决相关问题提供了难度的标准,且对正确评价解决该类问题的各种算法的效率、进而确定对已有算法的改进余地具有重要的指导意义。文献38研究的对象局限于PSL线性时间逻辑各片断的计算复杂度,这不适应实际复杂应用问题属性的逻辑表示,今后需要进一步研究PSL所有操作符表达的逻辑公式的上述两类问题的复杂度,特别是需要研究如何将这些复杂度理论真正引导到解决实际问题的过程中,这是引导PSL研究从理论转向实践的一条途径。