任务流模型检验的研究

摘要：对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在，而是关心状态组合提供的功能是否存在及各状态组合之间是否存在指定的转换关系，从而避免了状态空间爆炸问题。模块搜索算法以模块为基础对任务流模型进行搜索来验证给定系统是否满足规范要求。

关键词：验证、模型检验、任务流模型

中图分类号：TN402文献标识码：A文章编号：1009-3044(2007)03-10795-03

1 引言

数字电路系统的规模仍然按摩尔定律呈指数增长，使得数字芯片的电路规模变得十分巨大，从而对验证方法和技术提出了极大的挑战。验证过程所耗费的时间一般占总设计周期的三分之二，甚至达到80%以上[1]。

目前采用的主要验证技术是模型检验技术。模型检验(Model Checking)技术是由Clarke等在1981年代提出的，实现了对于并发系统的自动验证问题[2]。模型检验是一种自动验证有穷状态系统的技术，基本思想是通过遍历系统模型的状态空间来检验系统模型是否满足给定的性质。模型检验技术不需要测试平台和测试向量，当发现错误时，将生成从初始状态变化到指定属性不成立状态的完整轨迹记录。但模型检验技术也有其局限性：如模型检验只适用于有限状态系统，当状态空间非常大时即使是有限的，也是不可实现的[3]。再如随着系统元器件数目的增多，任何系统的状态空间呈指数增长―状态爆炸问题[4]。

为了克服模型检验技术中的状态爆炸问题，出现了一系列经过改进的模型检验技术，如基于有序二叉决策树（OBDD）[5]的符号模型检验算法[6] OBDD方法只要选择合适的变量顺序就可大大减少状态数量，从而在一定程度上减轻了状态爆炸问题。再例如将可满足问题引入模型检验产生的有界模型检验技术[7]等。虽然这些技术在一定程度上解决了状态爆炸问题，但仍然适应不了日益发展的集成电路验证的要求，为此提出了任务流检验方法。

任务流检验方法从状态空间数目中脱离出来，只关注状态及状态组合间的转换关系，从而大大减少了搜索空间，提高了验证效率。模型检验技术的关键问题是如何设计数据结构和算法，来表示大规模系统模型的状态空间，本文采用了基于模块的搜索算法来表示系统模型的状态空间。

论文的第二部分介绍了任务的相关概念及任务任务流的描述方法；第三部分给出了基于模块的任务流模型检验算法；第四部分通过给出实例来证明任务模型检验的优越性，并得出结论。

2 任务流模型检验技术

传统的模型检验主要关心的是系统状态以及能否从一个指定的状态到达另一个指定的状态，这种方法随着状态数目的增多，已难以全面完成验证要求。为了解决这一难题，提出了只检验转换关系是否存在的任务流模型检验。

2.1 任务的相关概念

任务――对于并发系统，设有状态集合S和功能集合F，并且{sa}∈S，{sb}∈S。如果存在一个要求M，在满足约束条件V的情况下，能使一个或若干个功能形成功能组合{fk}∈F，则称M为一个任务，即 M?圳{fk}∈F，?坌（{sa}∈S，{sb}∈S）

由上可以看出，实现某一个任务是需要条件的，即任务只有在特定条件下才能存在。

任务转换―所谓任务转换，是指任务之间的转移。从数学上看，任务转移是一种运算，运算的形式由约束条件所决定。

任务流―多任务执行过程的表示，也叫做综合任务模型。把任务按要求级联起来，就构成了任务流，任务流反映了多个不同任务的执行结构和执行机制。

任务规范―是任务的算法描述。在任务模型检验中，规范由任务功能要求和约束条件构成。规范代表了完整的任务要求和约束条件并提供了推理方法。

2.2 任务流模型检验系统的算子

2.2.1基本功能算子

（1）SDetector：状态组合探测；

（2）SProcess：状态组合处理；

（3）STrans：状态组合转移；

2.2.2约束条件的基本算子

（1）Par并行方式：要求所影响的功能以并行方式工作；

（2）Ser串行方式：要求所影响的功能以串行方式工作；

（3）Syn同步：两个或多个功能或功能组合之间具有同步关系；

（4）Asyn异步：两个或多个功能或功能组合之间具有异步关系；

2.2.3 功能规范的描述规则

以FUNCTION表征各模块，其后紧跟功能组合、端口约束和其他约束说明。格式为：

FUNCTION 模块名

{ F (功能组合说明)；

IO (IO限制说明)；

Constraint (其他约束条件)； }

2.2.4 验证规范的描述规则

（1）任务流规范的描述

任务流规范的描述是以MISSIONFLOW作为关键字的，后跟该任务流的名称。Clock、Control和Data是标签，表示其后所跟的任务表达式构成了时钟、控制和数据任务流。

MISSIONFLOW 任务流名

{ Clock:任务表达式；

Control:任务表达式；

Data:任务表达式； }

（2）任务规范的描述

