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

3　系统级验证语言

3.1　基于事务的验证和基于断言的验证

验证语言的提出需要说明基于事务的验证和基于断言的验证。解决所谓系统芯片的"验证危机"，策略之一是基于事务处理的验证（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。Sugar 2.0的获胜造成了Accellera组织的分裂，包括Cadence在内的多数EDA工具供应商支持Accellera 的决定。另外一部分则转向支持Syopsys的 OpenVera 2.0。作为一种真正的工业标准语言，Sugar 2.0语法和语义很简单明了。基本上是基于线性时态逻辑语言（LTL）,他是由基于分支时态逻辑(计算树逻辑CTL）的Sugar1.0演化而来的。其关键思想是利用一种扩展的正则表达式的构件。因此对于形式验证领域来说，理解Sugar是很容易的。

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

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

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

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

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

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

OpenVera 1.0 是Synopsys捐献出来公开的验证语言。对于模拟，他已经具有描述断言的能力。Synopsys公司和Intel公司的ForSpec相结合后产生的OpenVera 2.0也能够支持形式化验证。和Intel公司联合推出OpenVeraForespec 作为工业标准的断言语言，但是因为对于工程师来说难以接受，因此被拒绝。但是其概念还是有特点的。他的目标是作为一种支持模拟和形式验证的性质描述语言。从ForSpec借用的构件和操作包括"assume"，"restrict"，"model"，"assert" 等，这些都为形式化验证服务。语言成分" assumeguarantee"可以把断言作为模块的性质，在高层上又作为监视器。OpenVera 用来描述断言时可以精确的描述在多个周期时间的时序行为。硬件描述语言例如Verilog和 VHDL是用来描述硬件的过程行为。这种过程模型难以有效地表述在多周期的时态行为。利用Ope nVera的断言语言OVA，用户可以方便直观地描述输入输出行为、总线协议以及其他复杂的硬件行为和关系。和硬件描述语言的描述比较，要简洁3~5倍。和Sugar语言的4级结构相比，OpenVera 2.0分为5个主要的级别：

上下文（环境）帮助定义断言的辖域（或作用域）。

指示词描述所要检查或监视的性质。

布尔表达式。

事件表达式表示时间序列。

公式表示表述时间序列之间的关系。

Sugar和 Open Vera 2.0 有2个层次是相同的，即布尔层和时态层。这些层构成了断言的核心。他们的差别在其他层次上面。OpenVera 2.0 重视性质的细致结构，用户能和断言深入交互，以便考察和探索形式验证的知识。Sugar的另外2个层次服务于性质的"格式化"，而简化与用户的交互。总之，不管用那种语言，Open Vera 2.0 或者Sugar，他们都提供了高效验证复杂系统芯片的手段。

4　对于当前验证方法的*述

目前的设计验证方法迅速发展，设计和验证语言层出不穷。但是以下的观点和结论是明确的：

1）形式化方法取得了长足进展，特别是等价性检验已经集成到标准验证流程中。模型检验技术以及定理证明等还不能成为设计环境的主流验证方法的主要原因有:

①缺乏广泛接受的性质描述语言。

②缺乏商业化的工具。

③至今缺乏有效地使用形式化方法学的指导原则。

④在改变验证方法带来的收益是否明显的问题上还在观望。

2）形式化方法还需要和传统的方法相结合才能发挥作用。设计和验证方法的进步应当是渐进的，不可能革命性的改变。因此在可以预见的几年内，混合验证方法应当成为主流的验证方法。断言对于表示接口限制、设计性质和设计假设都具有很深刻的作用和影响。这些会对发现过去的方法不能发现的设计错误做出贡献。特别适合测试覆盖结合起来可以极大的改进验证效率。

3）基于断言的验证是结合形式化验证和传统的模拟验证可行的途径。支持这种途径的统一的设计和验证语言是SystemVerilog。他是在新的Verilog语言标准上扩充系统描述构件而开发的一种过渡性的系统级设计语言。该语言可以统一的描述复杂的设计和测试方案（ testbenches）。SystemVerilog支持多级接口设计和断言，充分利用了当前的设计验证技术和实践。他后向兼容verilog,具有继承性，与其同时成为一个结合设计和验证的语言。该语言已经得到很多EDA厂商和用户的支持，预计将会流行起来。