添加顺序和结构验证

你不能改善无法测量,当谈到方法测量的概念变得更加困难。添加的概念技能,能力和经验水平的个人在一个组织中,采用特定的技术,这可能影响他们的能力,它需要相当大的关注。

这就是能力成熟度模型(机)等概念。CMM允许公司评估,他们站在技能和能力方面比其他公司在一个行业,并识别领域中,他们可以优化他们的流程从他们的工程团队获得更多的价值。它还可以定义风险水平与引入新技术方法。

几年来,威尔逊研究进行了一项调查,代表导师,西门子业务,以评估的成熟行业的各个方面功能验证。对于任何调查,趋势时才可以看到问题在调查中保持不变。添加新问题或修改现有的,紊乱的结果,因此它需要一段时间才能看到这些新趋势。此项调查开展以来的一个领域,改变了显著的状态形式验证(见图1)。

图1所示。正式的验证技术的增长。来源:导师,西门子的业务。

形式验证已经从一种技术,要求博士理解和操作技术可以更广泛的观众。同时添加了额外的调查问题,他们缺乏深度和结构调查的其他部分。例如,调查结果包括应用程序SoC集成连接和X语义安全检查但不包括clock-domain穿越。调查还说什么如何有效的特定的技术,例如assertion-based验证(酒精),是如何被利用的。

了解该行业的第一步是今天,所以进展可以被追踪到,就是建立一个成熟度模型。Oski技术所做的,它发布了第一个版本今年早些时候一群业内专家。半导体工程受邀揭幕。为了促进自由讨论,所有匿名评论,蒸馏的主要参与者的想法。在讨论韦恩Yun,AMD;Ram纳,手臂;Sanjay DeshpandeArteris IP;布赖恩•莫里斯Ciena;Anatoli Sokhatski,思科;迈克尔•西奥博尔德DE Shaw的研究;阿德里亚娜马焦雷谷歌;埃里克•塞利格曼英特尔;Aniket Ponkshe,赛灵思公司。从Oski:克雷格•雪莉Vigyan Singhal, Ninad Vartak,罗杰·尼科尔斯Sabbagh和格洛丽亚LaunchM。

正式的影响
有几种方法,正式的技术能有多大的冲击,但是每个理由都是不同的。最初与这些传统是很重要的模拟的验证流程,这样的好处可以评估。

图2所示。正式影响基于仿真的流。来源:Oski技术。

许多公司看向正式解决模拟的弱点。说:“人们把这些曲线模拟克雷格•雪莉Oski总裁兼首席执行官。“也许他们画这些曲线模拟,但他们不给正式画这些曲线。正式往往显示一点好处或小凹凸的曲线,但它是可有可无的功能在某些领域。今晚,我们将画一条曲线,显示了芯片级各种形式验证方法的影响。”

图2中的红色区域显示模拟弱的地方。就是这样一个领域testbench的战略趋势渐近水平,使团队很难改善报道。有时这是由于极长时间运行时必要公开这些bug。模拟有助于减少这些运行时,然后提出额外testbench困难。

“好消息是,90%或更多的这些错误是块级错误,”雪莉。“他们不是系统级错误。我们不断地问别人有多少块修复这些错误进行修改?它几乎总是。所以我们仍然做块级验证,即使我们称之为系统级。他们往往是高度并行的角落案件。”

这意味着提升空间块级验证,与先进的正式方法和一个趋势是推动正式签字高风险的街区。

另一图2中红色区域是与时间相关的第一个错误。开发基于仿真的testbenches需要很长时间,这意味着很多RTL编码完成第一个测试之前已经准备好了。“当你开始使用正式的早期,工程师经常发现错误错误创建2或3天后,”雪莉。“RTL仍记忆犹新。他们不需要从一些其他项目的上下文切换。另一个好处是,设计师可能有点更激进的如果他们知道会发现错误更快,及其修复验证详尽。也许他们现在有更多的带宽和bug修复bug,因为他们不是淹没。的许多错误,你发现可能会发现在simulation-eventually-but你正在寻找他们。”

一位与会者有一个有趣的观点。“左移位对许多人意味着什么是怎么去质量周期最快的。多久我们可以运行在一个模拟器或FPGA吗?它不仅仅是第一个bug。对我来说,时间最后的错误比左移位更有吸引力。”

正式的水平
正式的正式CMM定义五个层次方法可以应用。所有五个层次是有用的,但目标,培训和工具要求每一层都是不同的。在讨论中,很明显,将来可以添加额外的水平,但是这代表了行业发展的现状。

