ML可以帮助验证吗?也许

功能验证产生了大量的数据，可以用来训练机器学习系统，但并不总是清楚哪些数据有用，或者它是否有帮助。

ML的挑战在于理解何时何地使用它，以及如何将它与其他工具和方法集成。有了一把足够大的锤子，很容易把所有东西都称为钉子，而仅仅用ML解决问题并不一定能解决问题。

斯坦福大学(Stanford University)计算机科学教授克拉克•巴雷特(Clark Barrett)表示:“我看到过很多例子，人们试图用人工智能解决不太适合人工智能的问题。”“就连政府也犯了这个错，说我们会给你钱来解决这个问题，但前提是你使用人工智能。有些事情人工智能真的很擅长，但如果你需要进行精确的推理，如果你需要找到以前从未被发现过的东西——比如以前没人见过的bug——那么也许人工智能就不是适合这项工作的工具。”

机器学习就像后视镜一样，它可以使用过去发现的模式，并将它们应用到当前的问题上。在预测以前从未见过的事物时，它的效率要低得多。那么如何用它来帮助验证问题吗?

IBM研究院(IBM research)研究人员阿维·齐夫(Avi Ziv)表示:“验证正试图对抗机器学习。“验证就是试图制造混乱，制造很多随机性，这让学习变得更加困难。这是您没有看到很多ML对主要方法做出贡献的主要原因之一。如果我们想要实现它，那么我们可能需要一些新的机器学习技术，可能需要改变验证方法，我们如何产生数据以及产生什么数据，以及我们如何将数据输入到机器学习中。”

不过，这并不意味着我们应该放弃。VerifAI首席执行官桑迪普•斯里尼瓦桑表示:“我是一家初创公司的创始人，我有一个大胆的目标，那就是缩短上市时间，并将验证速度加快50%。“如果我们把它看作是把初学者的心态带到一个老问题上，那么有时当你这样做时，就会有巨大的创新。我们已经在机器学习的几个领域看到了这种情况。”

有几个问题可能需要解决，或者验证方面需要改进，但对于微软SoC验证负责人Erik Berg来说，其中一个问题最为突出。“几年来，我一直专注于调试问题，我想知道我们是否应该尝试解决这个问题，或者我们是否可以解决它。无论是谁解决了调试器自动化问题——这对我们来说都是验证中的大奖。”

如果ML只能使用过去来预测未来，那么专注于具有惯性的数据将是有意义的。VerifAI公司的斯里尼瓦桑表示:“旋钮设置是我们看到的显著增长领域。“这不是创造随机性，而是找出输入的显著性，以优化特定的输出。使用强化学习，你会去除一点随机性。通过类似的输入设置，您可以优化覆盖率和bug发现探索等目标。客户表示，它减少了回归时间、模拟时间，并增加了覆盖率。”

不过，这是一个不小的挑战。IBM的Ziv说:“强化学习是一种进行机器学习验证的好方法。“但这并不容易，因为我们追逐的是一个未知的目标。这意味着很难定义代价函数，或者任何我们想优化的函数。成功的一个方面是形式验证在那里你有一堆可用的引擎。ML已经成功地决定了首先尝试哪个引擎来证明或推翻一个属性。”

验证的长尾
虽然这可能是有帮助的，但它并没有真正解决主要问题。斯坦福大学的巴雷特说:“也许你可以减少一些这样的时间，这很好。”“但瓶颈不就是验证的长尾吗?长尾理论指的是那些极其罕见、难以触发的漏洞。我怀疑像机器学习这样的技术是否能找到这些。”

专注于简单的部分是很有诱惑力的。“我同意长尾理论是有趣的部分，”微软的伯格说。“有一部分报道非常容易被击中，我实际上并不太关心它。这是长尾，没有纳入测试计划的情况，没有预料到，没有考虑到，我们没有适当的方法来识别和测量你无法真正预料到的低频事件。关键在于找出量化这些低频事件的代理。”

目前使用的许多优化方法都是基于统计数据的。Ziv说:“统计数据善于观察你的回归正在做什么。“然后你可以识别有效的测试，更多地利用它们，减少工作量，减少机器数量，并提高验证的效率。这些东西不一定是机器学习。”

了解所使用技术的功能和局限性是很重要的。“自动推理是一种你试图证明定理的技术，”巴雷特说。“你在做非常精确的数学分析。这是所有正式引擎和硬件验证的基础。自动推理的好处是你会得到一个是或否的答案。有bug，或者没有bug。有些问题的答案是你想要的。在验证的许多方面，尤其是长尾理论，这是最理想的。现在，在其他问题中，模糊推理已经足够好了，它可以帮助解决更多的问题。在之前的项目中，fuzzer发现的bug比开发人员有时间修复的要多。 They didn’t need the formal hammer. Do we really need the ML hammer? Or should we just use fuzzers to find most of the easy bugs, and then if you really care about the hard bugs, use some kind of formal?”

更重要的是为工具箱创造合适的工具。“我们需要先进的分析技术，无论是机器学习、统计、推理，还是有助于验证的东西，”齐夫说。“人类没有足够的时间和脑力来完成现代设计所需的所有工作。”

选择工具本身就会令人困惑。“你可能永远不会得到一个完全自动的正式解决方案，”巴雷特说。“你可能永远不会得到一个全自动的ML解决方案。但如果你能以一种聪明的方式将所有这些工具组合在一起，也许这就是ML的作用——帮助人类协调这些不同的部分，并知道什么时候使用正确的工具来完成正确的工作。”

