路科验证(Rocker IC)专注于验证系统思想和前沿工程资讯,拥有一支活跃的技术原创团队,著有《芯片验证漫游指南》一书,致力为高校微电子相关专业学生与IC从业人员提供技术食粮。 您可以在手机移动端同步关注微信订阅号“路科验证”或是登录网页www.rockeric.com了解更多资讯。如果您需要联系我们,请发送邮件至 rocker.ic@vip.163.com 。

逃逸的漏洞(续)

上一篇 / 下一篇  2018-12-01 22:39:40 / 个人分类:验证前沿资讯

利用形式验证技术

形式验证就是为应对这一挑战而发展的一个领域。NetspeedRamanujam说:早在系统更加简单的时候,模拟足以探索空间并找到漏洞。然后人们意识到规模变得越来越大,需要仿真帮助运行更多的周期。然后系统变得更大,使得人们走向形式验证,用来更准确地证明RTL代码是按照功能描述文档去实现的


形式验证还适用于不同类型的问题。Ramanujam补充道:  “许多客户说他们曾遇到死锁。死锁意味着你被阻塞了,因为规模太大,几乎不可能没有死锁,特别是在进行涉及到多次仿真穷举的测试。你可能到最后也不知道是否已经触发了每个场景,而形式验证能使工作变得更加容易。


还有其他类型的漏洞更适合形式验证OneSpinAnderson说:资源死锁,系统挂起或安全性受损等等。只有形式技术可以在硅前验证中预先发现异常漏洞。通过针对指定预期行为的一组断言详尽地分析芯片设计,形式验证可以设置每个可能的边界情况来纠错。当分析不再发现漏洞时,形式工具可以证明不存在进一步的漏洞。这样的确定性是无法通过仿真,仿真甚至在实验室测试芯片来获得的。


但形式验证也有缺点。Gandhi说。形式验证理论上可以找到所有可能的漏洞,但可能需要更多时间。形式验证可以用于单元级,但通常不能用在更大的块上。因为找出漏洞的深度难度大,耗时长。我们今天能做的是使用代表RTL的模型。在这些模型中,我们可以抽象出很多导致深度问题的事情。这可以减少验证体系结构所需的时间。我们也在小层次上使用形式验证,例如避免死锁等方面。形式验证更适合这些任务。

 

添加可移植刺激
Accellera
刚刚发布了可移植激励标准Portable Stimulus StandardPSS1.0Foster说:新的可移植激励标准也可以帮助发现异常漏洞。例如,我们已经将分类机器学习应用于PSS基于图形的技术工具,以定位尚未验证的场景。与传统的约束随机模拟相比,该技术在覆盖率领域更高效。我们还通过收集和关联事务级活动来表征性能参数,应用数据挖掘技术将Portable Stimulus的应用扩展到验证之外。例如,光纤路由效率和带宽,系统级延迟,高速缓存一致性,仲裁效率,无序执行,甚至操作码性能。找到异常漏洞的关键是需要在设计和输入之间进行充分的交叉探索。这就是约束随机、形式技术和基于PSS基于图形的智能激励可以提供帮助的地方。


PSS还将在系统级验证创建更复杂的测试。Cadence产品管理和营销总监Larry Melling说:发现和隔离一个bug,仍然很难理解和创建一个修复它并将其添加到回归套件中的可以实际调试的测试,使其不再发生的方法。我们正在探讨通过许多处理器同时进行操作,以迫使总线触发这些时序问题。这不是一种普遍适用的方法和途径,但许多人希望用这项技术看是否能够改善现状。

 

Bug逃走了

即使增加了新的工具和技术,漏洞也会逃脱。Gandhi说:当你看到一个漏洞,尤其是硅片级时,你并不知道它是否真的是一种漏洞。你必须设法找到现象的原因。芯片内部应该有一些额外的功能,例如扫描链、从芯片内部的重要结构读取数据的方法、跟踪调试或性能监视器等等。利用这些信息,就可以尝试找出是否存在漏洞。


