Sugar语言是由IBM的Haifa 实验是经过8年研究开发的［4］，是一种说明性的形式化性质规范语言。其语义是严格的，但是易于理解和使用。可以用类似定理的形式 描述要验证的属性，这些描述可以作为模型检验和定理证明的输入，也可以做模拟程序中检查程序的输入。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）形式化方法取得了长足进展，特别是等价性检验已经集成到标准验证流程中。模型检验技术以及定理证明等还不能成为设计环境的主流验证方法的主要原因有［3］:
①缺乏广泛接受的性质描述语言。
②缺乏商业化的工具。
③至今缺乏有效地使用形式化方法学的指导原则。
④在改变验证方法带来的收益是否明显的问题上还在观望。
2）形式化方法还需要和传统的方法相结合才能发挥作用。设计和验证方法的进步应当是渐进的，不可能革命性的改变。因此在可以预见的几年内，混合验证方法应当成为主流的验证方法。断言对于表示接口限制、设计性质和设计假设都具有很深刻的作用和影响。这些会对发现过去的方法不能发现的设计错误做出贡献。特别适合测试覆盖结合起来可以极大的改进验证效率。
3）基于断言的验证是结合形式化验证和传统的模拟验证可行的途径［5］。支持这种途径的统一的设计和验证语言是SystemVerilog。他是在新的Verilog语言标准上扩充系统描述构件而开发的一种过渡性的系统级设计语言。该语言可以统一的描述复杂的设计和测试方案（ testbenches）。SystemVerilog支持多级接口设计和断言，充分利用了当前的设计验证技术和实践。他后向兼容verilog,具有继承性，与其同时成为一个结合设计和验证的语言。该语言已经得到很多EDA厂商和用户的支持，预计将会流行起来。
本文关键字：暂无联系方式综合-其它，单片机-工控设备 - 综合-其它