根据任务的定义，对一个任务的描述包括如下几个要素：任务名、功能和约束条件。任务名是任务流中每个任务的唯一标识符；功能为完成任务所需要的状态转移，即需要的功能算子；功能约束条件是完成功能所需要的约束条件。

MISSION 任务名

{ FM (功能组合说明)；

IOM (IO约束条件)；

CM (其他约束条件)； }

3 任务流模型检验算法

任务流模型检验用来验证所设计的系统是否能满足设计规范要求，即对系统的设计结果进行验证，任务流检验根据系统设计要求，从初始任务开始，按照任务流向，对系统结构进行检验，由于任务通过不同的功能模块来实现，因此采用模块搜索算法可以有效地验证系统。

根据任务与功能的关系以及任务和功能的定义，可以建立如下的搜索算法：

（1）输入电路框图（功能模块），翻译成功能计算树模型[8]；

（2）输入设计规范，并将规范中的任务及任务流转化为计算模型[9]；

（3）在任务计算模型中提取模块，并按数据流向与功能计算模型进行比较：

(a)先进行功能模块搜索：在任务中搜索模块，以“_”为标记，每当遇到“_”，后面的字符为模块名，找出某一任务所涉及到的所有模块，然后与设计中的功能模块比较。具体方法是：初始化时，假设此任务中所有模块的搜索标记均为0，然后按数据流向在设计的功能模块Mi，i=1,2,…,n中搜索，如果设计中存在此模块，则该模块的搜索标记变为1，如果任务中所涉及到的模块都为1，则停止搜索，说明此任务涉及到功能模块在设计中都存在；如果设计中的模块都搜索完毕后，任务中模块标记仍有为0的，则说明此模块在设计中不存在。

（b）在功能模块中进行基本功能算子搜索。在对某个功能模块的搜索中，首先设此模块中的所有功能算子的搜索标记均为0。然后与设计中相应模块的功能算子比较，如果设计中相应模块存在此功能算子，则该算子的搜索标记变为1。如果所有算子的搜索标记均为1，则停止搜索，说明设计模块中存在实现任务所必需的功能算子；如果模块搜索完毕后，仍有功能算子标记为0的，则说明设计模块中不存在此功能算子。

在基本功能算子搜索中，要检查功能模块中是否存在与任务描述中相同的算子，检查输入、输出、时钟和使能关系是否一致，如果一致，还要检查IO约束和其他约束是否一致。如果完全一致，则标记该模块的该功能算子能实现该任务中指定功能。

（4）完成任务的搜索之后，进行任务流检查，即检查相邻任务之间的连接关系是否正确。这些约束条件包括串行，并行，同步，异步。

当任务流中所有相邻任务的互连结构都满足要求，则该任务流能实现，也就是该任务流所描述的特定系统功能能实现。

4 任务流方法应用实例

图1为简化的8位CPU中算术运算逻辑单元alu的结构框图。此设计采用任务流模型进行检验。在对此设计进行任务流模型验证之前，必须清楚知道设计能够实现那些功能，某个任务是有哪些功能模块完成，以此建立任务流模型，写出任务设计规范。本实例根据alu的工作原理，把两数相加的功能用任务流加以描述：首先接收指令，并翻译为需要进行加法运算，接着接收两个数据（并行），再进行加法运算，存储，最后输出结果。具体的任务流程如图2所示。

要对此设计采用任务模型算法加以检验，必须从设计和验证规范两方面加以描述。设计方面采用功能描述，如下所示：

由描述知：描述了一个名为alu的功能模块，其中FUNCTION是编程使用的关键字，alu是该功能模块的名称。SDetectorPE是编程使用的关键字，说明在时钟上升沿时刻具有接收输入的功能，即在时钟clk上升沿和控制输入信号wa有效的情况下将来自data0信号线的数据写入到op1中。SProcessVPE说明在时钟上升沿时刻具有数值处理的能力，即在时钟clk上升沿和控制输入信号add有效的情况下将op1和op2中的数据相加并将结果存入register中。IN提供了该功能模块输入端数目，其中C wa=1表示有1条控制输入线，D data0=8表示data0是一条8位的数据输入总线，E op1=8表示op1是功能模块内部一个8位的数据接收单元。OUT提供了对该功能模块输出功能的约束条件。D datai=8表示datai是一条8位的数据输出总线。CK表示该模块具有一个控制时钟。Constraint语句为该功能模块的其他约束条件。Ser表示输入数据和输出数据不能同时进行，以串行方式工作。alu具有输入锁存相加功能的模块，以串行模式工作。

采用相同的描述方式对寄存单元reg和控制单元ctl进行描述，如下所示：

―STransPE说明在时钟上升沿具有输出锁存的功能，即在时钟clk上升沿和w1和r1有效的情况下将内部模块中的数据送到信号线data0中。

此功能模块reg在时钟上升沿clk及控制输入信号有效的条件下将输入数据分别锁存到src1和src2中，运算结束后运算结果从锁存模块dest输出。

