正式的路线图

形式验证已经在过去的五年里取得了长足的进步,因为它专注于狭窄的任务验证流中。半导体工程坐下来讨论的进展和未来的正式技术,总裁兼首席执行官OneSpin解决方案;哈里·福斯特首席科学家验证导师图形;皮特•荷迪产品管理总监节奏;首席架构师Manish Pandey新技术Synopsys对此;的首席执行官Agnisys;,总裁兼首席执行官Oski技术。以下是摘录的谈话。第一部分可以被发现在这里。

SE:我们越来越接近更正式的规格吗?

问题你代表了连接和如何指定它正式呢?如何指定需要检查什么?你有开始的地方,有人来创建断言。但这一切都始于一个正式规范。然后你可以带来一个引擎来证明这一点。

福斯特:除了断言,我们有一个问题与规范。很多今天的模拟/混合信号问题可以得到解决,如果我们有这两个世界之间的正式规范。不需要断言。这只是一个可执行的规范。

Pandey:在规范方面,事情在某些领域更机械化。有正式的规范,非常明确的语义,我们还有很长的路要走。

福斯特:我同意。一个正式规范的一个问题在于,你立即缩小自由度。在某些领域,如协议规范,这是适用的,但是,我反对一个正式规范。它是棘手的,和没有错自然语言规范。

问题:有它可以应用的领域。

Brinkmann:它需要的东西是干净的,定义良好的和容易处理。但它不是一个通用的解决方案。

福斯特:有时它会。

荷迪:连接和状态控制寄存器中指定IP-XACT,那就是起飞。

福斯特我断言偏执狂,我接受,世界上可能只有10人喜欢他们的人。

荷迪:但这已经发生了改变。我们看到更多的人这些天舒服的断言。

Brinkmann:我同意。

问题:如果你手动创建断言,然后确保断言的问题是正确的。这只是两种相同的表示。

Pandey:你是对的,它是一样的。

福斯特:没关系。这是一个规范。

Singhal:规范与否,这个过程是关键。你必须决定你是否想要自动或手动完成的,但我们的目标是它如何适应设计周期和进度,和专业知识。你必须计划,你想要自动的规格,你要手动写断言,你想做什么系统级检查,一旦你有一个计划,可以测量。你知道当你可以说你做。

福斯特:这是关键,因为它从问题和说,“我有一个工具,我可以用它来做什么?”

Brinkmann为汽车用户:经常发生。人采用的方法从哪里开始验证计划和分解系统和定义他们验证目标,然后把它分成他们将使用什么形式验证会做什么模拟。不仅因为它是一个好主意,而是因为他们需要和需要提供的灵活性,能够证明他们已经做了很好的工作的验证。他们不能只是说,‘这是我的热点,然后试着做一些验证。不工作了。它必须被分解以系统的方式。

荷迪:你需要两个。的事情之一是一个大的心态变化,这导致了正式的收养,是人们乐于发现bug,生成相反的例子。现在错误狩猎是一件大事。我们不再总是专注于正式完成。这是好的,我们有一堆引擎,专门这并非旨在完成证明,但在深层勘探和反例的生成状态。这是正式的成功做出贡献。当你能把一块,应该是完全模拟,验证了给一个正式的专家或熟悉的人足够的工具,使用这些找出bug方法和找到更多关键错误,这是非常强大的。验证管理开始醒了,正式的力量。

Brinkmann:这是所有关于报道最后。他们必须提供它,不管他们是如何做的,是完整的证明,部分证明或bug打猎。你必须能够证明你已经做了很好的工作,独立于你是如何做到的。我们也看到客户的属性和分析它们的完整性和检查情况下如果他们已经走完了所有的角落。所以他们分析输入找到差距。差距分析需要的属性列表和说,如果你链这个属性与属性,如果你不在乎一个输入呢?所以必须有所缺失,告诉你要做什么。

荷迪:你必须提供覆盖率数据的方式可以被验证经理查看测试的覆盖率数据从所有可用的验证引擎。所以你必须确保报道由于正式的贡献可能出现在整个验证指标验证计划。这是唯一被接受和正式的全部价值。

