自动确定正确的验证策略基于可能带来挑战的设计特点。
老、直观,帕迪Shekhar和Paula Neeley
经过长时间和艰苦的一周,周五晚上,你准备休息和放松的一杯酒,一顿丰盛的晚餐和一个伟大的电影。你打开Netflix和希望,它将不仅对你有很多中肯的建议,但也最合适的一个基于所有的以前的电影和节目观看。毕竟,它是使用机器学习!
机器学习是一个过程,我们今天使用的许多服务,推荐系统像Netflix, YouTube和Spotify;谷歌和百度等搜索引擎;Facebook和Twitter等社交媒体供稿;语音助手Siri和Alexa的例子不胜枚举。在所有这些情况下,每个平台收集尽可能多的数据对你,你喜欢看什么类型,什么你点击链接,等等,并利用机器学习让一个受过高等教育的猜测你可能想要的是什么。当你的机器学习的普遍性让你意识到基本的和直观的过程。找到模式,预测模式,应用模式。
现在,这是不合理的期望上优于半导体设计这样的系统在我们的领域,特别是正式等价性检查?这正是形式等价性检验研发发展。简单地说,我们正在创造一个等价性检查系统,可以从数据做出预测或决策。了解这种学习基础决策过程预计将提供巨大的生产力,我们首先描述当前挑战等价性检验的过程。
Synopsys对此的综合解决方案,设计编译器,编译器NXT和融合提供了一个广泛的优化技术,如以,多位数银行和高级数据路径优化,设计师想利用达到最大QoR。这些优化压力导致“硬验证”等价性检查技术。
努力验证可以发生的原因很多,但他们真的下降的一个关键因素:这两个设计是非常不同的结构相比,尽管他们执行相同的功能。当设计是非常不同的,证明他们的计算成本相当于可以成倍增长。这些巨大差异发生的原因有很多:datapath公司的高级优化表达式;两者之间的不同的运营商架构设计;也不在乎条件参考设计用于积极实现逻辑优化;大型纠错网络创建全球裁员等等。
形式是解决这一问题,多维策略之间的协调:
正式使用拓扑设计参考和实施设计分割成较小的、独立的验证任务。当正式启用分布式处理(DPX),这些任务是派去解决在分布式处理环境中运行。验证是由各种各样的“策略”或配置的解决在实践中已被证明产生更快的验证或允许验证很难得到解决。随着时间的形式开发了大型阿森纳的这些策略应用于静态排序,直到验证逻辑,或形式达到预定的超时限制。
绝大多数的设计,一些策略比其余的和可靠的选择静态排序。然而,困难验证要求替代策略。选择最好的替代策略并不总是显而易见的,和静态排序的一个更严重的问题是错误的策略应用到任何的一部分设计最终被昂贵的性能代价。验证可能运行几个小时,仍然是不确定的。逆也适用:选择正确的策略可能导致第一次巨大的性能提升。
这是形式背后的洞察力的新的机器学习方法在DPX动态策略选择。监督学习模型训练识别特征可能导致困难的设计验证或其他需要使用替代策略。正式的模型提供了建议,可以使用更新的订购策略适用。
正式人员,帕迪Shekhar和Paula Neeley已经确定了一些可能带来挑战验证努力的设计特点。超过30个这样的特点已经被选中,他们继续实验,找到更多。这些特征形成了特性集的模型使用培训。
各种模型进行测试,但该模型最终选择展品最先进的性能、可伸缩性和效率与计算时间和内存资源。当前原型显示近95%精度测试集,和在未来,研究人员在正式将使用客户特定的训练数据,进一步适应策略建议以适应客户的需求。
这是一个非常令人兴奋的时间形式。基于监督学习的方法我们已经投资显示出巨大的成功预测的能力,这意味着我们正坐在门槛向我们的客户提供一些惊人的生产力的运行等价性检查。
让我们明白这一点。设计师使用3理查德·道金斯方逻辑等价性检查工具通常经过多个费力迭代在设置和验证阶段。没有学习型预测方法,他们别无选择,只能尝试不同的解决杂乱的食谱,希望它可以解决验证。但在现实中,这些食谱可能或不可能实现的验证。这段旅程,这需要深厚的专家用户的干预,可以持续数天到数周聚集在一块。
我们听到我们的设计师,在平均项目中,经过约50块合成。他们经常想跑,但限制因素是长或不确定的等价性检查运行的3理查德·道金斯方的工具。因为等价性检查往往成为瓶颈,设计师最终被迫关掉这些工具成功地验证他们的设计优化。
在上面的场景中,工程管理人员可以量化方面的运行时惩罚机小时预算,但这是不可能的评估人的时间和精力专家用户干预取得成功的等价性检查验收。这是一个指标,很难破解,因此他们选择规避风险,最终牺牲QoR目标为了可验证性。
想象现在,正式毫升系统可以基于强大的并行与分布式处理。想象一个系统,可以删除专家用户干预的要求准确地识别正确的配方需要解决这个问题。想象这是开箱即用的,没有设置迭代和验证重启。想象一个系统,可以利用分布式处理的力量,可以扩展到多个工人。想象一下机器和人小时生产率增长。想象一下!
|
|
|
|
|
|
|
|
|
|
留下一个回复