由Constraint可知，对内部模块src1和src2的读操作和写操作不能同时进行，同一模块的读写操作也不能同时进行。reg具有输入输出锁存的功能。

FUNCTIONctl

―SProcessLPE说明在时钟上升沿具有逻辑处理的能力，即在时钟信号的上升沿将操作指令进行并行逻辑运算，即将操作指令翻译成各种控制信号。

IO{IN:C instr=8 ; ―8位输入控制线，即操作指令是8位的。

Constrain{Syn(wa,wb,wc,wd,add);};―由操作指令翻译成的各种控制信号以同步方式运行。}

ctl单元主要是对各种控制信号进行描述。

采用上述方法实现了对设计功能的描述，由描述可知CPU的功能，功能的实现条件，输入输出位数和类型以及运行方式。

验证方面采用任务流及任务规范描述，根据图2写出的任务流描述规范：

由描述可知：描述了一个名为alu的任务流，其中MISSION FLOW是编程使用的关键字，alu是任务流的名称。Clock后面的任务表达式构成了时钟任务流。Syn (IR; SendA,;SendB; Add; Reg;Outreg;Read)说明了各个任务是以同步方式工作的。Control说明其后的任务表达式是控制信息。Data说明其后的任务表达式是数据信息。SendA,SendB在同一行并以” ,”分开，说明送数A和送数B是并行执行的。Add实现加法的任务，与SendA,SendB不在同一行说明SendA,SendB与Add是顺序执行的，只有在并行执行完送数A和数B的任务之后才能执行两数相加的任务。

具体任务描述如下：

上面描述了一个名为IR的任务，其中MISSION是关键字，IR是任务的名称。其中FM说明完成任务所需要的功能算子，功能算子含义与功能描述中的相同；IOM是完成任务输入输出口的限制条件；CM是完成任务其他的限制条件。IR是一个将输入指令翻译成控制信息的任务。

SendA描述的任务是先将输入数据送到锁存器src1中，然后在控制输入信号wa有效的情况下将数据送入到op1中为做加法运算做好准备。

SendB与SendA描述相似。

Add描述的任务是在时钟上升沿和控制输入信号add有效的情况下，将事先存入到op1和op2中的数据做加法运算并将结果存入到registeter中。

Reg描述的任务是将加法运算后的输出结果送到输出信号线datai上。

OutREG描述的任务是将输出信号线datai上的数据锁存到dest中。

Read任务是将最终结果从data线上输出。

采用上述方法实现了对任务的描述，通过对任务规范的描述可容易地看出任务的实现过程。

按照前文所述任务检验流程，在[10]的验证界面的基础上，采用模块搜索算法所得验证结果如图3所示：

此例采用上述的功能算子方法加以描述，用模块搜索的方法来搜索任务流模型，实现了对8bitCUP的验证。

通过实验发现，传统的模型检验方法需要搜索8位CPU所有可能的状态空间，在时钟信号（clk）和控制信号（wa,wb,wc,add）都已有效的情况下，只进行8位加法运算，需要搜索的状态空间就已达65536个，而采用任务流模型检验技术，对此加法运算进行模型检验，只需验证在约束条件下，加法的转换关系是否存在以及对输入输出口的位数及类型进行检验即可，从而大大减少了搜索时间，提高了验证效率。

5. 结论

本文采用的模块搜索算法，可以很好地实现对系统结构的验证，并可以减少搜索时间为模型检验技术的进一步发展，解决状态爆炸问题提供了一种有力的方法，但由于此种方法处于研究的初期，还存在许多待完善地地方。

参考文献：

[1]吴为民，数字系统的形式化验证[N]，计算机世界报 2005年第37期B11,B12

[2]E.Clarke and E .E merson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic[J].In Proceedings of the Workshop on Logic of Programs. LNCS ,vol.131,pp .52-71.Springer-Verlag,1981.

[3]Tatsuhiro Tsuchiya, Shin'ichi Nagano, Rohayu Bt Paidi, Tohru Kikuno.Symbolic Model Checking for Self-Stabilizing Algorithms[J].IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, VOL. 12, NO. 1, JANUARY 2001.

[4]Ilya Romanovsky.Model-Checking Real-Time Concurrent Systems[J]. 18 Sep 2001.

[5]R.E.Bryant. Graph-based algorithms for Boolean function manipulation[J]. IEEE Transactions on Computers,C-35(8),1986.

[6]Olivier Coudert,Christian Berthet,and Jean Christophe Madre. Verification of synchronous sequential machines based on symbolic execution[J]. Automatic Verification Methods for Finite State System,1995.

[7] A.Biere, et al. Bounded Model Checking[J]. Vol.58 of Advances in Computers.

[8]杜慧、李哲英、骆丽，MCTL系统中建立任务流集合的研究[J]，北方工业大学学报，2004 Vol.16 No.1.

[9]骆丽，数字硬件设计的形式验证理论及应用研究[D].博士论文.

[10]杜慧 SoC设计中的验证方法研究[D].硕士论文.

本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文。