尽管如此，数据量和复杂性仍在不断增加。斯里尼瓦桑说:“当有大量数据时，人类很难将累积奖励最大化。这意味着为了实现长期目标而做出不明显的短期决定。强化学习即将到来。它可以帮助我们优化长期决策。并不是说人类做不到，而是数据太多了。”

一些研究人员已经开始研究神经符号计算。巴雷特说:“这是利用机器学习来给你一个形状、模板或其他东西，让你在那里找到一部分。”“然后你想要使用精确的分析来进行实际的验证或检查。例如，如果你正在寻找一个不变量，你可能会使用机器学习来给你一个不变量的模板。然后你可以用一个正式的工具来检验。在那里可以做一些非常有趣的事情。”

有可能从以前的设计中学习吗?“我想你可以，”齐夫说。“通过分析自然语言或设计本身的规范之间的差异，您可以确定哪些地方发生了变化，并在某种程度上至少可以确定设计之间的语义差异。这可以帮助你创建正式的属性，或者调整你的机器学习基础或其他测试平台，以完成他们需要的任何事情。”

但在这一点上并没有普遍的共识。巴雷特说:“我不认为你可以这么做，因为很多房产都是专门设计的，只有设计师知道它们是什么。”“它要求在给予类似刺激时，即使微观结构不同，它也应该表现相似。这可能会帮助我们取得一些进展。”

对调试的关注
调试是最不可预测且花费时间最多的验证部分。

斯里尼瓦桑说:“我们雇佣最聪明的工程师来查看日志文件。”“每周有40,000次失败，使用自然语言处理非结构化日志数据有助于加快调试过程和做出决策。这不是一种灵丹妙药，但如果你从不同类别的角度来看，每一种都有巨大的省钱机会。”

其他人报告了类似的发现。伯格说:“在微软，大约50%的员工都在做调试工作。“部分问题在于绝大多数DV工程师不了解他们如何调试。有人发现调试手册非常有用吗?有很多人在挥手。当你对人们是如何调试的，以及与调试相关的数据有了强烈的感觉，然后通过特性工程过程——然后也许你可以自动化它。调试问题的维度太大了，除非你用一种非常聪明的方法来设计你的功能。你永远无法找到你需要的模式，尤其是在失败非常罕见的情况下。”

有没有中间立场?“调试的艺术是非常困难的，”Ziv说。“但机器学习在很多人认为容易得多的事情上已经失败了，这就是分流。你怎么能把每天晚上成千上万次的失败归结为有共同根本原因的事情呢?找出已经知道的事情并将它们移到一边，然后将新的失败分配给正确的人。机器学习不能提供好的解决方案，不能让人们愿意信任。在开始调试之前，我们需要解决这类问题。”

斯里尼瓦桑说，这可以分为两项任务。“一个是分诊，另一个是集群。集群是指当您有10,000个失败时，您将它们放入10个桶中。然后分类就是把你的bug分类为DV bug或RTL，创建一个机器学习模型，然后预测出现在这些类别中的新bug。我想说的是，这真的很有效。我不知道你为什么会说它不管用。也许在某些特定的情况下，也许你的模型没有正确的功能。或者你的集群有非常高的维度。”

未来路向
也许，如果机器学习在验证方面遇到困难，行业应该考虑如何进行验证，看看是否可以改变。“也许我们需要编写一些不同的测试平台，让机器学习更容易与它们交互，”齐夫说。“也许我们应该改变从设计中获取数据的方式，这样机器学习工具就会更容易使用。Trace不应该是一种自然语言。跟踪数据应该尽可能结构化，因为理解结构化数据要容易得多。由于它是由机器生产的，并将被机器消耗以进行机器学习，这使得双方都更容易工作。验证社区和EDA供应商可以做一些事情来帮助机器学习实现这一目标。但这就足够了吗?我还不确定。我相信在某种程度上，我们会找到如何使用它的正确组合，以及使用哪种机器学习技术，以使它们真正高效。”

这个行业有正确的模式吗?“我们实际上并没有试图开发新模式。我们只是想弄清楚如何利用现有的解决方案。”“如果你让ML的人为狗和猫做一个分类器，他们可以看到他们的工作结果。如果没有我们的输入，他们很难用我们的数据集来帮助他们判断结果。大多数验证人员不能用任何一种算法来描述他们的过程。我们需要了解我们是如何调试的，了解相关的数据，了解我们需要的特性，以便能够更清晰地处理我们提供给ML人员的数据。”

如果这两个组织能走得更近一些，就有可能取得进展。斯里尼瓦桑说:“我希望看到DV工程师和领域专家更多地学习机器学习，而机器学习工程师也能更多地学习DV。”

Berg表示同意。验证工程师需要提高数据意识，以便能够思考我们生成的抵押品如何映射到机器学习模型，或如何被机器学习模型使用。我们不需要验证工程师是ML的人，但我们需要他们精通ML。我们需要更加了解我们所创造的数据，我们所创造的格式，以及我们在运行模拟时如何暴露部分设计。”

最后，这一切可能都需要从一个新的角度来看待。巴雷特说:“有时会有人拿着锤子到处找钉子。”“他们实际上并没有试图解决一个真正的问题。他们只是在寻找任何看起来像问题的东西，他们的锤子会击中。这肯定是人工智能和其他技术的一个问题。我总是告诉我的学生，首先找到一个有趣的问题，并对你要用什么技术来解决它持开放的态度。也许ML起了作用，也许没有。”