开裂的螺母用正式的方法

Pranav莎,首席技术官的真实意图,保证一个拥挤的房间里正式的方法在最近的研究者和实践者FMCAD会议:“静态验证用于验证的设计。每一个主要的芯片是使用静态方法今天签字。”他使用类比螺母开裂。”有一个正确的方式和错误的方式,如果你不选择正确的方法,正式的-就像一个螺母很难破解。通过结合关注点分离和使用解决方案驱动方法,SoC验证,变成一个简单的难题。”

莎讨论如何设计范式改变了过去几年。不再有一个应用程序驱动的高端设计。相反,有许多领域包括移动、服务器和通信。尽管最近宣布苹果A7芯片包含了10亿个晶体管,复杂性不仅仅是晶体管计数。系统是由多个子系统组成的。“有100多个时钟域和嗨——速度异步接口,有电压岛屿和动态时钟和电源控制,所以等更多的时间限制,确保设计出现在一个确定的状态,设计测试(DFT),数以百计的IP核和模拟,都集成到一个单一的系统芯片(SoC)。”

虽然这是一个艰巨的挑战,但根据莎并不是不可逾越的。“有一个系统。这提供了一个清晰和关注点分离的验证。每一个定义良好的,是一个实质性的签字要求,有些是肥沃的土壤为应用程序的静态方法。范围的缩小,使正式的方法可行。”

使应用程序可行的你需要三件事:一个规范,强大的分析工具,高质量的用户体验。“通过一个狭窄的焦点,正式的引擎发光。作为一个例子,如果你正在验证数据的异步传输跨时钟域的逻辑需要引进来验证的正确性转移不是芯片的复杂性。本地小得多,很专注。”

没有完成正式的分析时,有很多信息,计算引擎内部用户可以清晰的方式定制或集中核查用户试图解决的问题。莎认为今天和数据方面做得还不够,它把正式的处于劣势。他描述了静态和动态的划分方法非常简洁:“模拟使用,当你不明白这个问题。你看一下输出有意义的事情。当你理解了问题你可以找到更好的方法。”

异步时钟域
爆发以来,接口的数量在一个SoC是不再可能发送相同的时钟设计的所有部分,因为延迟将超过时钟周期。部分系统使用变频,时钟的扩散控制和运行每个接口的渴望自己的频率,通常有大约100的芯片和时钟域代表100000个信号通道,每一个都必须得到核实。

这就是功能和定时相互交织和验证要求时间维度探讨由于亚稳定性。这使得现有的流的崩溃RTL综合和门级仿真或等价性检查。

致命错误引起的时钟域交叉。图的真正意图。

时钟域问题是麻烦的,因为失败是间歇性的。当它执行以合成也可以插入问题,所以即使RTL很好,但这并不意味着所有的已确定的问题。“你不能追求每一个单独的问题,而是你需要一个完整的策略来处理类的问题。”莎告诉观众。“这始于一些锚,可以发现,在这种情况下它是跨边界的时钟。”

这通常是一个同步器的地方。“一旦锚被发现、识别所使用的协议,查看被正确使用。这一定是自动完成。正如所有正式的方法:当发现违反创建一个紧凑的例子来证明这个问题。“莎指出如何一个分析的结果提出了是很重要的。“需要最小的痕迹,让用户明白是怎么回事。”

其他的正式目标
另一个问题是沸腾起来,根据莎,是时间限制管理。“在过去的这个错误不是至关重要的。这是一个质量问题的结果。今天,它正在成为一个关键的问题,可能会导致灾难性的失败。这需要约束准备早些时候流(RTL布局而不是在前),但这通常是依赖于不同的组织在一个公司。”一个例子涉及到多循环路径,设置和保存时间可以周期之间的问题。这又涉及多个时钟漂移。莎重申,在这种情况下,规范是隐性的,问题是绑定的范围,使它成熟的开发使用正式的方法。

“我们关注的领域之一”莎解释说,“我们可以绑定问题。块级别验证涉及到大量的时间开发一个试验台但是通常简单的调试,但当移动到系统级,升级调试困难。“这是错误的含义应该尽可能早地发现和正式不应该保存,直到所有其他验证技术的利用。通过使用正式的早些时候在这个过程中,可以避免昂贵的模拟使用自动化的方法,因为问题已经解决。

正式可以发光的另一个领域是模拟处理语义的能力有限。X传播是这些领域之一,仿真可以既乐观又悲观。尤其是一个问题在初始化期间很多Xs电路中存在的地方。门电路级仿真既慢又悲观。静态方法可以做得更好。

X-Hazards可以产生乐观和悲观。图的真正意图。

莎的结论是通过谈论如何重要的正式的方法已成为SoC流和他的观众传达了一个信息“FMCAD社会导致了这一结果,但也可以学习它是怎么来的。EDA公司技术,这个社区的消费者创造了但是他们只是引擎。如果你意识到我们正试图解决的问题的类型,它将为你的工作创建一个锚。”

观众的反应
摩西·瓦迪,莱斯大学计算机工程教授,问“总量的验证工作,一些自称是70%的设计、动态和静态是多少是多少?“虽然莎说,他不知道,瓦迪声称,没有这种信息很难知道他们的努力的影响。首席执行官,Oski Vigyan Singhal说,他大约10%的信念一直是静态的。莎还说,它所需的设置有关。“正式的验收要求。所以百分比是无关紧要的。”

瓦迪反驳道“当发现问题时,我们出一个方法来解决这个问题。这是一样的微软缓冲区溢位问题。但学科只有在被发现的问题。“莎回答说,“你可以定义纪律,但你不能强迫工程师接受。所花的时间在正式很小,因为它的工作原理。这些任务将花费很多时间在模拟”。

另一位观众问到引擎所需要的EDA的改进?莎问他们如何调试经验可以提高从所收集的信息进行分析。“即使分析是不完整的仍有可操作的信息,可以给用户。仿真的优点是它总是提供一些看看。”

与会者莎最后一个发人深省的消息。他告诉他们,他们应该寻找解决小问题在SoC设计流程,而不是假设他们可以成为唯一的工具用于验证。通过观察聚焦问题,可以实现有形的结果比仿真。

参见:
学生需要更多的正规教育吗?
提出了正式的回答