EDN China > 其它文章 > EDA工具与服务 > IC设计与设计服务 > 正文
? 2016博客大赛-不限主题,寻找电子导师,大奖升级??

在设计过程早期发现并解决问题

Gabe Moretti?? EDN技术编辑?? 2004年03月23日 ?? 收藏0

事实:C语言和与之相关的 Unix 操作系统都可以廉价买到,维护费用低,大多数大学都使用它进行编程教学。他们指望大多数电子工程师都在一定程度上熟悉 C 语言。
  遗憾的是,C语言不具备精确描述一个电子产品的结构和健全性,C 语言的派生语言C++ 更适用于软件开发,但很难掌握和使用。如果轻率地使用C++的功能强大结构,可能会导致开发人员难以发现而且要花很高代价才能纠正的错误。SystemC 尝试把某些硬件结构引入C++,如时钟周期和并行性,但仍然无法抓住硬件设计的本质。因此,C++不能帮助设计师,例如,在某一设计部分硬件实现方法和软件实现方法之间做出明确的抉择。使用 SystemC 成功地按时完成设计验证的工程师小组都由高水平的和有经验的工程师组成。如何让普通水平的工程师也能用这一方法还是一个未知数。迄今为止的实验仅仅表明:不管使用什么工具,经验都是无法替代的。
  现在已有更多适用的语言,如 Esterel 技术公司使用的 Esterel。EDAptive 计算公司正在开发基于 Rosetta 语言的工具,而 KeesDA 正在开发基于 B 方法的工具。Esterel、B 和 Rose

tta 都提供定义和规范设计要求与制约因素的健全方法。使用这些工具的工程师发现,设计中出现错误较少,而且很容易获得设计正确性的形式证明。据 Real Intent 公司总裁兼首席执行官 Prakash Narain说,“抽取与分割处理的范例尚未开发用于功能验证。”他指出:“断言和基于特性的规范就是实现抽取与分割处理的最实际的范例,”但是抽取的设计表述则更进一步。Narain 认为,芯片设计工作是一门精确的艺术,将来会出现什么样的抽取和精确的方法尚不清楚。因此,业界仍在努力发现错误——而不是避免错误。
  形式证明
  设计小组把某一项目的计算机时间大部分用于进行逻辑仿真,以便从功能上验证他们的设计。逻辑仿真一直是一种发现设计错误并证明后来的纠正措施是解决问题的最有效方法。有两个因素会对逻辑仿真的效率造成负面影响。仿真就是建立逻辑信号在电路中的传播模型,由此来模拟实际电路的功能。由于电路规模的增长,仿真所需时间以及仿真结果数据库的容量也随之增加。工程师们必须监控更多的逻辑功能,因此他们使用的测试向量数量也大大增加。
  开发测试向量不是一种决定性的技术。一组测试向量的有效性很大程度上取决于验证工程师的直觉和创造力。因此,即使在处理复杂程度一般的电路时,你也决不能断定已经测试了所有可能的错误来源。为应对这一挑战,验证方法已从手工创建测试演进到由制约因素驱动的随机激励生成技术。受约束的随机验证方法可以揭示出那些手工不可能包含的情况,但由于这种方法的随机性,使人们难以判断一个设计是否得到充分验证。
  形式验证试图克服功能验证的不足之处。它不需要测试向量,但一种常用的技术,即半形式验证,则依赖逻辑仿真来建立形式证明的起始状态。形式验证使用数学分析方法来确定电路的状态以及相邻状态之间的关系。这一技术的执行速度高于对电路中所有节点的逻辑状态的计算速度。纯形式验证很难使用,因为它要求工程师以一种适合数学证明的形式把设计表达出来。尽管前述的新兴语言可以支持所需的形式,但为大量工程师进行培训和更换工具的费用正在减缓它们被接受的进程。因此,形式验证方法往往要求工程师把电路分割成较小的模块,用断言或对设计特性进行定义的方法来引导证明引擎。
  许多形式验证方法的厂商都支持基于断言的验证。这种验证能在设计中提供断言和覆盖点,从而加大实现覆盖范围,而断言和覆盖点又反过来改进可观测性,为仿真和形式验证提供覆盖范围反馈,并使用自动化的形式分析工具来加大验证的覆盖范围。0-In 设计自动化公司的首席设计师Richard Ho指出,仲裁逻辑是适合基于断言的验证方法的一个电路实例。他说,你把具有断言或验证 IP(知识产权,如 0-In 的CheckerWare)的这一“验证热点”作为目标,然后用完整的形式验证工具对其进行完整的证明。据 Ho 说,这种方法可以提供对仲裁逻辑的全面覆盖,从而免去了数百万个周期的冗长的重复仿真过程。
  Cadence 公司和 Synopsys 公司都提供兼有功能验证和形式验证两种技术来验证一项设计的验证系统。Hybrid RTL 形式验证用形式验证技术来驱动内置的仿真引擎,并证明引擎则不断地执行形式分析,以验证设计是否满足某一额定的特性。它提供的是没有假性错误(即由于芯片实际运行时永远不会发生的状况所导致的错误)的确定性结果。
  形式证明引擎具有其固有的局限性,使大多数形式工具的范围缩小到常常以 RTL 代码嵌入的实现方法所特有的断言。Jasper 设计自动化公司提供一种块级的纯形式验证产品,它运行在基于断言验证的最高级别(规范级),可提供端到端的特性,用以验证一个


?? ?? ??


打开微信“扫一扫”,打开网页后点击屏幕右上角分享按钮

1.扫描左侧二维码
2.点击右上角的分享按钮
3.选择分享给朋友
?? ??

设计? EDA? 电路板?

相关文章

我来评论
美国的游客
美国的游客 ??? (您将以游客身份发表,请登录 | 注册)
?
有问题请反馈