>
首页 » 技术文章 » SoC有限状态机优化验证方法研究

SoC有限状态机优化验证方法研究

作者:王忠海,叶以正  时间:2007-01-18 17:14  来源:

摘要:利用图论及数学规划方法分析并解决有限状态机验证路径的选择优化,提出一种在仿真验证方法中对SoC有限状态机验证路径进行优化的方法。C*Core 提供的验证环境中,对其部分Golden File 验证任务的有限状态机进行了优化处理,通过原方案的验证时间的对比,表明了该方法可以使用更短的时间有效解决有限状态机验证问题。

关键词:有限状态机;验证;图论;数学规划

 引  言

在片上系统( SoC) 设计中,验证是最为严峻的挑战之一,为了确保产品的正确性,验证流程贯穿了整个设计过程,当前的SoC 设计中,验证工作占据了约70 %的设计时间和资源消耗。

在硬件设计中,采用有限状态机描述硬件系统的行为,对设计者而言可以使其明确硬件系统的控制流程,方便对设计进行实现。在验证过程中,确认“设计是否符合规范描述的有限状态机”是一个需要解决的基本问题。在传统的基于仿真的验证方法中,状态机验证包含在测试计划之中,验证人员按照测试计划的安排,完成对有限状态机的验证工作。

随着SoC 设计的复杂化,有限状态机的复杂度也随之增。SoC 设计方法是一种将不同功能IP 集成于一个芯片的设计方法,SoC 对应的有限状态机就成为这些IP 的有限状态机的一个集合.传统的依靠测试计划验证有限状态机的方法显然面临着以下两个主要问题: (1) 如何全面覆盖状态转移条件;(2) 如何提高验证效率,缩减验证时间。通过细心编排测试计划,传统的硬件有限状态机验证是能够保证对状态转移条件完全覆盖的,但是它显然难以同时保证验证时间上的优化。此外,如果采用人工编排测试过程的方法,当硬件有限状态机复杂度提高,用于构思验证测试顺序的时间也将会大幅度增加。

本文针对仿真方法中SoC 硬件有限状态机验证提出了一种优化验证方法,该方法可用于提高验证计划和程序的编写效率,同时可以减少仿真验证使用的时间。

 基本概念

本文涉及到有向图论及运筹学的相关知识。

定义1. 有向图D ,以顶点v 为起点的弧的数目叫作v 的出度,记作degout ( v) ;以顶点v 为终点的弧的数目叫做v 的入度,记作degin ( v)

定义2. 在有向图D , 存在一条路径可以从D 中的某一点出发, 经过D 中每条弧一次且仅一次,这样的路径称为Euler 路径;如果存在这样的封闭回路,它遍历D 每一条弧一次且仅一次, 这样的回路称为有向Euler 回路。

定理1. 一个有向图D 存在Euler 回路的充要条件为D 是连通的,并且是平衡的,

degout ( vi) = degin ( vi)

  定义3. 线性规划数学模型的一般形式为

其中aij , bi , cj ( i = 1 , ., m ; j = 1 , , n) 为已知常数。

 有限状态机验证的相关问题

 

有限状态机验证与功能验证的关系

有限状态机验证是功能验证的一个组成部分,但并不等同于功能验证。这是因为状态机验证偏重于对状态转移情况的遍历,而功能验证往往代表着对一系列状态转移不同组合情况的确认。图1 所示为功能验证包含的内容以及这些内容彼此之间的区别和联系。

功能验证不仅包含了有限状态机验证问题,还包括对不同状态转移组合情况的验证以及对角落事件的验证。

有限状态机验证与有向图遍历

硬件的有限状态机问题可以抽象为对有向图进行研究,有限状态机验证的实质是按照各种状态转移条件运行有限状态机,确认其到达规定的各个状态。这在其对应的有向图中是一个遍历问题。与一般有向图比较,硬件有限状态机对应的有向图有其自身的特点: (1) 硬件设计具有初始状态,因此其对应的有向图具有初始结点,这就使得要单独验证某状态结点时必须要由初始结点出发; (2) 硬件设计中存在置位情况,这在有向图中相当于初始结点之外的其他结点都有一条有向边可以直接回到初始结点。

