中文 英语
知识中心
导航
知识中心

X验证

X传播导致问题
受欢迎程度

描述

今天的soc是高度集成的,采用许多不同类型的IP,以不同的时钟速率运行,具有不同的功率要求。了解所有这些并发症合流产生的新故障模式,以及如何预防它们并实现终止,是很重要的。虽然在验证中处理“X”的问题一直存在,但由于低功耗应用程序经常关闭芯片部分,产生“未知”,这一问题变得更加严重。

数字设计中所谓的“未知”被表示为“X”逻辑电平。这意味着在四态逻辑中,信号实际上可能具有“1”、“0”或“Z”的值。X值在逻辑设计中一直存在,通常用于表示未初始化信号的状态,如未驱动的网络,或未重置的存储元素。“X-传播”发生在其中一个X值提供下游逻辑时,导致额外的未知。例如,如下所示,当信号` ` a '是一个未知值时,该未知值有时(但不总是)会传播到输出。

赋值y = a && b;

A b输出0 0 0 0 1 0 1 0 0 1 1 0 x 0 0 x 1 x

X在合成和验证中也起着有益的作用。对X值的显式赋值可以表示“不关心”条件,授予合成工具更大的灵活性来优化生成的逻辑。X值还用于验证,以标记由总线争用等问题产生的非法状态。自动形式检查工具可以使用这些赋值来检查是否无法到达非法状态。

不幸的是,由于被称为“X乐观”的X传播解释危险,X也可以掩盖RTL中的功能性错误。x乐观主义是不完全编码的一种特征,它错误地将未知值转换为已知值。当条件被评估为X值时,“If-else”语句和“case”语句可以是X乐观的。模拟语义不传播X值,而是将未知X值转换为已知值。条件是未知的事实不再可见——它是隐藏的,以某种方式使x传播难以捉摸。这里有一个例子:

// if-else条件
reg着干活;

Always @(*) begin ' if(条件)' ' out_1 = 1'²b1;' else ' out_1 = 1'²b0;结束
条件| out_1 ============ 1 1 0 0 x 0

当condition为1'b1时,输出为1'b1,当condition为1'b0时,输出为1'b0。但是注意当condition是X值时会发生什么。这里的X值是一个“未知”。但是输出被转换为1'b0,未知的X现在伪装成它肯定是1'b0,而实际上它可能是1'b1或1'b0,这取决于它如何合成成门。

虽然在门级模拟中可以检测到X-optimism错误,但在那里调试是缓慢而痛苦的。x - optimistic也可能是无害的,但仍然会导致RTL和门级模拟之间的差异,为了实现签名,必须努力解决这些差异。

现有工具的一些功能可以帮助进行x验证。例如,RTL分析工具将识别X分配。自动形式化工具更进一步,可以验证无法到达指定的“非法”状态,从而验证X值不会传播。虽然非常有用,但这只涵盖了可能存在的X的相对较小的百分比。此外,四状态形式化验证工具允许您编写显式断言,以确认X值不能传播到指定点。然而,这需要断言语言的知识和完全指定输入的适用行为的能力,以及需要知道设计中需要由断言验证的每个点,这是非常不切实际的。

X验证的签名不是一个容易解决的问题,因为仅仅存在X值并不是一个问题。问题是危险的X传播往往难以捉摸,因为它被X乐观主义转化为所谓的已知值。此外,x乐观主义是一个潜在的和间歇性的问题,因为只有当乐观主义发生时,x优化信号被用于设计时,它才会成为一个问题。在X乐观主义发生后,许多时钟可能无法检测到结果的功能问题,并且在其扇入中可能有多个X来源,使得分析根本原因非常困难。此外,如果在门级进行调试,模拟将非常缓慢,逻辑也不像原始RTL那样可读。

我们需要的是一个建立在现有RTL验证基础设施上的全面解决方案,它可以检测X值的传播何时掩盖了功能性错误。

页面内容最初由真正的意图


多媒体

科技讲座:应对未知


相关的实体

Baidu