一种基于System C语言的模型检测方法*

吴丽佳，于 琼，靳庆庚

(广西民族大学 广西混杂计算与集成电路设计分析重点实验室，广西 南宁 530006)



一种基于System C语言的模型检测方法*

吴丽佳，于 琼，靳庆庚

(广西民族大学 广西混杂计算与集成电路设计分析重点实验室，广西 南宁 530006)

System C语言在软硬件协同设计过程中被广泛用来建模和仿真.笔者提出了一种验证System C设计的方法，即通过把System C设计映射成为一个具有良好定义语义的UPPAAL时间自动机.System C设计的结构和非正式定义的行为在形成的UPPAAL时间自动机中得到了完整的保留.产生的UPPAAL模型允许使用UPPAAL模型检查器和其配套工具来进行验证.模型检查器用来验证设计的一些重要属性，比如活性，死锁问题和时间约束属性.通过对两个实例的活性、安全性和时间属性的验证来证明该方法的适用性.

System C；时间自动机；模型检测

1 System C语言介绍

System C[1-3]语言是一种系统级的硬件描述语言，它继承和扩展了C++，这使得它可以建模不同抽象级别的包括软件和硬件的复杂电子系统，它既可以描述纯功能模型和系统体系结构，也可以描述软硬件的具体实现，但核心是进行电子系统级设计、建模和验证[2].System C具有所有硬件描述语言所共有的基本特征，包括模块、进程、端口和信号等.

一个System C设计的仿真语义可以总结为以下几个步骤：1)初始化：每个进程被执行一次；2)求值：所有待执行的进程以顺序被执行；3)更新：原始通道被更新；4)如果有△延迟通知，则相应的进程被触发并重复步骤2)和3)；5)如果有定时时间通知则仿真时间被推进到响应的定时通知并且重复步骤2)～4)；6)如果没有定时事件通知则仿真结束.

2 UPPAAL时间自动机介绍

时间自动机，就是在传统有限状态机的基础上增加了时间约束的概念[6],通过用于时钟约束来建模时间依赖行为的时钟变量来阐述时间的概念.系统包含多个并发进程，这些并发进程由多个时间自动机来建模，然后通过交叉语义被执行并且在通道上保持同步.UPPAAL[4-5]是一系列工具的结合，包含仿真，动态演示和对多个时间自动机所构成的网络结构模型的验证.UPPAAL模型检查器能够对时间属性包括活性和安全性进行验证.模拟器可用于可视化模型检查器产生的反例.

3 转化设计

在本章中描述了我们是如何把System C语言元素转化为时间自动机以及如何把这些映射嵌入完整的设计的转化中去的，这种转化保留了System C设计的行为语义和给定的System C设计的结构.该方法要求两个微小的限制，第一，不能处理动态进程或者对象的创建，这不会使方法的适用性变得狭窄.第二，UPPAAL只支持有界整型变量.

3.1 方法转化

可执行的System C代码是完全包含在方法内的，每一个方法被转化为一个独立的时间自动机模型，为了建模调用-返回语句的语义，运用一个同步通道m_ctrl，如图1所示.给出的两个自动机表达了传统的调用-返回语义，左边的调用者用信号m_ctrl!来手动控制被调用者，等待被调用者的方法主体被执行，然后在接收到m_ctrl?时继续执行下一步.图1展示了一个参数m_param和一个返回值m_result是如何被传入给方法的.

图1 方法转化

方法主体是一系列的声明的集合，例如return，arithmetic，if-else，while，continue，break和method call.对于每一个声明我们都附加了转化和位置.接下来，在转化的每一步用术语 current location来参考最后的附加的位置.我们也保留着初始位置的引用，如果到达一个返回状态，会把当前状态和初始状态连接起来并且把这个转化标记为m_ctrl!,并且赋值给返回值,如图1所示.返回状态会终止当前块的转化，并且随后的代码不会被执行.在自动机模型中采用算术表达式作为更新的条件，因此把当前位置定为紧急位置并添加了算术语句作为转换条件，当达到这个条件时执行更新操作并转移到下一个位置.为了转化if-else语句增加额外两条边，如图2所示，其中一条边用if条件来标记，另外一条边用if的否定条件来标记.我们把当前位置定位紧急位置是因为if条件的判断不需要时间.把if语句块添加到if位置上，并且把else语句块添加到else位置上.如果其他的分支没有其他的返回语句，则转移到新的当前位置.如果其他分支有返回语句，使用其他分支的最后节点作为新的当前位置.如果所有分支都有返回语句则当前块的转化终止.对while循环的建模和if-else语句类似，如图2所示；循环体的语句被附加在满足while条件的位置上，对于返回语句，当前位置和初始位置连接起来，对于continue语句附加在while_begin位置上，break语句附加在while_end位置上.