有限状态机的验证中,要验证某一状态往往要经过数个状态转移,显然这些中间状态和状态转移情况被同时验证了。当验证的情况增加时,这些中间状态和状态转移情况被重复验证的情况也同时增加,这就意味着仿真验证时间的增加。在对应的有向图中,这表现为对一些有向边的重复经过。

 有限状态机的有向图加权

上面提到了有限状态机中的仿真时间,这里进一步讨论有限状态机中的加权问题。

在状态机运行过程中,状态转换本身并没有产生时间消耗,而是在进入某一个状态之后出现了运行时间问题。 因此,我们将其有向图的权值规定为:一个有向边的权值是该有向边指向的那个状态本身运行消耗的时间。

以图2 为例,状态结点1 的实现代码中使用的判断语句就构成了状态转移情况,两种情况下( condition-1 condition-2) 状态1 可以跳转到状态2 ,这就构成了从状态1 结点到状态2 结点的两条有向边1 有向边对应的权值则是其在状态2 实现代码中对应代码的运行时间( task1 task2)1 因此同样是由状态1 到状态2 的跳转,由于其跳转的条件不同,对应的权值也可能不同。权值的计算可以是一个预估值,也可以是精确的时间,这将根据验证的层次不同而定。

有限状态机验证面临的问题

由上面的讨论可以看出,有限状态机验证面临着以下两个主要问题: (1) 有限状态机状态转移情况的覆盖问题。目前仿真验证方法中包括有限状态机验证在内,都以人工编程方式为主,随着状态规模的扩大,如何保证所有状态转移情况都被覆盖,这既是一个工程设计问题,也是一个验证方法问题; (2) 仿真验证时间的优化问题。如前面所言,实际情况中为了验证某一个特定的状态,势必要经过其他一些状态转移条件的组合才能实现,对于有限状态机验证而言,这些中间状态转移情况在验证特定状态的同时也被验证了。当有限状态机变得复杂时,这种中间状态转移被重复验证的情况会频繁出现,这就意味着相当一部分仿真验证时间被这种重复验证耗用了。因此,如何有效地减少不必要的重复验证也是有限状态机验证面临的问题。

 

SoC有限状态机验证优化方法

 SoC有限状态机的遍历方式

对于有限状态机验证来说,如果可以从初始结点出发找到Euler 路径或Euler 回路,则它不仅会覆盖全部状态转移情况,同时其验证使用的时间也是最优化的。根据Euler 路径和Euler 回路存在定律,在实际的有限状态机中,Euler 路径或Euler 回路几乎不可能存在。

除此之外,如果可以使得所选的多个验证任务是待验证状态机的不同子集,并且这些子集的并又覆盖了原有向图,那么这种选择也是非常理想的,但是这种有向图子图覆盖问题是NP 问题。

上述分析表明,对于有限状态机验证来说,合理的方法应该是在对有向边遍历的前提下尽可能地减少被重复的有向边的权值总和(即时间)。在硬件有限状态机中构造Euler 路径和回路,可以有以下两个优点: (1) 可以实现对有限状态机的完全覆盖;(2) 可进行严格的优化,使验证问题等到合理解决。考虑到构造Euler 回路比构造Euler 路径更适合于IP 模块和SoC 集成后的有限状态机统一化处理,我们采用在硬件有限状态机中构造Euler 回路的方法。

构造Euler 回路的可行性证明

构造Euler 回路的方法,构造方法:从每个入度大于出度的结点(我们这里称之为入度点) 出发,找一条到每个入度小于出度(出度点) 的结点的最短有向路,从中取最小者,添加这条有向路上的所有重弧1对新得到的图,重复此步骤,直至所有非平衡点变成平衡点,此时可得到有向Euler 回路。

定义4. 对于出度大于其入度的非平衡结点,其出度值与入度值之差的绝对值定义为该结点的出值;同理定义入值。

定义5. 在有向图D , 如果任意两个不同的结点互相可达,则称该有向图是强连通的。

根据硬件有限状态机的特点,有下面的引理。

引理1. 硬件有限状态机对应的有向图是强连通的。