图3所示。正式的应用程序的水平。来源:Oski技术。

应用工程副总裁罗杰Sabbagh Oski,描述如图3所示。“我们从1级开始,人们使用之类的东西产品毛羽。这是非常基本的。自动正式检查,重点是小,具体问题。你可能会寻找一个内存地址的范围。用户甚至不知道他们正在运行一个正式的工具。没有断言需要写。执行是无痛的。

“二级介绍了正式应用。这就是用户指定一些关于他们的设计意图,也许在一个电子表格。例如,他们可能捕获所有的连接设计,或不同类型的寄存器和行为与这些寄存器相关联。该工具生成必要的断言。他们可能需要应用一些约束接口的设计,但它仍然是相对容易采用因为用户没有写任何的断言。例子是连通性检查,时钟门控和连续的等价性检查。

“三级是人们开始有针对性的写断言分布在整个设计。他们可能是当地的断言,写的RTL设计师,如总线是一个炎热的总线。他们可能目标控制逻辑,比如仲裁者和FIFO控制器或接口。验证工程师可以将断言添加到设计,加上他们可以使用断言贵宾,这可能检查标准接口协议。你正式运行在这些断言以及在仿真运行他们。”

与水平相关联的大多数工具类的一个通过三个落入转变left-finding虫子比可能使用模拟。在讨论,指出,这些工具还发现bug,很难发现在模拟,如clock-domain路口,或者可能需要很长时间的模拟,如连通性检查。

“四级是我们开始取代模拟块级验证,“Sabbagh说。“我们的目标是与正式签署街区的功能验证。这意味着开发变化类型的属性。他们成为当地跳棋的端到端跳棋相反。正式的签字可以处理一些复杂的块。例子包括加载/存储单元的CPU、GPU的经纱音序器,多端口网络设备缓冲区管理器,一个多车道对准器作为PCIe接收机或MAC层块接收路径的无线接口控制器。

“5级基于四级。我们开始做建筑形式验证,解决一些系统级的要求,否则会很难验证。我们可以证明跨多个异构cpu使用不同的缓存一致性协议。同样解决死锁,可能需要运行完整的软件栈来展示这个问题。”

水平1到3在很大程度上是通过工具和语言加以解决,但有一个3级和4级之间的鸿沟。四级需要更多的贡献从方法和更多的用户的技能。在这一点上,周围几个讨论了覆盖收敛的概念和技能组合包含在公司。协议的一个领域,任何公司试图水平4或5可能雇佣全职正式验证工程师。

四级技能需要一个飞跃,但这也带来了不同的风险/回报水平。一位与会者说,“如果你想让你的经理在正式的投资,它可能更容易在四级进来,因为正式取代模拟。在较低的水平,当一个经理问什么是模拟避免或资金将如何得救,你的回答是,你还有他们所有人。四级是对管理者更具吸引力。但是,我不建议人们从四级开始,因为它是一个非常危险的事情,你可以进入很多麻烦。”

协议的另一个区域的粘性的水平。“水平1和2往往是非常棘手的。3级变化每级设计和为每个项目4是完全不同的。低层次包含的东西,可能是也可能不是对每一个设计有用。但是当你做一些工作,然后经理往往是快乐,并希望你重复它。”

正式的功能
某些技能需要支持的各种组织的水平。这基本上是分为四个Cs(检查、约束、覆盖范围和复杂性)。是太多的覆盖所有的细节包含在图4中,或者是详细的分析每个技能的类型,所以只有那些生成的讨论爆发。

图4所示。形式验证工程技能矩阵。来源:Oski技术。

ProofCore覆盖的适用性进行了讨论。ProofCore是一个可观测性覆盖指标,可以用来确保检查程序设置完成,所有行为的设计。它实际上决定了如果一个逻辑为证明检查器。如果逻辑修改,没有检查失败,那么它不是真正使用的证据。这是类似的突变分析概念,需要这一步。

一个评论指出“ProofCore取决于跳棋是如何写的,这样如果有一个根本的弱点你的断言,你可能只发现与突变分析的弱点。”

另一个说“突变涵盖了不同的区域,这是最重要的一个角色验证工程师,设计意识。有一个元素的规划,不是这里,和理解设计的一部分,复杂性的来源,了解如何有效地分解成单个的功能检查和验证计划策略。”

