正式的抽象和覆盖

在过去的三年里,Oski技术促进了聚会的形式验证专家在餐桌上讨论问题和他们面临的问题。他们讨论技术他们一直试图与正式的验证技术,以及他们已经实现的结果。

半导体工程有记录,谈话和凝结成要点。以前的峰会是在这些故事报告:可以正式取代模拟?和一个正式的转换。

为了促进自由交谈,参与者,下面列出,要求直接引用。所以所有的评论都转述,匿名的。

Kamal Sekhon Oski形式验证工程师,拉开了晚会。她谈到了他们做的可替代的工作。可替代的是网络创业团队成员更熟悉的空间模拟不是正式的。Oski说服他们考虑一块形式验证。虽然一开始不情愿,他们同意了,但继续使用模拟正式的验证已经完成后。

Sekhon描述策略用于验证和得出结论,正式在设计发现23个bug。到目前为止,他们没有发现虫子从模拟,除了一个意外了。它被正式回归套件。集成块时,模拟出现一个错误。这是一个情况的验证块过度约束基于软件用例并不完全理解。

该集团有足够的问题基于使用正式与节省的时间。Sekhon说不可能提供这个信息,鉴于传统的方法没有并行运行,但指出正式验证了大约5周。她估计与仿真已经三个月。

使用正式的发现
验证方法的一个关键方面是创造一个正式的参考模型。Vigyan Singhal首席Oski解释道,这非常类似于一个创建模拟,只是以不同的方式来实现。”断言你所能做的就是找到当地的bug。目标是找到所有的虫子。”

这种方法的一个主要区别是如何发现bug。与模拟,发现一个bug。它必须是调试固定,然后模拟重复。正式发现许多错误的同时,据报道,这是很多更有效的过程。

可替代的是没有准备好考虑基于正式签收。问题的一部分是,下游仍执行验证。“你不能做基于签收RTL模拟。您需要知道库将被使用,合成它和注释,然后再次运行仿真,确保时间限制都是正确的。鉴于仍将需要签收,你能依靠正式的功能验证吗?”

另一个人评论一个次要优势相关的创建正式的参考模型。“通常没有好规格,或者你可能会试图找出规范。有漏洞,我们发现最近在建筑层面涉及安全我们甚至不认为测试。正式的可以帮助我们发现那些。”

模型的连续性
模型的连续性是很重要的。“当你开发一个模型,你想要的概念模型继续一直到实现,”一位参与者说。“许多公司想出一个办法。他们可能会形成不同的模型然后寻找方法来验证信件。有问题的方法。首先,这些模型在不同的水平,这是一个抽象的差距。通常是一个艰巨的挑战,因为事务的差异。第二,当你沿着链,你可能想要使用相同的模型RTL验证。如果你最终创建模型在低水平的抽象你失去快速验证的好处。每个公司考虑如何保持连续性。 Some are successful, other give up. Other just do some analysis using the model and then expect the downstream folks to follow. Maybe there are ways around formal to abstract the core essence of the architectural model.”

讨论了语言和质疑如果任何语言或形式主义能够描述的一切。在出席者评论:

• “验证的东西,你必须先指定它精确。”
• ”在C或c++可以描述所有的东西,但更多的领域特定语言会帮助很多,就像SystemVerilog帮助核查。更好的架构建模语言是什么?”
• “不同的问题需要不同的形式。如果你是记忆行为建模合金从麻省理工学院(MIT)可能是合适的。问题是一旦形势变得更加复杂,你要把更多的心思,但是合金使他们能够创建操作规范。”
• 不同的公司也有不同的侧重点。“我们的架构团队建模团队和他们一起工作。一般来说,他们关注性能和一些权衡,如功率、性能和面积(PPA)。我让datapath公司有多宽?建筑功能,如吞吐量和带宽,交易与力量。建模团队擅长处理,但他们并没有有效地建模其他系统级特征,如没有死锁,安全问题,缓存一致性和安全性。正式可以真正帮助。今天他们编写C模型和仿真运行,但这提供了与直接测试覆盖率非常低。”
• “性能模型通常基于队列或者随机模型。我们不走这条路,我们需要看活锁、死锁和你需要一个不同的形式。”
  另一家公司有一个非常不同的范围。“固件认证对我们来说是一个非常重要的问题。你如何保证一个恶意的设备驱动程序不能加载坏固件吗?它涉及许多IPs SoC。我们开始建模,几年前,发现了一些严重的错误。”