证明. V W 分别是硬件有限状态机对应有向图D 中任意两个不同结点,另设S D 的初始结点。由有限状态机性质可知,必有路径Pv 可以实现由结点S 到达结点V (若没有路径Pv 则表明结点V 所代表的状态是状态机无法到达的, 这与V是有限状态机的一个状态的性质矛盾) 同理,必有路径Pw 可以实现由结点S 到达结点W

根据硬件有限状态机的置位特性可知,有路径Bv B w 可以实现由结点V 和结点W到达初始结点S 。因此,路径( B w , Pv ) 就实现了由结点W 到达结点V ,路径( B v , Pw ) 就实现了由结点V 到达结点W ,从而V W 互相可达。

因此硬件有限状态机对应的有向图是强连通的。

证毕。

定理2. 由硬件系统有限状态机生成的有向图可以构造Euler 回路。

证明. 设有向图D 中有n 个结点,其中平衡点用pi ( i = 1 ,2 , ., m) 表示,非平衡点用f i ( i = 1 ,2 ,., t) 表示,显然有m + t = n

又因为平衡点

  这个结果说明非平衡结点的出度之和与入度之和相等。结合引理1 可知, 从一个入度结点到一个出度结点是存在有向路径的, 因此本文给出的构造方法中关于“从每个入度大于出度的结点出发,找一条到每个入度小于出度的结点的最短有向路径”是存在的。同时每引入这样一条路径,就会使得相应的起始结点(即入度结点) 的入值减少1 , 而这条有向路径的终点(即出度结点) 的出值也会减少1 显然这样的路径每增加一条, 就会使非平衡点的出度和入度总和在数值上同时减少1 , 因此在经过有限次(我们用ct 表示这种操作的次数) 这种操作之后,原有的有向图最终会被改造成为全是平衡点的有向图。

问题优化的原因

上面给出的构造方法的可行性证明表明,根据非平衡结点的出值与入值,可以于有限步骤内在原有向图中构造出Euler 回路。但是这种构造方法并不一定是优化的,即其增加的权值总和不一定是最少的。本文以一个简单的加权有向图为例来进行说明,如图3 所示。

3 中出度结点有“1,3,4,其出值都是1 ,入度结点有“2,6,7,其入值都是1。按照第4.2 节给出的构造方法,从结点2 ,6 ,7 各出发1 ,寻找到达结点3 ,4 ,6 中的对应结点的最短路径,就实现了有向Euler 回路的构造。 注意,一旦一个非平衡结点改造成为平衡结点,就不能再对其进行改造了。

根据排列组合原理,由结点“2, 6, 7”到“1,3, 4”的对应方式共有P33 = 6 ,1 所示为这6种对应方式。

应该注意的是,每一种对应方式中结点和结点的映射关系代表的是两个结点之间最短有向路径,比如方式1 中⑦→④表示的是由结点7 到结点4 的最短有向路径:7 2 4 。显然,每一种对应方式就代表着一系列的新增有向路径, 也同时意味着一种新的验证路径和其仿真运行需要的时间。

可见当出度结点、入度结点数目及对应的出值与入值增加时,这种对应关系的排列组合情况也会增加。如何在这些可能的对应关系中找到使验证运行时间最少的那种关系是我们关心的。

Euler 回路构造方法可以发现, 原有弧的权值是必须计算在内的, 因此实现优化的关键就在于使增加的重弧的权值总和为最少。为了使增加的重弧总权值最少,显然需要计算

其中, Pij表示从结点i 到结点j 的最短有向路径,结点i 是入度点,结点j 是出度点, ct 是操作次数。

选择最短有向路径的方法有很多,为了便于编程实现我们选择了Dijkstra 算法。

Dijkst ra 算法:引入辅助向量L ,其分量L [ i ]表示当前找到的从源点v 到每个终点vi 的最短路径的长度,用加权邻接矩阵dist [ i ] [ j ]表示有向图,dist [ i ][ j ]表示弧〈vi , vj〉上的权值,若〈vi , vj〉不存在,则置dist [ i ][ j ]为某一最大值M。向量S 是已找到的从v 出发的最短路径的终点的集合, 其初始值为空集,算法具体步骤如下:

Step1. v 出发到图上其余各顶点(终点) vi 可能达到的最短路径长度的初值为L [ i ] = dist [ v ][ vi ] , vi V

Step2. 选择vj ,使L [ j ] = min{ L [ i ]| vi| S , vi V } 。则vj 就是当前求得的一条从v 出发的最短路径的终点;且令S = S { vj} ,即将vj 加入到S 集合中。

Step3. 修改从v 出发到集合V - S 上所有顶点vk 可达到的最短路径长度。如果L [ j ] + dist [ j ] [ k ] < L [ k ] , 则修改L [ k ]L [ k ] = L [ j ] + dist [ j ][ k ]

Step4. 重复Step2 Step3 最后可求得从v 到图上其余各顶点的最短路径是依路径长度递增的序列。

其中, V 为有向圆顶点结合。

为了求解式(2) ,需要建立选择矩阵进行分析。

 选择矩阵

设集合R 由入度点组成, 称为入度集合, 集合C 由出度点组成,称为出度集合,由集合R 到集合C 的映射关系为最短有向路径。 以图3 为例,出度集合的元素有结点1 , 3 , 4 ;入度集合的元素有结点2 ,6 ,7

为分析从集合R 中集合C 的映射关系问题,先作如下假设:设集合R b 个元素r1 , r2 , , rb ;集合C 中有d 个元素c1 , c2 , , cd ; 同时引入选择矩阵Xb ×d = ( kij) b ×d1 其中, kij = 结点ri 到结点cj 的最短有向路径长度。

特别地, 我们令集合R 中的元素作为行, 集合C 中的元素为列,这样可以得到图3 的选择矩阵为

选择矩阵的概念虽然清晰,但是一般情况下行数b 与列数d 不等, 不便于对问题的理解和解决,需要进一步的变换。可以按照下面的方法定义新的选择矩阵Xs ×s :

Step1. 对于入值等于h ( h 1) 的集合R 中的元素,其对应的矩阵行重复生成h .

Step2. 对于出值等于m ( m 1) 的集合C 中的元素,其对应的矩阵列重复生成m .

优化问题的解决

有了新的选择矩阵,(2) 的问题就转化成在约束条件“一旦选中某一元素,其同行与同列的其他元素都不能选择了”下,怎样从选择矩阵Xs ×s中挑选元素,使得选出的元素总和值最小。

这个问题的数学模型可以表示为

其中, vij表示矩阵中元素aij的权值, x ij表示选择系数,对于选择系数x ij有约束条件

  由式(1) 可知,(4) 的问题是一个数学规划问题,解决这个问题的方法很多,为了易于编程实现我们选择了匈牙利算法,具体步骤如下:

Step1. 把各行元素分别减去其所在行元素中的最小值;然后在此基础上再把每列元素减去其所在列中的最小值。此时每行及每列中肯定都有零元素了。

Step2. 确定独立零元素,并作标记。若独立零元素等于矩阵阶数,则已经得到最优解,若小于矩阵阶数,则继续。

Step3. 对矩阵进行最大覆盖,在未被直线覆盖的所有元素中找出一个最小元素,用未被直线覆盖的行中所有元素减去这个最小元素。

Step4. Step3 必然出现负元素,对负元素所在列中各元素都加上这一最小元素以消除负数;再返回Step2 ,确定独立零元素个数。

Step5. 重复上述操作,直到找出最优解。利用匈牙利算法对前面得到的选择矩阵进行求解得到

这个结果表明,构造以下三个最短路径即可实现图3 所示的加权有向图的最小有向Euler 回路:由结点2 到结点4 的最短路径、由结点6 到结点1的最短路径以及由结点7 到结点3 的最短路径,即增加图4 中虚线所示的重弧。

增加重弧之后,可以实现优化原有的验证状态机的目的,以增加最少的被重复验证的状态转移情况对状态机进行完全遍历。 我们可以按照下面的路径遍历增加重弧后的图3 :1 - 2 - 4 - 6 - 2 - 4 - 5 -2 - 3 - 5 - 6 - 2 - 1 - 7 - 7 - 2 - 1 - 7 - 2 - 3 - 6 - 7- 11 利用这条验证路径不仅可以覆盖验证有限状态机的所有状态转移情况,同时可以保证验证用时是优化的。