图2 if-else和while循环转化

3.2 调度机

System C 设计的执行是由调度机来控制的.进程是最基本的执行单元，调度机的执行基于△周期，一个△周期包含求值和更新两个阶段.一个求值和更新循环构成了一个△周期.在求值阶段，处于就绪状态的进程按随机顺序执行，在更新阶段，原始通道通过获得新的值来更新.

用来建模调度机的时间自动机模型如图3所示.UPPAAL暗含了初始化操作，在主要仿真循环前，进程和方法都执行一次.我们也可以处理非初始化情况，但是这遗漏了空间限制的情况.调度机开始求值阶段时，通过evaluate位置来刻画求值阶段，如果有处于就绪状态的进程，则调度机会发送一个激活事件activate!，处于就绪状态的进程收到激活事件时开始执行.为了保证一次只有一个进程被执行，我们采用了二进制通道来激活.为了保证调度机一次只发送一个激活事件给就绪状态的进程，我们创建了一个计数器ready_procs来控制数量，当被触发时则计数器增加1，当挂起的时候则减1，当进程被执行完的时候则计数器ready_procs==0；当调度机到达update位置时则开始更新阶段，在更新阶段，更新请求通过接受激活事件update_start来随机执行.在更新阶段，立即通知是不被允许的，如果没有更多的更新请求，则调度机进入下一个△周期，也就是下一个位置next_ delta.当结束更新阶段时，调度机会发送一个delta_delay!事件来通知△延迟通知一个△周期已经结束.如果有△延迟通知，则相应的进程立即被触发进入就绪状态，他们将会在下一个△周期执行；如果没有触发任何进程，则ready_procs==0,仿真时间向前推进到最早的定时通知.在System C语言中有两种定时通知：一种是函数e.notify(t)，另一种是wait(t).在System C语言中，定时行为完全由调度机控制，在时间自动机模型中，可能在本地等待一个给定的时间，因此，对包含时间的进程和事件进行建模更合适.在调度机中等待最早待定定时通知的一种简单方法就是在有延迟时让含有定时行为的进程和事件发送一个同步广播信号advance_time!.调度机接收到advance_time?信号然后开始一个新的△周期，即通过定时通知来执行进入就绪状态的进程.

调度机的时间自动机模型和System C中的调度机表现完全一样.用来控制进程执行的二进制通道和更新通道保证了模型检查器可以考虑到每一种可能的序列.用于表示△周期执行的位置是紧急的，因此不消耗仿真时间.计数器的作用是用来保证挂起的进程被完全执行.在事件通知中，坚定位置的作用是保证调度机中事件触发优先于状态改变.

图3 调度机的时间自动机模型

3.3 事件

如果一个事件对象e被其拥有者通知，则那些对此事件敏感的进程恢复执行.System C支持三种类型的时间通知：一种是e.notify(),即相应的进程会在当前△周期立即被触发；第二种是e.notify(0)，即相应的进程会在更新原始通道后下一个△周期立即被触发；第三种是e.notify(t)，t>0，即相应的进程会在给定的时间t后被触发；如果一个事件被挂起的通知所通知，则只有最早的通知起作用，这意味着e.notify()不考虑所有的挂起的通知，e.notify(0)不考虑e.notify(t).

我们为事件对象的建模如图4所示.

图4 事件对象的时间自动机模型

建立的时间自动机模板为每一个被给定的System C设计声明的事件对象实例化一个模型.同步通道notify_imm，notify，wait和整型变量t是它的模版参数.在最初，事件仅仅等待被通知.如果被立即通知，则接收notify_imm?信号，并且在广播通道上立即发送wait!信号.如果一个事件定时通知或者△延迟通知所通知，则接收notify?并且把参数t拷贝给本地变量ndelay，本地变量ndelay是由延迟通知产生的，并且在同一时间，本地时钟x被重置，当前到达的坚定位置被用于重新初始化变量ndelay和重置时钟x.接下来我们需要等待三种情况：1)一个立即时间通知覆盖了所有的当前挂起的通知；2)如果ndelay==0，我们接收到了delta_delay?信号；3)当前延迟到期，即x==ndelay&&ndelay!=0；接下来发送wait!信号，并且回到初始位置.当一个定时通知期满时，通过发送advance_time!信号来通知调度机开始下一个求值阶段.由于广播通道advance_time!的作用，如果多个事件的延迟到期，则只有第一个advance_time被调度机接收；就像之前提到的一样，要想保留System C的语义，调度机就必须不能在时间通知完成之前开始求值阶段.为了保证这条原则，被挂起的事件对象，作为接收者，也需要和advance_time?保持同步；如果它们接收了advance_time?并且在同一时间他们的延迟期满，即如果x==ndelay，他们会立即触发相应的挂起的进程，除此之外其他的什么也不发生.广播同步的语义保证了延迟期满的事件在同一个语义步骤中且在调度机到达求值阶段的时候可以到达坚定位置.坚定位置保证了这些事件在下一个语义步骤中是优先的.