突变分析的问题是,它是计算重。然而,与会者仍然认为它包含值。“如果你看看模拟,我们报道了刺激,但是我们没有覆盖检查器。突变分析填补了这个空白。这使它非常重要。计算power-yes而言,它是昂贵的。”

“有时候有一种人们忘了启用断言。有时一个检验员,有时他们只是禁用一些测试。可能有一个脚本的问题,剩下的东西。”

报道时发展成了一个热门话题4和5的水平。一位与会者说,“作为一名经理,没有正式的指标是足够签字。我舒适的跳过模拟,但是我想看到在FPGA或仿真系统运行表明,它实际上通过测试你申请和周期的数量让我舒服。我担心我们可能将覆盖度量的设计师和验证人很渴望请管理,他们会很高兴,图表显示我们覆盖率达到100%,但实际上他们并不知道他们错过了一些关键性的东西。我有意识的人们远离移动正式报道尽我所能。”

这不仅仅表达技能水平,但团队的成熟度。流程可以是到位的,但如果盲目跟随,或如果人们寻找捷径没有理解为什么他们存在,那么他们可能会导致失败。“如果流程没有意义,那么您需要一种方法来修改它。这是一个过程,控制的过程。”

中缺少了一种技术,与会者觉得正式CMM是设计评审。这些也与技巧和成熟度级别。“这是真正的函数有多少信任验证工程师与设计师。如果你被视为一个人会用很简单的问题,你可能会发现,这是不太可能你会得到很多的参与。”

“当我做我自己,我没有任何保险措施,所以这是一个演示通过审查过程的充分性。我不得不让它尽可能简单回顾。信托进来后我们看到这些单位工作。我看不到出路的评论。”

另一个缺失的元素被这一组辅助属性。这些属性被用作假设和可以帮助降低状态空间或证明收敛更快。

管理和个人
每个组织都有哪些工作水平提供最大的价值。它不是一个种族到达5级。“我不认为5级更划算。我认为5级是更多的爆炸和美元。需要更多的努力和更多的钱。1级也可以非常高的货真价实,因为努力是如此之低。”

与会者质疑这个与个人技能水平和组织成熟度级别。“这确实是一个工程技能矩阵,并组织成熟度与检查。你检查器级别的野心是什么?那是你组织成熟。”

一切开始于个人技能。“我们设想耦合这个技能矩阵与调查这样一个工程师可以品位,“Sabbagh说。“这让人们意识到他们是在比是可能的和正式的,有多少不同的技能。接下来我应该学习什么?你可以使用这个年级调查方法在每个轴,计算平均分数。“一个例子如图5所示。

图5所示。工程技能分级图示例。来源:Oski技术。

从概念上讲,你必须能够从人们技能组织的成熟度。“应该在这里的东西验证计划。它是一项关键的技能。决定如何处理正式是非常不同的知道如何去做。”

参与者同意了。“这谈论个人工程师,也许我们需要考虑经理。如何决定做哪块的方法,如何分配,如何衡量当你完成。”

“一个组织需要看看他们最大的难点。技能涉及到个人和组织中谈到你的能力。”

一位与会者建议这种方法:“你回举行前一个项目吗?未来你将适用什么补救措施和如何正式发挥作用。然后选择你将资源和问题需要什么样的技能,所以你实际上上下通过图表。”

正式和混合仿真
仿真和正式如何一起工作解决验证的挑战?许多团队面临这种困境。“这从组织变化很多,“Vigyan Singhal说。“我们故意试图远离,因为它可以成为宗教。有一些组织认为正式和模拟之间有严格的墙和其他地方,他们希望合作从一开始,他们想与对方交换错误。”

参与者也觉得比模拟仿真可以发挥明显不同的作用。“模拟的力量是要找到硬件/软件错误而不是块级错误。”

最初的反应
它可以花时间一个新概念,成为接受,和最初的反应可以理解不一。“这是一个好的开始。我们已经看到使用这种事情不可思议的结果。正式的工程师可以看看他们所需要的新技能。”

“我有点怀疑。好像你试图强加严格的线性顺序的事情并不是线性的。根据你的问题,它可能并不总是需要从3到4。也许他们应该ABCD。”

无论多么熟练或成熟的一个组织,问题将继续存在。“如果你所有的工程师在5级,你仍然局限于你能想到的东西。我害怕的是我们发现我们没有想到的。你可以三倍或四倍资源项目,仍然没有发现他们。我不认为很好地回答了这个问题。”