优化方法小结

本文的优化方法优化的过程如下:

Step1. 由有限状态机产生邻接矩阵和距离矩阵,其中邻接矩阵说明了有限状态机对应的有向图的状态转移及出度、入度关系,距离矩阵是在计算最短路径时结合邻接矩阵使用的,这两个矩阵可以利用数据结构中哈希表方法快速生成。

Step2. 由邻接矩阵计算得到非平衡结点,然后结合距离矩阵通过Dijkstra 算法计算出非平衡结点之间的最短距离关系矩阵。

Step3. 使用匈牙利算法从最短距离关系矩阵中计算得到优化解。

本文编程实现了这一优化方法,其设计实现流程示意如图5 所示,其中Graph 运算模块用来实现Step2 中对于非平衡结点的计算,产生非平衡结点之间的对应矩阵,Dijkst ra 算法模块结合距离矩阵与产生的对应矩阵计算最短路径,经过Dijkst ra 算法模块之后将产生关系矩阵,并由数学规划算法模块计算得到验证路径。

有限状态机的验证路径是验证人员进行验证测试遵循的依据,传统的方法中验证路径是人工选取的,这样做不仅会占用大量人工思考与比较选取的时间,同时得到的结果也会由于状态复杂度的增加而出现状态重复验证的情况,有时甚至会造成一些状态转换条件的遗漏情况。 经过本文优化方法得到的验证路径有效地解决了这些问题,优化验证路径可以自动产生,验证人员只需依据得到的验证路径即可进行验证测试编程。

 实验及结果分析

本文实验是在苏州国芯科技有限公司提供的C*SOC100仿真验证平台进行的,C*SOC100 能够支持RTL 以及门级的仿真,包括完整的功能验证模块。我们对其自带的Golden File 中的部分验证任务进行了状态机验证优化处理。

实验用机的硬件环境为: Sun 工作站,CPU 443MHz ,内存为128 MB

2 所示为这些验证任务的状态及状态转移数,同时包括这些验证任务在C*SOC100 环境中的原始验证仿真时间及我们经过有限状态机验证优化方法之后运行的时间比较。由于验证路径的优化过程是使用程序自动进行的,耗时很少(这里优化的例子耗时均小于1 s) ,所以没有将其计入优化时间之内。从表2 可以看到,随着有限状态机的复杂度的提高,CPU 仿真运行使用的时间在优化前与优化后的变化逐渐变大,显然这些变化会影响到整体仿真的时间。

  表2 中的结果也与文中对于这种优化方法的解释是一致的,随着状态机的复杂化,人为的对于状态机验证路径的规划会出现越来越多的冗余验证,即对于一些状态转移情况进行了不必要的多次验证。因此可以说随着状态机复杂度的增加,本文提出的优化验证方法就越显示出良好的优化效果。

 结  论

通过实验结果可以看出,使用本文提出的状态机优化方法在保证所有验证目标不缺失的情况下,可以有效地缩短验证时间。缩短的验证时间来自于那些原验证任务中被忽视的、重复验证的状态转移情况。虽然这些状态转移情况每一个的时间耗用可能不多,但是其累加起来的量却很大,这就是为什么可以出现表2 中缩减出的时间,而且实验结果表明越是复杂的有限状态机这种优化的效果就越显著。此外由于本文方法自动化的特点,它在验证测试计划阶段同样可以有效地节省验证人员对验证路径选择时的筛选时间。

相关推荐

NEC与F5 Networks共同实施基于节能平台的SAP系统优化验证

NEC  F5 Networks  SAP  验证  2009-06-19

混合信号FPGA的智能型验证流程

FPGA  验证  PSC  2009-05-19

微捷码FineSim SPICE被作为标准验证工具

2009-05-06

泰克仪器用于3Gb/s监视器设计验证和测试

2009-04-24

Cadence公司CPF在低功耗设计验证中的应用

CPF  低功耗  验证  2009-04-15

新思科技VCS多核技术使验证速度提升两倍

新思  VCS  多核  验证  2009-04-07
在线研讨会
焦点