片上调试和理解将变得更加重要。McDermott说:众所周知,我们的设备配有多个处理器,因此可以在现场使用处理器来帮助查看情况。你需要了解内部总线上的数据流动。如果发生的事件可能与你尝试查找漏洞的区域无关,则数据流动是必须注意的因素。虚拟平台和真实硬件等多种方法可以查看。


海森堡的不确定性原理可以在追踪时间方面的问题时发挥作用UltraSoC首席执行官RupertBaines说:你必须全速运行。因为系统级问题偶尔会出现,速度也十分重要。片上检测可以提供与位和字节无关的抽象,它不是关于JTAG消息传递,而是提供系统级视图。可以识别协议性能,事务级统计性能并帮助识别异常。一旦知道问题所在区域,你就可以到更低层次放大细节。


隔离一个bug后,你需要修复它。Gandhi说。一旦找到它,就要尝试找到解决方法。可以用软件或硬件的解决方法,例如校验位,或稍稍改变做法,例如添加少量时间。虽然这可能会影响功能或性能,但在许多情况下可以忽略。


要求产品可以更新。这是人们特别为物联网采用的新型软件开发,”McDermott说。过去,'制造产品-严格测试-上市-完成'的模式不再适用,不过持续更新是现在物联网嵌入式产品的标准。


自动化正在加入需求。Foster补充说:产品中设计的检测和纠正机制将取决于系统故障(例如在功能验证期间从未发现的边界情况)或随机硬件故障的安全影响。但目标并不是真正发现异常值本身,而是要发现一个会影响安全目标的故障。


并且因为有最小的几何尺寸,芯片也可能需要检测瞬态漏洞Anderson指出:当一个alpha粒子翻转一个存储位,芯片必须能够检测到并可能纠正这个漏洞。形式工具可以考虑一系列可能的故障,包括瞬态和永久性故障,并分析它们对设计的影响。


可以更新硬件的系统越来越多了。Sherer说:目前,更新的最先是固件,但它也可能是FPGA更新,然后是硬件更新。日益增加的复杂性需要一个解决方案。


机器学习增加了另一层复杂性。Ramanujam补充道:通过机器学习可以验证系统及其工作方式。但如果它有一个学习神经网络怎么办?现在的系统可能不会像过去那样对给定的刺激做出反应。你如何验证正在学习的系统?


这就需要一些新功能。他说: “你所描述的是一个系统在某一系列操作条件下出现故障。在可调试的工具集中重现整个环境并不像重新运行测试那么简单。因为调试依赖于学习状态,我们需要将系统状态加载到可调试环境中。然后这就变成了一个安全问题。


结论

验证的性质已发生变化,并将持续变化。Singhal说: “传统方法适用于顺序块,但大环境已发生改变,验证也要重新启动。取回硅片后再想怎么做?那就太晚了。你必须以不同的方式计划验证。


Singhal建议你从设计过程开始。当你构建设计或对块和微体系结构做出决策时,必须将并发性与顺序性作为第一决策点。

7U[S`8VG8F70$__4E)0G42N

7U[S`8VG8F70$__4E)0G42N

TAG:

 

评分:0

我来说两句

显示全部

:loveliness: :handshake :victory: :funk: :time: :kiss: :call: :hug: :lol :'( :Q :L ;P :$ :P :o :@ :D :( :)

路科验证

路科验证

路科验证(Rocker IC)专注于验证系统思想和前沿工程资讯,拥有一支活跃的技术原创团队,为高校微电子相关专业学生与IC从业人员提供技术食粮。 您可以在手机移动端同步关注微信订阅号“路科验证”。如果您需要联系我们,请发送邮件至 rocker.ic@vip.163.com 。

日历

« 2018-12-18  
      1
2345678
9101112131415
16171819202122
23242526272829
3031     

数据统计

  • 访问量: 201510
  • 日志数: 268
  • 建立时间: 2016-06-25
  • 更新时间: 2018-12-09

RSS订阅

Open Toolbar
博评网