等效性检查在芯片设计的验证过程广为应用,然而,由于用户模型既非门级也非可综合RTL,因此用户设计工程师认为等效性检查并不实用。最近出现的可支持晶体管级和行为级结构的符号仿真技术,使用户设计工程师有可能建立自己的等效性检查技术。
过去五年来,形式验证技术已被证明是EDA领域中最有前途的开发工具。形式验证能解决关键的验证问题,并能加大功能覆盖率,同时可极大地缩短达到目标覆盖率所要花费的时间。形式验证的关键是将两个设计进行等效性比较,即等效性检查工作,目前为止,等效性检查的重心一直是放在门级到门级、RTL到门级以及RTL到RTL。
一般来说,开展等效性检查需要满足如下一些要求:1. 可综合RTL或门级描述；2. 同步设计；3. 两个描述间的状态点映射。
当这些要求得到满足时,等效性检查工具就能充分发挥其强大功能和易用性,并能取得设计的巨大成功。等效性检查能有效填补综合驱动设计方法中的空白,并能将仿真时间缩短数周。
在系统级芯片(SoC)设计中,采用有效的方法比提高时钟速度更能提升系统性能,因为电源与热问题会限制时钟速率,并且难以克服。解决问题的关键是提高集成度,特别是增加片上的存储器容量。用户定制存储器和其它模块的设计工程师采用等效性检查的理由在于,他们向SoC客户提供的行为模型必须与电路实现相等效性。这些嵌入式存储器周围存在大量的逻辑,因此很有可能发生难以跟踪的缺陷。另外,所选用的仿真环境(Spice或Fastspice)可能造成比基于语言的流程需要更长的运行时间。此外,目前尚没有现成的方法将Spice工具的输出与参考模型做比较。
对用户设计人员来说,旧的等效性检查工具基本没什么帮助。原因有三点:首先,由于没有对模型进行综合的考虑,所以参考模型是不可综合的；其次,设计模块之间不一定是同步的,因此存在许多当前的等效性检查工具无法探测的复杂时钟方案；第三,不存在状态点映射(state-point mapping)。
但随着形式验证技术中先进功能的不断增加,现在所提供的等效性检查工具已非常适合广大用户电路设计工程师使用,可以使他们更方便、更有效地用于开发SoC的IP或内核。
半形式符号仿真的运用
原始的形式验证工具主要是进行等效性检查和模型检查,而现在形式验证已经运用到了一些崭新领域,半形式验证(semi-formal verification)就是其中之一。半形式验证方法能很好地做到易用性与完整性的统一,它也许不能保证在所有情况下提供百分之百的覆盖率,但它具有更大的容量以及更好的易用性。
符号(symbolic)仿真是一种事件驱动的仿真,它的输入端需要引入符号或变量。以前设计工程师常用0、1、X和Z,而现在还可以用S。旧的仿真器传输0、1、X和Z,而符号仿真器除了能传输0、1、X和Z之外,还能传输表达式。
请考虑这样一个告警例子:当门(D)或窗(W)打开时,告警(W)被置位,并发出告警音(图1)。旧的仿真器在完全验证该设计时需要八个矢量,而符号仿真只需要一个。符号仿真时传输的并不是实际值,而是逻辑表达式,该表达式表示了输入输出之间的关系。因此符号仿真能以非常高效的方式验证全部行为模型。这种技术的优越性在于等效的二元覆盖(binary coverage)是两符号输入。如果采用10个输入,那么有1000X个覆盖；当使用100个输入时,大约是1030X个覆盖。用户等效性检查充分利用了这种覆盖的优越性。
用户等效性检查的工作原理有别于旧的等效性检查,但仍能让用户设计工程师比较晶体管级设计与行为参考模型。用户等效性检查依赖于两大要素:
- 统一的仿真环境,该环境允许设计人员进行晶体管级模型输出与行为参考模型的比较。
- 可提供完整功能覆盖的符号输入传输功能。
用户等效性检查工具需要把被测试的晶体管级模型器件与其参考模型(REF)连接起来,这样可保证两者有相同的输入,然后再比较它们的输出结果。从某种角度看,这种用户等效性检查在一定程度上类似于传统的检查方法,不同点在于它的输入信号不是确定的1/0值,而是符号(变量值)。用户等效性检查方法可以提供完整的功能验证覆盖,但所用时间只是旧的检查方法的几十分之一(图2)。
图3给出了等效性检查的四个步骤:
- 读取Spice网表并建立存储器的Verilog开关级模型。这一步需要设置正确的晶体管方向(或使晶体管处于双向状态),识别缺陷晶体管,向时钟发生器等自定时电路插入延时,并用行为模型替代模拟元件。
- 准备约束条件。约束作为控制信号1的输入端,从而选择是高电压、互斥、高电平激活还是低电平激活？并对输出数据有效时的输出检查进行约束。
- 进行比较,并试图发现开关模型与参考模型之间的任何不同点。
- 对这些不同点进行调试和排除错误。
因此设计人员采用用户等效性检查方法能方便地开展晶体管级实现(如SRAM)和行为参考模型之间的比较检查工作。旧的等效性检查需要数周的运行时间才能达到一部分覆盖率,但现在的等效性检查做到完整的覆盖率也只需数个小时。
存储器设计实例
SRAM和SDRAM存储器是代表验证复杂性的两个极端例子。SRAM概念上非常简单,但随着性能的不断提高,SRAM的结构也变得越来越复杂,因此通常很难发现潜伏的故障。验证复杂性的另外一个极端例子是内含复杂定序器(sequencer)的大型存储器SDRAM,它不仅需要数据完整性检查,还需要序列完整性检查。序列完整性需要检查所有可能的合法或非法序列,以便发现定序器(大多数SDRAM有4个)是否被锁定并影响到存储器的正常工作。
单端口SRAM需要进行数据完整性检查。换句话说,如果往任意地址写数据,然后从同一地址再读出来,读取过程是否真实可靠？再换个角度想:如果往任意地址写任意数据,然后从其它地址读数据(也就是说要读的数据并不是刚写进去的那个),那么前面的写入操作会影响到现在的读取操作吗？
这种情况下的4个检查步骤是:1. 读Spice网表；2. 准备比较约束条件；3. 进行比较；4. 调试不同点。
毋容置疑,读取Spice网表并将之转换成HDL格式费时费力。设计人员比较晶体管级与行为参考模型的基础就是HDL(例如Verilog),然而由于HDL仿真器是对数字信号进行处理,所以从Spice网表转换的过程很容易丢失数据。
在此,需要管理的信息非常多:
- 当存在冲突时,需要识别缺陷晶体管。这在字和位线、锁存器以及内核存储单元中比较常见。
- 自定时电路如时钟发生器依靠小的延时来产生脉冲。在缺省情况下,HDL仿真器的正常运行时延是零,因此需要人工插入时延值。这些时延值并不需要十分精确,只要足以产生和传输脉冲就行。
- 要用行为模型替代模拟元件。HDL仿真器在数字域工作,它把晶体管当作是一个开关,因此任何工作于晶体管线性区域的元件都必须用行为模型替代。另外,设计人员可能会对自己确信的正常功能模块(例如传感放大器)选用行为模型,这样可以提高运行时间性能。
- 要去除不影响功能的晶体管,如偏置晶体管。对于偶然的初始化,需要多次定义初始化条件,因此不可避免要花费一定的时间。另外,还需要一些工具用来管理从Spice到HDL的转换过程。
转换工作一般需要花2小时到2天不等的时间,具体取决于存储器的复杂程度(图4)。一般会有一个转换环境,用于读取Spice网表和配置文件以及所有的模型文件,模拟元件的行为模型就保存在这些模型文件中。设计人员希望转换工作会成为未来自动化设计的重要组成部分,并藉此大大减少人工干预的工作量。
准备比较约束条件
缺省的等效性检查过程需要循环6次。根据需要,循环次数还可以增加,但在正常情况下6次循环已足够处理每个序列。
前3次循环用来初始化模型,并检查这些模型的读写功能是否正常。符号周期(symbol cycle)涵盖了读和写,因此3次循环涵盖了从3次写到3次读的所有可能性。
即使检查对象不是存储器,也可以运用同样的规则,当然这时就不是读和写了。从模块初始化开始,用两个二元周期检查所有元件是否工作正常,然后通过一系列符号循环就可以覆盖整个功能空间。
约束条件的修改可以手工完成,更简单的方法是利用工具读取正在使用的模型并通过管理内部机制来设置约束条件。尽管做了很大的努力,设计人员仍须再次确认所写的约束条件是否正确,这很关键。半形式验证可以完全揭示设计人员的所有设计行为。
至此,设计人员差不多完成了所有的手工作业。等效性检查器开始自动运行,并产生所有差异点的计数样本。设计人员可以运行等效性检查器以确认读写周期是否工作正常(换句话说,检查器从REF和DUT处读回在前一周期写入的数据),然后在符号周期检查整个功能空间。
日志文件会记录所有的不同点,这也是新的等效性检查工具功能强大的一个方面。全部6次循环中大部分输入端都是符号或变量,6次循环结束后如果出现任何差异,系统会自动产生错误报告文件。这个错误文件中的变量都有具体值,以便于再现错误情况。
接着,所要做的就是用这些确定值重新开始检查。这时会产生具有重要意义的波形轨迹,它们可以帮助设计人员及时识别错误位置并加以修正。
这一工作有点等价于“搜索营救”操作。符号验证会扫描整个空间以搜寻错误。当发现错误时,它会自动产生一套确定的数值,以便设计人员快捷地找到错误所在的位置。
存储器的容量与复杂性不同,运行时间也不同,有时差距还比较大。最长运行时间是10分钟。实际的运行时间有时会延长到30分钟或数个小时。如果太长那就不正常了。
由于等效性检查依赖于行为级与晶体管模型并存的HDL环境,设计人员必须作好从Spice到Verilog的转换准备工作。一旦所有条件具备,等效性检查就能在覆盖率与运行时间方面显示出极大的优越性,并能提供方便易用的调试流程。
256MB SDRAM是一种带复杂定序器的存储器,因此必须分成几个部分分别检查。通常把SDRAM分成存储器组和定序器两大部分。第一项工作是检查存储器组的数据存取操作,第二项工作是检查定序器是否以合法控制序列正常工作。
SDRAM是由某种序列控制的大容量存储设备,其内部每个存储器组都有一个独立的状态机与其它状态机协调工作。SDRAM的检查内容包括了对存储器、状态机以及状态机之间通信的检查。
首先需要测试的是数据完整性,这时可以把SDRAM看作是一个大容量存储器。众所周知,符号数据和地址要采用合法的读写序列,这样才能证明:如果控制序列是合法的,存储器就能对任何地址存取任何数据。
其次需要测试序列的完整性。这时要使用地址与数据检查小型子集的所有合法序列。换句话说,要测试各个独立的状态机之间是否存在合法的交互作用,以便存储器能正确停止工作。
SDRAM序列验证
序列验证的方法是插入合法的符号命令。例如,当状态机空闲时,合法命令有:ACT(激活行)、REF(刷新)、MRS(模式寄存器设置)、NOP(空操作)。在每个检查周期的开始,设计人员需要确定将要操作的具体存储器组(可以从存储器组地址获得有关信息)。确定了存储器组后,需要决定目前的状态,然后根据状态产生覆盖了所有合法状态的符号输入。
由于是符号形式的输入命令,因此在一个周期内就可覆盖所有可能的命令。如果存储器地址也是符号,那么可以为所有存储器组产生全部可能的合法命令。
实际上,16次处理就可以覆盖所有状态机之间交互作用的全部可能性。为了演示这种验证,需要一个可以揭示内部存储器状态的白盒子模型。下图所示的外部模型或向参考模型中加入这种功能即可满足这个要求(图5)
SDRAM检查环境会自动产生合法的符号输入,这些输入覆盖了所有可能的输入值组合。外部白盒模型的使用可以提供独立检查参考模型和开关模型的能力。检查环境并不对模型初始化,它只是提供信息所需的必要条件。然而一旦所有模型都得到初始化后,检查环境可以按步骤检查序列并报告存在的差异。
检查细节
SDRAM检查可能不会引起人们太大的兴趣,然而,这种检查技术本身非常重要,它代表了以序列为主导的检查,在许多存储器和其它设计领域会有广泛的应用。
对于序列检查来说,地址与数据大部分具有明确的数值。上文已描述了数据完整性检查,并对命令合法情况下的存储器工作进行了检查。下面需要研究的是:是否可能存在引起状态机锁闭的序列命令。可以把这个问题作为一个嵌套条件描述来考虑:
=============================
顶层条件描述命令
case (bank_address)
2'b00: active = bank0;
2'b01: active = bank1;
2'b10: active = bank2;
2'b11: active = bank3;
endcase
legal_command(active);
============================
这条命令说明了哪个存储器组是激活的,哪个存储器组会产生下一个命令,并为激活存储器组产生所有的合法命令。记住,如果bank_address是一个符号,它就代表所有的存储器组。
legal_command命令现用于创建序列,虽然不能涵盖所有的状态机,但仍可以涵盖上面所提及的情况。现假设该命令处于IDLE状态:
===========================
IDLE: begin
case (next_fork)
2'b00: next_command = NOP;
2'b01: next_command = REF;
2'b10: next_command = MRS;
2'b11: next_command = ACT;
endcase
ACTV: begin
==========================
对存储器组可以应用相同的技术。这里有个值next_fork,如果要确定的值,那么将从4个选项中选1个；如果next_fork是一个符号,那么它可以覆盖所有的路径。
这是经过简化的工作过程,因为有些过去的状态可能先占用了某个数值(例如,如果其它存储器组处于某个确定状态,REF将是非法的)。这正是白盒提供信息的地方。道理其实很简单。在测试时,如果是用确定的数值,需要进行反复的多选一工作(4个存储器组中选出1个,4个命令中选出1个)。但如果用符号的话,自然就能涵盖所有可能的组合。
同样重要的是,当发现有不同点时,等效性检查工具会产生明确的数值,因此调试变得相当简单。存储器的容量(在此是256MB SDRAM)充分说明了等效性检查工具的强大功能。在进行数据完整性检查时,可以先执行2次符号读,再执行2次符号写。SDRAM具备执行任意长度突发读写的能力,在此可以限制为4个脉冲。序列完整性检查被限制为具有确定数据和大部分确定地址的16次循环,由于这里的重点不在于数据完整性,因此16次就足够了。数据完整性检查的运行时间从30分到3小时不等,主要取决于运行机器的类型。而序列完整性检查所需时间为1到4小时。这两者的具体运行时间要取决于参考模型的复杂度以及开关级模型的详细情况。
SDRAM最吸引人的因素还是序列完整性检查。它向人们演示了如何去构造一系列相当复杂的测试,却不用考虑所有的奇怪偏僻案例。通过创建由随机取样功能空间获得的确定数据所驱动的测试,并借助于符号,设计人员能实现所有测试要求。
本文总结
为了满足性能、成本、容量和功耗等方面的市场要求,SoC器件必须使用最成熟的模块和工具。先进的存储器结构和其它用户模块将变得越来越重要,因此也会驱动设计工程师用来开发用户芯片的行为模型的需求,最终激发对等效于用户实现的行为模型的强劲需求。
京公网安备 11011202001138号