问题:为什么不是正式被用作验证后的第一步,而不是吗?

Singhal:它是。不同的公司以不同的方式使用它。

荷迪:绝对的。的一个问题把它作为第一步是,尽管很多验证人舒服的断言,与其说这是设计师。所以技术,如自动正式和生成属性直接从RTL的帮助。能够使用assertion-based验证知识产权,所以如果我有一个安巴协议,我已经有一堆断言。这些东西可以自动化早期正式,而不是设计师的梦想把代码从一开始就断言。这些自动验证技术帮助巨大。

Singhal:提出正式的是这样一个令人兴奋的领域。他们用来做什么在沙箱验证他们现在在正式。

Brinkmann:他们更富有成效。人们简单地使用验证IP提出和验证芯片做一些有用的东西,或者至少是阻止他们在工作。他们不想感到尴尬时,集成。

福斯特:一个问题是,我们已经搬到UVM和这么多的验证工作进入建筑的基础设施,我们已经错过了单元测试。我们做太多调试在更高层次和企业也开始认识到。回到单元测试,在正式或沙盒测试,开始再次发生,这是一件好事。

Brinkmann:这是一个理想的正式申请-单元测试。你不需要考虑向量,你只是说你想看到的东西。

福斯特:它不需要详尽的。

SE:什么是正式的地位被用于模拟/混合信号吗?

荷迪:它是一个区域的发展。应用连接是相当简单的,因为你可以做真正的整数转换。如果你可以申请注册验证,从根本上说,所有模拟块与数字计算系统通过通信寄存器和您需要验证。很多取决于如何设计分区,如果注册是可见的在层次结构的层面上可以得到。所以有改进。模拟块的形式验证,您可以捕获的学位在转移函数和以不同的方式表达出来,是有可能的,但我们从广义模拟正式的一些路要走。

福斯特:模拟世界取决于超级巨星,这是一个问题。他们做事的方式。他们有自己的香料甲板,他们不想改变。他们必须创建一个模型,在数字的世界里,但他们甚至不运行它们。他们通过这个模型犯愚蠢的错误,如反极性和它经常不工作。这是一个简单的问题来解决,两组之间的一个可执行的规范。你不需要做正式的。

Pandey:也许会有转移功能,但如果人们想进入模拟领域,仍有大量的工作在结构方面。你想确保基本结构检查可以帮你很长一段路。我们能期待的最好在未来五到十年是如果你有模型的系统通过非正式技术可以显示他们对应的模拟块是什么。

问题:有些人定义注册界面模拟,唯一的选择是使用模拟。也许有些事情可以做在外围。

Brinkmann:还有一个经济问题。总有一个人模拟连接,他很想有一个正式的工具,但一个人在一个大公司意味着你不会出售太多副本所以它不是一个重要的目标。

Pandey:如果你看看工业控制系统,大量的模拟。你有这个数字接口驱动器,但我没见过这个工作扩大,所以它需要一些工作。也许有半打世界上研究人员正在研究这一领域。系统包含传感器,它可能成为一个更受欢迎的地区,在市场上更迫切的需要。在可预见的未来仍将是一个研究领域。

荷迪:成功的关键是好分区和分离和优雅地忽略的能力而不是正式的事情有重大问题不能忽视。

Singhal:如果你有模型,您可以验证模型的模拟设计。他们可能希望确保X传播正确的模型是忠实于模拟的行为。如果有一个错误在模型中你可能得到一个系统级的错误,但真正的模拟验证是很长的路要走。

Brinkmann:你必须确保模型所需要的基本功能。

有关的故事
正式的路线图(第1部分)
专家看正式的进展在过去的五年里,我们可以看到新功能出现。
差距在验证流程
专家在餐桌上,第3部分:小组成员讨论软件验证,SystemC和未来技术将有助于验证跟上。
选择验证引擎
什么工具最适合一个特定的验证任务可能会更清晰的营销文献中比在现实世界中。