形式化能力
某些特定技能是被需要用以支持各个组织级别。 基本上将其分为四个C（检查，约束，覆盖率和复杂性）。 覆盖图4中包含的所有细节或对每种技能类型的详细分析过于繁琐，因此仅分解那些展开讨论的内容。
图4. 形式化验证工程师技能矩阵。 资料来源：Oski Technology
这里先讨论ProofCore覆盖范围的适用性。 ProofCore是一种可观察的覆盖率指标，可用于确保检查集的完整且涵盖了设计的所有行为。它确定逻辑是否实际送入与检查程序关联的证明中。如果修改了逻辑并且检查没有报错，则证明中不会真正使用它。这与突变分析类似，可以进一步进行分析。
一条评论指出“ ProofCore取决于检查程序的编写方式，因此，如果你的断言从根本上存在弱点，则只有通过突变分析才能发现该弱点。”
m
另一位代表说，“突变能涵盖不同的领域，这是验证工程师最重要的角色之一，那就是设计意识。计划的一部分在这里没有显示，其中一部分是了解设计，复杂性的来源，了解如何有效地将功能分解为单个检查程序以及计划验证策略。”
突变分析的问题在于计算量过大。但是，与会者仍然认为它具有价值。“如果你看一下模拟，我们有激励的覆盖率，但并没有检查程序的覆盖率。突变分析填补了这一空白。这使其变得非常重要。就计算能力而言，是的，这很昂贵。”
“有时有人会忘记启用断言。有时是检查程序，有时他们只是禁用了一些测试。脚本可能有问题，有些东西被遗漏了。”
当进入第4级和第5级时，覆盖率成为一个热门话题。一位参与者评论说：“作为经理，形式化指标还不足以满足签核要求的。我可以轻松地跳过仿真，但是我希望看到该系统在FPGA或仿真中运行，以表明它确实通过了你正在应用的测试和周期数，这让我感到很舒服。我担心我们可能会将覆盖率指标交到非常渴望取悦管理人员的设计师和验证人员手中，他们会对图表中显示达到100％覆盖率感到高兴，但实际上他们不知道自己是否已经错过了重要的事情。我有意识地使人们尽可能地远离形式覆盖率。”
这不仅表示技能水平，还表示团队的成熟度。可以部署流程，但是如果盲目地遵循流程，或者如果人们在其中寻找捷径而又不知道它们为什么存在，那么它们可能导致失败。 “如果该过程没有意义，那么你需要一种方法来对其进行修改。因此，存在一个控制该过程的过程。”
与会者认为形式化CMM中缺少的一种技术是设计审查。这些也与技能和成熟度水平相关。“实际上，这取决于验证工程师在设计人员中赢得了多少信任。如果你被视为一个提出非常简单的问题的人，这些问题本来可以自己解决的，那么你参与其中的可能性就较小。”
“当我自己做时，我没有任何覆盖率的衡量标准，因此这是通过审核过程证明的充分性。我不得不让他们尽可能容易地进行审查。我们看到这些环节开始运作后，便产生了信任。我认为没有办法不进行审查。”
该小组确定的另一个缺失要素是助手属性。这些是用作假设的属性，可以帮助减少状态空间或更快地证明收敛。
管理层和个人
每个组织都必须确定哪些级别为他们提供最大的价值。这不是一场为了达到第5级的比赛。“我认为第5级不会带来更多收益。我要说的是，第5级是付出更多收获更多。这需要更多的精力和更多的钱。第1级可以说是物超所值，因为需要付出的努力非常少。”
与会者质疑这与个人技能水平和组织成熟度水平有何关系。 “这实际上是一个工程技能矩阵，组织成熟度与检查人员息息相关。你在检查级别的雄心是什么？那就是你的组织成熟度。”
这一切都从个人技能开始。萨巴格说：“我们设想将这种技能矩阵与调查结合起来，以便工程师可以对自己进行评分。”“这使人们意识到自己所处的水平——用形式化可以做什么，有多少种不同的技能。接下来我应该学什么？您可以使用这种调查方法在每个轴上给自己打分，并计算平均得分。”一个示例如图5所示。
图5. 工程技能等级表实例。 资料来源：Oski Technology
从概念上讲，您必须能够从人际交往能力发展到组织成熟度。“这里应该有验证计划。 这是一项关键技能。 决定用形式化验证做什么比知道怎么去做难得多。”
参加者表示同意。 “这里探讨的是个体工程师，也许我们也需要考虑经理。 如何决定以哪种模块采用哪种方式，如何将其分配给人们，如何衡量完成的时间。”
“组织需要着眼于他们最大的痛点。 该技能组与个人相关，并讨论你在组织中的能力。”
一位参与者提出了这种方法：“是什么让你退回上一个项目？ 今后将采取什么补救措施，以及形式化将在其中扮演什么角色。 然后选择你将在其中应用资源的级别，并询问需要哪些技能，实际上你会在等级表中上下波动。”
混合形式化和仿真验证
仿真和形式化如何共同解决验证难题？ 许多团队一直都面临着这个难题。 Vigyan Singhal说：“各个组织的差异很大。” “我们故意试图远离它，因为它可能成为宗教。 有些组织认为形式化和仿真之间以及其他希望合作的地方之间从一开始就存在严格的隔离墙，他们希望彼此交换发现的错误。”
与会者还认为，仿真与模拟相比可以发挥显着不同的作用。 “模拟的优势在于查找硬件/软件错误，而不是模块级错误。”
初步反应
一个新概念被接受可能需要一些时间，并且可以理解的是，最初的反应是各色混杂的。 “这是一个伟大的开始。 使用这种方法，我们已经看到了惊人的结果。 形式化工程师可以研究他们需要掌握的新技能。”
“我有点怀疑。 似乎你要对非线性的事物施加严格的线性顺序。 根据你的问题，可能不一定总是从3增加到4。也许它们应该是ABCD。”
无论一个组织多么有技能或成熟，问题仍然存在。 “如果你手下所有的工程师都处于5级水平，那么你仍然受限于可以想到的事情。 令我感到害怕的是我们发现的我们没有想到的。 可以在项目上增加三倍或四倍的资源，但仍然找不到它们。 对于这个问题，我想不到很好的答案。”
扫描上图二维码可直达课程页面，马上试听
往期精彩：
路科发布| 稳中带涨！25w成芯片校招薪资平均底！2020应届秋招数据全面分析！
理解UVM-1.2到IEEE1800.2的变化，掌握这3点就够
