正式的混乱

形式验证已经在过去的五年里取得了长足的进步。工具开发人员改变了方向,开始创建独立的应用程序,导致了技术的快速扩散。但正式的一套不同的工具,可以解决各种各样的问题在验证空间,这创造了一种不同的行业内的混乱。找出行业如何应对这些技术的迅速扩散,它可以听用户本身更感兴趣而不是工具厂商。

半导体工程坐下来讨论对与错方法应用形式验证技术Normando Montecillo,副技术总监博通公司;阿施施Darbari,首席工程师想象力的技术;罗杰·Sabbagh在华为首席工程师;PMC塞拉和斯图尔特•Hoad领导工程师/Microsemi。下面摘录的对话发生在解码正式,事件由Oski技术和由Synopsys对此。

SE:什么是最好的类型的块或类型的设计的应用程序形式验证技术吗?

Montecillo:控制块是真的good-blocks不会被描述为交通工具。但是之外,我们看到块交织在一起的控制和转换,我们开始正式的边界推入其中的一些地区,看到成功。这是一个关于时间的问题,并给予足够的时间我相信转换块也可以实现。

Hoad:我们正在努力包括块包含错误,可能很难找到使用传统模拟技术在我们的正式计划。

Sabbagh:我不认为这是黑色和白色,一些街区是完全不适合正式的。有一个光谱。你可能有一个块有一些粗糙的数学,是不适合正式定义它。但在界面你可能有复杂的流控制,从正式开始的好地方。如果你看看块及其功能列表,其中的一些可能是困难的对传统验证方法和适合正式的。所以你必须看这个在个案基础上。

Darbari:设计有很多连续的历史和仲裁类型的问题往往最噩梦错误但也可以很容易验证如果你做对了。我们还应该解决另一个问题:什么是正式的吗?言下之意是,这意味着模型检查,但这只是故事的一部分。正式的还包括连续的等价性检查和定理证明。所以当数学块可能很困难,一些公司已经成功的与数据运算电路和主导我们有工具可以应付这些。因此而不是说我想确认,我将把它作为块难道你用正式的验证。

SE:这是一个验证计划的问题吗?

Darbari:我们甚至计划之前,我想问是什么或者是不可能的。然后我们可以尝试的组合策略。正式单独并不能解决所有的问题,但可以模拟和补充模拟。验证了看起来很困难,特别是正式,但验证解决问题。这是一个心态和文化问题。

Hoad:计划是关键。我们可以说正式将被应用到所有的东西,但是我们试着找出我们将得到最大的价值。正式的是有限的资源,我们没有无限的工具和我们没有无限的人可以运行它们。所以我们计划将得到最大的价值。它可能是低端问题,很容易和快速或区域,我们知道会很难模拟。

Normando:计划是很重要的。资源是有限的,为了满足日程我们需要把最好的方法。我们发现正式适合在我们可以做初始缺陷的前端狩猎和设计非常干净。它不是要取代什么模拟。它是关于补充。

SE:这是一个变化。正式使用时进行模拟已经筋疲力尽了。

Darbari:人们一直在问,‘我们在哪里开始?“先删除问题的复杂性和看如果它是一个新的设计或者有很多新特性。我们有现有的testbenches吗?这是一个遗留设计在过去有问题?这是一种选择要使用的方法。

Hoad:有很多因素,如成熟的设计团队和设计,验证团队和过程。作为正式的家伙,我没有选择块的奢侈品。它通常开始于前面的设计存在问题关闭覆盖或者我们真的发现了一些严重的错误。然后我们可以评估块和决定哪些特性是服从正式和我们在哪里可以增加价值。

Montecillo:如果我能找到一个缺陷在前端,为什么要推迟到后端?最早发现bug可以降低了错误的成本。如果我能尽快找到它们RTL完成后,将提供一个成本节约。正因为如此,我也将正式在前方,即使是发现非常简单的bug。

Sabbagh:我们可以把它比这更早。我们可以用它来帮助设计。

Montecillo:看到之间的交互设计师和验证可以开导他们。

Sabbagh:如果我不知道我需要的资源。design-feasible吗?我们也可以证明架构概念。

SE:谁应该做正式的工作吗?设计师,验证团队,还是应该是一个独立的专家团队吗?和你在哪里找到这些人吗?

Sabbagh:自动化的东西如连通性检查或结构覆盖关闭,这些任何人都可以广泛应用的设计团队。仿真人可以做到这一点。白盒验证可以通过设计者通过添加自己的断言,也许在接口中添加断言验证工程师。但如果你想证明它不能死锁或管道中没有危险,那么你需要一个正式的专家——那些与正式的在日常生活中,已经建立了专业知识,所以他们知道如何分解问题,使其通过正式的消化。我怎么能使用抽象?我如何使用非确定性?你必须使用这些经验,这需要一个正式的投资团队。

Hoad:你不一定要完全隔离设计和验证团队的正式工作,这样他们就可以理解最好地应用它。

Sabbagh:两队需要参与规划阶段,但它需要有人从一个正交视图。如果你不做正式的全职,很难建立专业知识。

Montecillo:我一直在努力推动更正式的设计师,和我所说的正式模型检查一旦他们完成他们的设计。我败得很惨。很多人拒绝这么做,因为他们没有时间去学习一项新技术。设计师们负担过重。人已经试过没有做得很好。有些时候他们已经超过我的预期,但这些病例非常罕见。我们发现,最好是有一个专门的正式团队,可以设置环境,编写刺激的约束、工作和迭代断言和跳棋设计师。这个模型似乎是最有效的方式得到压缩。做正式的设计师不是最好的验证。

Darbari:设计师应该生产更多标准化代码从线头,但我宁愿独立验证工程师可以评估的规范。我们有时也有第三人做设计的审查没有先验知识或验证,并且经常强调一些关键问题。我不会仅仅停留在设计和验证团队,但也补充说,建筑师可以受益于使用它的建模,例如性能建模。资源的问题上,人们不会来自火星。我们必须训练人们并创建资源的管道。

SE:什么是理想的背景的人进入这个领域?

Darbari:我只是寻找一个非常明确的head-problem解决技能。

Sabbagh:我不认为我们可以现实地说,每个人都能做到。你必须看看他们的方法思考和尝试解决问题。有些人就是不认为以正确的方式。

Darbari:经验和领域知识同等重要。

Sabbagh:人是一个纯粹的验证人,没有设计经验可能是一个问题。知道RTL设计可以帮助工作。能够有效的RTL代码或硬件设计以减少时间和面积相同的技能需要正式testbench代码。你必须让它尽可能简单。这通常是相同类型的技能。正式的验证者有时也做一些白盒测试和能够调查的设计和理解正在发生的事情时,是您正试图验证的内部结构。好如果你有设计经验知道你看着和角落的类型用例,您应该检查。

在两个部分中,小组成员解决问题与完成,相关报道和教育。

有关的故事
验证面临独特的拐点
加入点之间DVCon沃利莱茵河的主旨,谈话与Accellera Shishpal Rawat和节奏的午餐面板。
一个正式的转换
独家:当你把正式的领导人来自世界各地在同一个房间里,给他们一个小时讨论部署?
系统级验证处理的新角色
专家在餐桌上,第一部分:系统级验证的作用是不一样的块级验证,需要不同的方式来考虑这个问题。
做单一厂商流有意义吗?
设计工具提供商可能希望用户锁定在一个完整的工具流,但是是最适合用户或行业?