正式你了吗?

在第一部分圆桌会议,小组成员讨论了最近的变化,带来了正式的验证和讨论正式UVM带来的挑战。在这部分,我们开始探索这些困难所取得的进展和详细综合报道。参与小组皮特荷迪,在节奏敏锐的正式产品管理总监;盎司Levia,营销和业务发展副总裁碧玉设计自动化,这是通过节奏;在真正的意图Pranav莎,首席技术官;营销总监戴夫•Kelf OneSpin解决方案;首席执行官和Vigyan Singhal Oski技术。以下是摘录的讨论。

SE:让我们继续谈论断言的一代。断言是从哪里来的?

莎:我们谈论断言为疾控中心,自动生成能力,时间限制。有抵押品信息在RTL以外的东西。例如你有趟车,这可以开采的信息用于创建断言。UVM添加testbench抵押品,可以我和生成功能检查。

荷迪:但是UVM建造的吗?

莎:没有,但没有署或UPF值建立的目的。

Levia:UPF值是建立专门为权力的规范域,和IP-XACT建于定义接口的概念,和SystemVerilog建于模拟。他们甚至没有合成。有类型的属性,甚至不使用SystemVerilog。但这是阻碍发展的正式吗?不。人们找到办法的。有一些方法可以提取所有这些形式的断言。UVM不是一个障碍,但它不是帮助。

SE:我们与覆盖率和特别正式的报道?

Levia:报道有点棘手。我们有一个标准,但大型模拟供应商给的支持这是狭隘的。这是不幸的。值得庆幸的是,还有其他的方法整合报道的结果。我们可以谈论覆盖以几种不同的方式。一种方法是告诉用户关于testbench的质量。状态空间和锥的多少影响。这也适用于约束和有很多方法,我们可以显示用户,他可能要仔细看看。然后是覆盖率分析基于完整的证明。在这里,正式的远比模拟更全面。 With a full proof you can say something definitive about the coverage of the state space. What is perhaps more interesting is how you apply information that comes from bounded proofs. There are ways that we can show the user the difference between the relative bound and the theoretical bound. This can be used to assist the user in breaking up a big problem into several smaller ones that can converge into coverage. Lastly we have to work out how to integrate this will the coverage information they have coming from other sources, other companies, other tools.

莎:正式的社区已经过于关注证明属性,并通过这样做,他们没有意识到有如此多的中间结果中的信息可以提供给用户有一个更好的把握报道。从有界的结果生成的信息是非常重要的,不利用这个我们错过一些低挂水果。

Kelf:到目前为止,我们一直谈论的控制范围。我们到达了正确的部分设计?很重要,但是我们也要问,有足够的断言被写封面设计正常吗?如果一个问题存在于设计,会发现的断言?我们需要添加这种类型的覆盖一切。

荷迪:在一天结束的时候,我们还有一个教育问题。经理想知道,“我们做了足够的验证来知道我的芯片是否工作?“大多数人明白如果你完整的证明,这是绝对的。但验证经理不懂之类的有界的结果。他们想要的数据形式呈现给他们,他们可以理解。从正式我的贡献是什么,什么是我的贡献从模拟;现在我的报道是什么芯片,我相信我们是好去吗?

Kelf解决最根本的问题:我们如何让大众正式呢?

Singhal:几年前它是毫无意义的讨论的整合正式报道。今天,正式的方式覆盖已定义和实现工具意味着同样的事情在模拟。当覆盖率表明你有50%完成了,这意味着同样的事情在任何域。

SE:如果我买覆盖工具从你们所有的人,我能把你的覆盖率结果今天好吗?

莎:需要定义覆盖的解决你的问题。在前面我们听到谈论如何用户已经完成仿真,然后发现另一个二十个错误使用CDC的工具。

荷迪:测量错误发现非常重要,是一个伟大的方式为正式的ROI。但这不是验证管理器的问题。他的问题是关于错误的设计。

Levia:人有双重标准。没人质疑模拟覆盖及其完整性,但当他们谈论正式在他们心中的第一个问题是你怎么知道你是完整的吗?与模拟覆盖你不知道它意味着什么,它到达多远,状态空间覆盖或实际的报道。它并不重要,我们作为供应商合并我们的报道,但这给用户我们一起把我们的覆盖率信息。

荷迪:我们支持uci就其本身而言,但它并不远远不够能够定义覆盖指标和保证验证经理正在寻找。它还远远不能使我们提出多个解决方案供应商。

Kelf:我同意。uci需要很多工作都包括。uci不是为正式的但我们可以层设计一些东西。

Singhal:数据来自不同的供应商都有一些细微的差别。很难让他们同意。

Levia我们要求完美吗?用户想要什么是领先的模拟提供者和领先的正式供应商给他们一个覆盖目标和结果的统一视图。它正在发生。

莎我回到我从早些时候的声明。模拟总是为你提供了一些数据。与静态工具,用户可以花大量的时间指定问题,但有时它返回。这是一个差距静态和动态需要修复的方法。得到覆盖率数据的结果和信息约束是很重要的。用户应该给出一些可行的。如果正式说东西是遥不可及的,你不应该试着达到仿真。我们需要为其他情况类似的事情。

荷迪:这让我们完整的循环,我们已经讨论了改进的事情我们可以证明,算法的应用,关于教育的抽象,可以和正式的社区类型的正式将完成的问题。

在最后这个圆桌会议的一部分,我们将看到连续的等价性检查。