验证统一

半导体工程汇集了行业名人发起讨论正式技术将便携式玩刺激的作用,以及它如何有助于拉近两种执行技术。参与这个圆桌会议是乔Hupcey,验证产品技术专家导师,西门子业务;验证的传道者,导师和副主席汤姆•菲茨帕特里克的便携式刺激工作组(PSWG);的首席执行官Breker;工程副总裁罗杰Sabbagh应用程序Oski技术;肖恩·Safarpour CAE主任VC正式Synopsys对此;汤姆·安德森,他是产品经理节奏时间和秘书的便携式刺激工作组;和Ashish Darbari,产品管理主管OneSpin解决方案。下面摘录,谈话。

SE:早在这个讨论中,几次机会出土了便携的方式刺激(PS)和形式验证可以一起工作。今天用户能做什么?

Hupcey:在现实中,正式的是一个分析的设计和PS给你反映了吗testbench。这就是今天这是罚款。这并不是一件坏事。实际上,在工具箱中有不同的工具,最终用户可以下载并开始应用,但这就是为什么我很高兴我们都讨论过这个问题。为未来的工作有很多机会,但是今天可以做什么?今天有两种不同的工具箱中的工具,也许他们可以有效的被合并。

哈米德:反对是,首先,我们必须让全世界采用大问题并提供解决方案,如他们如何得到模拟来模拟硅。明天也许这是一个问题。

Safarpour:正式的一侧,可移植性和reuseability的背景下思考,我觉得当你发展刺激的约束,你的断言甚至报道目标,你重用他们。假设成为断言,以确保你没有使用错误的假设,等等。我们已经看到人们使用覆盖属性在过去现在使用覆盖群体,所以他们可以在模拟和正式使用。可移植性和复用的概念有正式,PS,而不是生成刺激我们可以生成假设,约束。会有很大的价值,但我不知道如何映射到覆盖,覆盖点或覆盖目标和断言,。对正式约束只有三分之一的问题。

哈米德:我们讨论的是随机生成的直接测试。他们是自检测试。我们知道结果,所以我们正在做的检查变成你的报道或断言。

Sabbagh同样的问题在模拟。PS只是给你一些高级时尚的方式来表达你的刺激,但你仍然需要testbench跳棋。

哈米德:PS背后的价值是,它提供了刺激计划,检查和覆盖率。

Hupcey:当我开始做一些研究PS,我的偏见,这显然是太窄,这东西是一个大测试生成的机器。虽然它是有价值的,它远远不止于此。这只触及到了问题的表面。

安德森:测试生成,但还有更多。

菲茨帕特里克:回到正式,当你写假设或断言,“这必须发生之前,或在X周期。“PS模式相似的概念,特别是当涉及到调度。虽然我们没有在N的时钟,你可以模型,可以计算并添加一个约束,它无法大于x你会使用相同的模型生成的断言或者正式检查设计的吗?也许PS可以用来创建一组断言构造的设计,因为它允许您组一起,捕捉行为。

Darbari:你是让你的假设,你得到约束,你报道点,让你检查。这三个方面和锻炼他们的能力在正式或testbench环境中运行它们的目标,甚至在一个模拟器FPGA是伟大的。当我们谈到正式的用法我们说它能做块级别的知识产权级、系统级或者你可以让他们运行在一个模拟的目标。我必须问正式在哪里?

菲茨帕特里克:问题——这就是为什么我们称之为PS-we预计PS工具的输出将刺激testbench运行,正式和整个事情就是没有testbench。

Darbari:这不是真的。

Sabbagh:这不是一个testbench。

Darbari:一些非常复杂的正式testbenches建立严重高质量验证。

Sabbagh:白盒之间的区别正式,你证明这个FIFO永远不会溢出,与端到端正式的、有testbench,就像一个参考模型或记分板检查整个函数的设计,你想设计正式签署。

哈米德正式的:一个很大的价值,如果它可以了,是PS为凡人设计工程师能够代码场景。如果这可以进入正式的引擎,可以让你得到你需要的信息不需要专家,我可以告诉你,希望这种技术的人不考虑正式。他们太忙于芯片集成,通过启动。

Darbari:你有更多的模拟工程师比正式用户。

哈米德:我们必须让芯片醒来,几个周期的仿真运行。我们忙于做这个东西。

菲茨帕特里克:人将创建一个PS模型会思考这类问题。我不认为一个任意的PS描述可以翻译本身为一组正式的东西。

哈米德:为什么不呢?我认为这是可以做到的,因为我们有一个正式的可分析的模型那么为什么人不能决定他们想要一个PS工具供应商正式和读PS和把它变成断言和约束?

菲茨帕特里克:这将是正式的模型比刺激略有不同。这是我最初的印象。