• 虽然形式是好的,有一个更大的问题。“最困难的部分是获得动力学和相关工具。我不认为语言真的很重要。什么是有趣的架构建模是找出协议。不考虑设计协议,然后实现它。相反,打开当你正式的设计。它提供了很多见解,您可能的性能问题。用它来设计协议更有趣,和验证是免费的。”
• 另一个人建议使用Verilog。“最终你想链接的实现。利用周围的基础设施行业标准工具,包括调试。最终你需要测试所有的假设在建筑层面实现。”
• 抽象的差距仍然存在。“你必须放一些想法。可能有决策点的RTL不能捕获在更高层次的事件时间,所以你作弊通过内部监控特定信号提供一个提示。经常提供足够。”

形式化的行为常常冲出来的许多问题。随着时间的推移模型可以精炼。

报道
新兴的便携式刺激(PS)标准。“PS被定义为动态验证人,因此潜在的重叠与正式的没有被最大化,”一位与会者说。大多数的参与者不熟悉细节关于这个标准或正式的方式可能会受到影响。很明显,从输出到输入PS是基于路径,这非常类似于正式的。

迅速移动到一个主题报道合并的结果动态和正式的验证:

•“你写一个测试规划因为它定义了什么,而不是如何。然后你决定如何检查每个行项目的正式测试规划,问如果你可以检查它。到目前为止,测试规划是由动态模拟。我们少了什么没有正式开的吗?我可以写一个检查程序因为这是测试规划的一部分?如果我可以写一个正式检查,如果可达性并不是一个问题,那么我可以正式目标。”

•“可达性之外,我们有一个计划进行动态模拟,coverage-driven跳棋等等,但是我们有一些具体形式。有一个分离。尽管我们尝试所有的断言在模拟和正式运行,我们当他们特定于正式的分化。不同的编码规则适用。”

•“你可以有一个计划,混合许多策略和技术或引擎。关闭,你必须合并从不同来源的报道。如果你的目标特性设计不同的引擎,你怎么结合报道?”

•“今天,它是独立的。你模拟和检查功能覆盖率。正式独立。我们可以将它们合并只有我们使用相同的工具供应商。所以,这有点手册。你已经从仿真和功能覆盖率有正式的报道,但他们在一起的计划。”

•一个项目。“许多断言需要模拟运行几周,我们没有使用模拟在这个项目。正式替代模拟。这是白盒测试。模拟的测试规划本质上是黑盒。我们深入了解微体系结构,然后真的深,跟设计师和添加断言——专门为正式。当我们做报告,有手动合并。”

参与者谈到断言覆盖从模拟和正式的方式是不同的,运行的价值主张在正式的模拟已经证明。

ProofCore
覆盖问题已经正式关闭。即使每一个属性都证明,你足够的属性定义吗?“ProofCore的概念是,你有一个设计和一个检查列表,”一位与会人士指出。“部分的逻辑必须包括证明的正确性检查吗?如果有部分中使用的逻辑,没有证据,你没有足够的跳棋。”

这个指标的价值,就像任何指标,发现的漏洞。当它说什么了这意味着还没有测试,但是如果覆盖,然后给你一个好的感觉,但它并不能保证任何事情。

相比之下积极影响锥(CoI)的分析。“COI是非常简单的,因为它是结构性的,”一位与会者说。“多少结构球迷的断言。这是非常乐观。ProofCore走远。正式引擎抽象提炼,他们把一些逻辑,一次一点,试着证明财产的小锥逻辑没有任何约束的输入锥的逻辑。当这变成可能,你做的。它不再重要的逻辑是什么意思。你知道没有违反逻辑属性在任何情况下。如果它失败了,那么你需要吸引更多的逻辑来限制输入。 As you pull in more logic – eventually you will get a proof – so how much logic of the design did you use to get the proof? Anything outside of that is untested.”

参与者包括Da壮族和Anatoli Sokhatski,思科;英伟达Ambar Sarkar;是一家Dhruv和剑王,AMD;萨瓦河不绝如缕,英特尔;•卡迈勒Belhous Teradyne;翟Kosaraju,可替代的。罗布·范Blommestein Oski关系人包括随时Vigyan Singhal,戴夫•帕里罗杰Sabbagh Kamal Sekhon。