3.4 进程和敏感度

在System C语言中，进程是最基本的执行单位，每一个进程的执行都意味着所调用的函数被执行.在System C中有两种类型的进程即方法进程和线程，方法进程通常在执行时会将方法体从头到尾执行一遍，它由一系列的敏感事件触发.用于建模一个方法进程的时间自动机模型如图5左边所示.线程可以在执行过程中被挂起，动态等待通知事件或者延迟结束，它只会在仿真开始的时候被触发一次.用于开始一个线程的时间自动机模型如图5右边所示.

当一个进程调用wait函数时会被挂起，如果wait()函数被无参调用，则它只有等待敏感事件列表中的事件发生时才会恢复执行；如果进程调用wait(e)函数，则它只有在e事件发生时才会被再次触发；如果进程调用wait(t,e)，则它只有在e事件发生后等待t时间单位后才会被触发；

图5 进程的时间自动机模板

我们采用同步通道的方法为时间敏感性建模，如图6所示.调用wait(e)函数的模型如图6左边所示，它挂起进程，即发送同步信号deactivate!，减少进程计数器ready_procs，然后等待被触发，即和事件对象的wait通道保持同步；当e_wait?信号被接收时，进程增加进程计数器ready_procs并且等待被调度机激活.我们也可以处理组合事件，例如e1&e2或者e1|e2.静态敏感和动态敏感类似，但是当调用wait()时，进程会等待敏感表中的一个事件发生.我们通过等待敏感表中的其中一个事件发生和在广播通道上发送信号sensitive!的方式来为敏感表建模，如图6右边图所示.使用一个坚定位置来保证立即事件通知立即发生.我们为包含一个敏感进程的静态敏感表建立的模型如图6中间图所示.和动态敏感表不同的地方是，我们把e_wait?替换为sensitive?.

图6 敏感事件模型

采用一个特殊的timeout_event来为定时等待建模.每一个进程都有其独有的timeout_event.调用wait(t)过程的模型如图7左图所示.首先，释放一个定时通知来启动超时操作.其次，进程通过和timeout_event_wait?保持同步来等待超时期满.通过增加一个同步信号e_wait?来扩展时间自动机模型的方式来满足等待一个事件定时延迟期满.如图7右图所示；为了保证一个timeout_event不覆盖随后的定时通知，当时间e发生时我们用一个立即事件通知来覆盖它.

图7 定时和敏感事件模型

3.5 通道和模块

模块是系统行为的主要载体，而通道则是通信的主要载体.如果原始通道想要在更新阶段让update()函数被执行则需要实现update()函数并且在求值阶段调用专用函数request_update().我们用一个时间自动机模型来管理更新请求，如图8所示.如果request_update?被接收到，则相应的通道的update()函数被调度机在更新阶段调用.我们通过在时间自动机模型中发送request_update!信号来为调用request_update()函数的过程建模.

图8 请求更新的时间自动机模型

模块和通道的转化要求我们采用变量作为全局变量，配置同步通道和参数声明以及生成必要的时间自动机模板.在System C设计中一个模块或者通道可能会被多次实例化，为了让方法模板可以多次重复使用，我们把所有在模块中可见的声明作为模版参数.当一个模块或者通道需要被转化时，相应的模板就会生成.全局和系统声明只有在一个模块或者通道实例化时才会被添加进UPPAAL模型中.接下来从模块或者通道中生成的模板会用这些声明来进行实例化；对于模块或者通道，事件和进程模板会生成一次.然而，模块中的方法可能会被当前进程多次使用.因此，对于每一个在模块中声明过的进程，所有对这个模块可见的方法都要被实例化一次，相应的全局声明采用模块名和进程名作为前缀.对于每一个绑定了通道的模块的每一个进程，通道的成员方法都要被实例化一次.

尽管在UPPAAL中没有结构层次，但是System C中模块的结构可以通过前缀体现出来.通过一个System C进程设计到UPPAAL进程的一对一的映射，System C设计的结构可以被完全透明的展示给设计者.这对于模型检查器生成反例是非常有用的.

