系统级芯片设计语言和验证语言的发展(3)

验证语言的提出需要说明基于事务的验证和基于断言的验证。解决所谓系统芯片的“验证危机”，策略之一是基于事务处理的验证（TBV），事务是概念上单一的数据或控制的转移，这种转移有事务的开始时间，结束时间和所有相关的信息确定，这些信息和事务一起存储，作为事务的属性。事务处理可以是简单的存储器读写，也可以是具有复杂的结构数据报在网络信道中的传送。把验证的层次从信号层次提高到事务处理层次，让测试具有更直观的方式，有利于测试产生、纠错过程和功能覆盖的度量。设计系统结构不是想象使能信号和地址总线如何工作，而是想象数据如何在系统中流动和存储。TBV就是这种高层次设计过程的自然展开。定性的验证过程包含3个步骤：测试生成、设计查错和功能覆盖分析。每个阶段都要提高到事务处理的抽象层次。可以用Verilog语言的task 来构成事务。这对于基本的测试也许还可以接受，但是当要产生复杂的数据结构、复杂的测试方案，动态的测试生成时，就会产生太多的限制。高级验证语言（HLV）例如近年来开发TestBuilder(C++)、Vera和 E等，就是要解决这些复杂的问题。

基于断言的验证(ABV)是把形式化方法集成到传统模拟流程中的一种有效的方法。设计团队在RTL设计中插入设计意图（断言）并且进行模拟，然后用形式化技术检查断言，限制条件，也就是合法接口行为的断言，和其他断言同时一同参加模拟。断言检查的结果改进模拟的有效性。即使利用传统的模拟验证，断言也可以大大提高模拟的效率。基于断言的验证要由用户写出断言，断言表示要验证的性质，因此需要性质描述语言。例如逻辑和时序方面的性质。这些也是验证语言要解决的问题。

3.2　目前的系统级验证语言概况

IC设计和EDA界需要一种标准化的具有公开接口的验证方法学，在2000年，Open Verilog International和VHDL International联合，组成了Accellera组织。其目的就是在系统、半导体和设计工具企业，推动、开发和培育新的国际标准。以便加强以语言为基础的设计自动化进程。面对几个在语法和语义方面都不够完善的形式性质描述语言，Accellera进行了一个选举过程，4个候选的语言是 Motorola的CBV，IBM的 Sugar，Intel的 ForSpec 和Verisity的e 语言。经过讨论，集中到Sugar和 CBV上，在2002年4月选定了IBM的Sugar 2.0［3］。Sugar 2.0的获胜造成了Accellera组织的分裂，包括Cadence在内的多数EDA工具供应商支持Accellera 的决定。另外一部分则转向支持Syopsys的 OpenVera 2.0。作为一种真正的工业标准语言，Sugar 2.0语法和语义很简单明了。基本上是基于线性时态逻辑语言（LTL）,他是由基于分支时态逻辑(计算树逻辑CTL）的Sugar1.0演化而来的。其关键思想是利用一种扩展的正则表达式的构件。因此对于形式验证领域来说，理解Sugar是很容易的。

Sugar语言是由IBM的Haifa 实验是经过8年研究开发的［4］，是一种说明性的形式化性质规范语言。其语义是严格的，但是易于理解和使用。可以用类似定理的形式 描述要验证 的属性，这些描述可以作为模型检验和定理证明的输入，也可以做模拟程序中检查程序的输入。Sugar由4层结构组成：

布尔层由布尔表达式构成。?

时态层描述逻辑值随时间变化的性质。?

验证层由一些指示词描述验证软件如何利用时态的性质。还有 些验证指示词假设某种性质成立。验证层也提供把Sugar的语句分成验证单元的方式。

模型层提供对于输入行为进行建模的方法，对于辅助信号和变量进行 说明并定义其行为。模型层也可以定义为时态层的性质和实体的名字。

Sugar具有3种风格，分别对应于硬件描述语言Verilog，VHDL和环境描述语言EDL（ IBM的RuleBase 模型检验器使用的语言）。采用不同风格时，在布尔层和模型层的 语法可以不同，但是在时态层和验证层相同。(责任编辑：admin)