Safarpour:不同的两种技术工作和正式的,原则上,更与需求比specifications-this我们做正式的方式。仿真是一个操作的方法。都有自己的理由。在正确的时间正确的理由。抽象层次,是关键。如果PS规范太抽象,不能映射到RTL规范SoC困难,那么是如何构建这些地图。这是一个挑战。

Hupcey:有synthesizable子集,可以创造出来的?

安德森:我不认为我们确定。这种技术非常新,没有很多例子。有认为你可能需要某些方面的行为从PS模型到某种形式的断言,可以对设计本身听起来可行的检查。我们描述testbench和测试结构,但是如果你看一个典型的模型与设计有重叠。你看到的一组行为和其他行为对应块的设计和他们一起交谈。也许你可以生成一个断言这两块应该做些什么,并检查它对RTL实现。这听起来并不太难。我不确定如何有效或有用。今天我没有看到人们写PS模型在建模约束DUT的输入和输出。你几乎总是假设您有一个贵宾说通过模拟。

Safarpour:如果你有正式的贵宾,那么您可以使用建立一个SoC的贵宾。在一天结束的时候,如果在模拟这都是可重用的,那么它必须synthesizable。

菲茨帕特里克仿真:我们正在考虑是,您将生成C代码并运行在处理器模型。我们不谈论生成RTL会编译。

Darbari:这不是那么糟糕,但这是一个想象的延伸。当然可行,可以编译C代码的机器代码,做C为硬件/软件正式在一起。

SE:图定义了路径设计。正式与路径覆盖,覆盖模型是在校准和正式的可以直接删除路径模拟需要考虑。

Sabbagh:有一个有趣的应用程序。如果有保险项目,可以通过正式的目标是遥不可及的,然后我们知道没有必要测试它。此外,正式的可以显示是可获得的。如果输入空间覆盖率模型没有提供一些报道点深入设计,然后正式可以帮助提供。可以喂,回输入空间覆盖模型和调整,显示这些序列将让你在那里,现在让我们改变输入覆盖空间允许,是可以达到的。

哈米德:它可以提供更多的价值。创建PS模型时,我们正在考虑可能发生的序列,场景可能发生,但是现在当我们在做动态测试,我们的业务运行大量的测试,因为个别场景往往不会失败,它是硬件交互时,他们往往会失败。在完美的世界里,我们可以把场景,把它们变成证据,表明将真正的在所有的情况下,没有其他IP或内存可以混乱。

Sabbagh:这是类似于我们前面谈到的,检查器可以生成并送入正式。但是,即使你不能,您可以使用仿真跳棋和提高你的刺激覆盖率模型基于来自正式的。

菲茨帕特里克:回到覆盖点,您可以使用正式的结果作为一个额外的输入到PS工具说的东西已经覆盖,或者我想要的目标,我知道如何到达那里。

Sabbagh:正式告诉你怎么做,如果你的覆盖模型不包括,它可以增强。

安德森为unreachability:我们已经这么做了,所以为什么不相反的例子,吗?

哈米德:仅仅因为正式证明的东西并不意味着模拟不是必需的。电很重要的东西。即使所有的逻辑是正确的,它仍然具有硅上运行。

Sabbagh我们并不是说。我们包括证人痕迹。正式的告诉你如何做某事,可以回滚到图。

Darbari问题是如果你有详尽证明通过正式一些的实现是没有可操作的生成测试的重点是什么?

哈米德:这是一个令人困惑的概念便携式刺激的家伙,因为我们将进入模型的定义应该是什么工作。

Darbari:真的,但实现可能不同。而且可能有一个错误在实现或一个规范的问题。

菲茨帕特里克:你的意思是正式的结果和用它来影响一代?应该有一个调和这两个方法。

Safarpour:这让我想起架构级验证,因为我们可以做同样的分析架构模型。还有很多东西你找到那里,发现不一致的规范。但是你还没有完成。那么你就去做设计,这可以被认为是金。

哈米德:PS的创建模型往往会迫使你理解你的规格。错误将退出所有的时间,因为这种原因。这可能是因为进进出出不匹配或你不能建立约束,因为模型不一致。

Sabbagh:这是一个经典案例。声明断言的属性约束或检查会发现bug。

安德森:任何严格的模型会有这种效果。你思考的方式超越了文字在纸上。

Sabbagh:试图使它可执行。

有关的故事
验证统一(第1部分)
验证任务依赖于动态执行和正式的方法今天,但这些技术有几个连接点。与便携式刺激可能会改变。
系统级验证处理的新角色
专家在餐桌上,第3部分:汽车可靠性和覆盖;便携式刺激的真正价值。
仿真的足迹
为什么突然模拟器是不可或缺的越来越多的公司,和接下来会发生什么。