4 实验结果

我们实现了转化并且自动地将System C设计转化为UPPAAL模型.采用Karlsruhe System C解析器作为System C设计的前端.用UPPAAL模型检查器来验证设计的活性和安全性等特性.实验环境为Intel 奔腾处理器 3.5 G主频，操作系统为Linux操作系统.第一个实例是生产者消费者协议；第二个实例是一个经过略微修改的信息包交换的实例.在这两个例子里都包含了System C的通道以及静态敏感、动态敏感和定时敏感的概念.对于生产-消费者实例，我们验证了以下几个属性：1)无死锁;2)无缓冲区溢出；3)消费者在给定的时间内读取生产者发送的所有物品，所有的属性都可以满足.对于信息包交换实例，我们验证了：1)无死锁;2)每一个信息包都发往其接收者方向;3)如果一个信息包被发给其接收者，则在给定时间内可以完成.属性1)和3)都满足的，属性2)不能满足，这是由于sc_signal的语义问题，即当值发生变化时，只有信号端口的改变事件被通知.如果随后的信息是相同的，则在包交换的输入端口没有改变时间发生，因此只有第一个信息会被发送给接收者.在生产者消费者实验中，我们改变了缓冲区大小(BS 10，BS 50，BS 100，BS 1000)，在包交换实验中，我们改变了主从服务器的数量(1主1从，1主2从，2主1从，2主2从)，表1和表2显示了10次实验的验证时间平均值.

表1 生产-消费者实例实验结果

表2 包交换实例实验结果

5 总结

我们提出了一种将System C设计转化为有着良好定义语义的UPPAAL时间自动机的方法.这种转化可以将UPPAAL工具，包括UPPAAL模型检查器，应用在System C 设计上，可以形式化验证System C 设计的时间属性.我们主要是将System C 中的进程转化为时间自动机中的进程以及用通道的概念让它们保持同步.用一个预定的调度机模型、特殊的事件模板和进程模板详细说明了System C设计的执行语义.这种转化可以自动进行且转化时间可以忽略.因此，混合的大型的System C设计也可以被转化.一个给定的System C设计的非正式的行为和结构可以被完全的保留在生成的UPPAAL时间自动机模型上.此外，通过我们这种方法产生的模型很简洁，很容易理解，并且可以有效地被模型检查器验证.在将来，我们会优化这种的转化，也计划用生成的模型来自动选择仿真的输入以及自动评价仿真的结果.

[1] T.Groetker.System Design with System C[M].Kluwer Academic Publishers,2002.

[2] A.Habibi and S.Tahar.An Approach for the Verification of SystemC Designs Using AsmL[J].In Automated Technology for Verification and Analysis,2005.

[3] IEEE Standards Association.IEEE Std.1666-2005,Open System C Language Reference Manual[K].2005.

[4]G.Behrmann,A.David,and K.G.Larsen.A Tutorial on UPPAAL.In Formal Methods for the Design of Real-Time Systems[M].LNCS 3185.Springer,2004.

[5]郭华，庄雷.UPPAAL——一种适合自动验证实时系统的工具[J].微计算机信息，2006(15).

[6]A.Habibi,H.Moinudeen,and S.Tahar.Generating Finite State Machines from System C[M].In Design,Automation and Test in Europe,2006：76-81.

[责任编辑 苏 琴]

[责任校对 黄招扬]

A Method of Model Checking based on System C

WU Li-jia,YU Qiong,JIN Qing-geng

(GuangxiKeyLaboratoryofHybridComputationandICDesignAnalysis,GuangxiUniversityforNationalities,Nanning530006,China)

System C is widely used for modeling and simulation in hardware/software co-design.Due to the lack of a complete formal semantics,it is not possible to verify System C designs.In this paper,we present an approach to overcome this problem by defining the semantics of System C by a mapping from System C designs into the well-defined semantics of UPPAAL timed automata.The informally defined behavior and the structure of System C designs are completely preserved in the generated UPPAAL models.The resulting UPPAAL models allow us to use the UPPAAL model checker and the UPPAAL tool suite,including simulation and visualization tools.The model checker can be used to verify important properties such as liveness,deadlock freedom or compliance with timing constraints.We have implemented the presented transformation,applied it to two examples and verified liveness,safety and timing properties by model checking,thus showing the applicability of our approach in practice.

System C；Timed Automata；Model Checking

2016-03-28.

吴丽佳(1991-)，男，河南许昌人，广西民族大学硕士研究生，研究方向：大规模集成电路验证.

TP312

A

1673-8462(2016)03-0080-06