消除 X 错误的自动化方法

摘要

由于未初始化的寄存器或者模块断电,设计中可能存在未知值 (X)。由于被称为 X 乐观(X-optimism)和 X 悲观(X-pessimism)的限制,无法在逻辑仿真中正确处理此类 X,从而产生可能掩盖 X 错误或破坏仿真结果的不准确仿真值。这可能会导致 X 错误逃避验证并降低设计质量。为了解决此类与 X 相关的问题,我们提出了一种全面的方法和几种新颖的方法,以在寄存器传输级别检测被掩盖的 X问题,并在门级别消除虚假 X问题。我们的案例研究表明,所提出的方法既有效又高效。

关键词 

X验证、逻辑仿真、形式验证、[1]  -- [16] 为本文最后列出的引用论文序号

1、介绍

与复位大多数设计寄存器的旧设计实践相比,物理综合优化和低功耗要求在复位后留下了更多未初始化的寄存器。此外,正常操作期间的掉电模块会在设计寄存器中产生未知值。在逻辑仿真中,“X”被分配来代表那些未知值,在实际硬件中可以是 0 或 1。这种未知值会导致电路中的状态不确定,从而使电路的操作变得不可预测。因此,确保这些 X 不会传播到重要的寄存器和破坏电路功能非常重要。      逻辑仿真是最常用的验证方法,是捕捉 X 相关问题的主要技术。然而,由于图 1 中显示的 X 乐观和 X 悲观问题,逻辑仿真无法正确处理 X。通常,X 乐观问题在寄存器传输级 (RTL) 仿真中最为严重,因为它们掩盖了 X 错误。对于门级仿真,X 悲观主义是主要问题,因为它会产生大量错误的 X,从而破坏仿真结果并使逻辑仿真变得无用。
Image
C在这项工作中,我们提出了一种更广泛的方法,可以检测被 X 乐观主义掩盖的错误并消除由 X 悲观主义产生的错误 X。我们的方法利用形式技术的证明能力和逻辑仿真的可扩展性,以便可以有效地执行准确的 X 分析。我们的方法包含以下组成部分:

• X-prescreener 分析测试用例以选择应该分析以暴露 X 错误的少量测试案例。

• XOPT Formal 正式识别由于 X-optimism 问题而被屏蔽的 X。

• XOPT Sim 启发式地将逻辑仿真偏向于采用与默认行为不同的条件分支来暴露 X 错误。

• 安全存入(Safe Deposit)方式分析输入,跟踪以识别寄存器中的 X,这些 X 可以安全地存入随机值而不会掩盖任何错误。

• SimXACT 消除了所有组合错误 X,以便门级仿真可以正常工作,并可以暴露真实的 X 问题。

(备注:X-prescreener,XOPT Formal,XOPT Sim,Safe Deposit, Simxact均为Avery相关工具的名称 )

在主要组件中,XOPT Formal 和 SimXACT 是基于我们早期的研究工作[1]、[2]、[3]、[4]、[5]提供的方案。整体 X 消除方法和其余组件是本文首次提出的创新。所提出的方法和技术目前正在商业生产中使用,表明它们在处理工业设计中的 X 问题方面是有效的。

本文的其余部分安排如下。在第 2 节中,我们回顾了相关的和我们以前的工作。第 3 节说明了我们消除 X 错误的方法,第 4-6 节详细描述了每个新组件。第 7 节提供了案例研究,第 8 节总结了本文。

2. 相关和以前的工作     

在本节中,我们简要回顾我们以前的工作和处理 X 问题的相关工作。

2.1. 相关工作     

大多数解决逻辑仿真中 X 问题的工作都集中在 RTL 上,因为 RTL 仿真中的 X 乐观可以很容易地掩盖错误。Piper 等人的论文 [12] 提供了有关如何在工业设计中生成 X 的全面背景。他们还调查了几位工程师以发现找出他们遇到的 X 问题以及他们需要的解决方案。但是,他们提出的解决方案缺乏技术细节,并且仅在小型 OpenCores 设计上进行了测试,因此它们在工业设计上的有效性尚不清楚。业界的另一个解决方案是 Synopsys [8] 的 XProp。在他们的解决方案中,当在语句的条件下遇到 X 时,会分析所有条件分支中的赋值并将它们的结果组合起来。如果变量的值在不同的分支下可能不同,则将 X 存入该变量。这种技术会创建额外的 X 并产生更接近门级仿真的逻辑值。但是,与门级模拟类似,也可能会创建假 X,从而产生大量需要分析的假警报。        取代修复逻辑仿真,Haufe 等人[6] 提出改变 RTL 编码风格以减少 X 乐观,使得当 X 存在时,RTL 仿真结果更接近门级。但是,这种方法只能缓解X问题,不能消除它们。Jasper 的 X 传播解决方案 [16] 和 Mentor [17]  提供了检测 X 问题的纯形式方法。与大多数形式方法类似,用户首先定义输入约束,然后指定要检查的寄存器。然后正式引擎检查指定寄存器中的 X 是否会破坏其他寄存器。此类解决方案可以提供适用于所有情况的准确证明。但是,设置形式分析可能很乏味,而且可扩展性仍然是一个问题。        为了消除门级仿真中的 X 悲观主义,Nicholas  [10]的工作增强了逻辑仿真以跟踪 X 及其否定面,并可以消除其收敛点处的假 X。他的技术是符号仿真(symbolic simulation)的简化形式,当设计变得过于复杂时,无法有效地追踪 X。Petlin 的解决方案[11]  可以找到 X 源以及可以捕获此类 X 的位置。但是,他没有提供如何使用分析来提高门级逻辑仿真精度的解决方案。此外,他的方法分析了 X 传播的所有可能路径,而我们的解决方案只分析了导致错误 X 的路径。后者具有显着的性能优势,因为搜索空间要小得多。萨尔茨等人。 [13]还提出了一种在门级模拟中减少 X 悲观的方法。在他们的工作中,他们假设了网表的一部分,称为“子电路”,其中可能出现 X 悲观主义。对于每个子电路,他们复制子电路并使用“X-splitters”将 X 分成 0 和 1。然后将这些具体值输入到子电路的两个不同副本中。然后使用“X-mergers”组合子电路的仿真结果。这种方法的问题在于识别正确的子电路进行分析可能很困难。此外,复制子电路可能需要大量内存。如果超过一个 X 可以馈入子电路,后者尤其成问题:重复的数量会随着每个额外的 X 源呈指数增长。与萨尔茨的作品不同,我们的工作自动识别遇到 Xpessimism 问题的子电路,并且由于使用了形式验证求解器,因此效率更高。

2.2. 我们以前的工作     

XOPT Formal 是我们检测 RTL 代码中 X 乐观问题的解决方案。它通过重放测试中的仿真轨迹并查找在逻辑仿真中具有非 X 值但实际上受 X 影响的寄存器来执行形式化的 X 分析。它在我们之前的论文 [2]、[4]、[5] 中有详细描述,这里是流程的简要总结:  1) 将设计划分为更小的块。  2) 对于每个块,将跟踪划分为几个时间间隔。  3) 对于每个间隔,用符号(symbols)替换 Xs 并使用主要输入处的仿真值作为激励来执行符号模拟。  4) 在间隔结束时,对于逻辑仿真中每个具有非 X 值的寄存器,根据其符号轨迹构建斜角连接(miter),并检查miter的输出是否可以为 1。如果是,则寄存器的值受到影响通过 Xs 并找到一个被屏蔽的 X。        SimXACT 是我们在门级仿真中纠正 X 悲观问题的解决方案。在 [1] 中,我们介绍了如何证明 X 是否为假,以及如何生成紧凑的修复程序来解决 X 悲观问题。下面提供了所提议技术的概述:  1) 给定寄存器 D 输入处的 X,我们通过沿 X 跟踪直到遇到非 X 值、主要输入或寄存器输出来构建布尔函数。然后我们使用中描述的proveX算法  [1] 证明X是否为假。这是通过使用 SAT 来显示布尔函数是否为常数来实现的。  2) 如果 X 为假,我们使用算法 ckt minimum1 和 ckt minimum2 来识别负责产生假 X 的小子电路。前者将子电路从输出减少到输入,而后者则相反。  3) 在识别出一个小的子电路后,我们生成行为代码来修复仿真。这是通过监控子电路输入端的值并在其输出端存储非 X 值来实现的。  在 [2] 中,我们要求用户提供检查点,并且只在检查点检查错误的 X。在这项工作中,我们提出了两种新方法,自动修复和自动监控,大大简化了使用模型。这些增强功能和新的 SimXACT 流程将在第 6 节中描述。

3. 消除 X 的方法     

 在本节中,我们将介绍我们消除 X Bug 的方法。对于 RTL,我们专注于检测被 Xoptimism 掩盖的 X。对于门级模拟,由于门级通常没有 X 乐观,我们的目标是删除所有错误的 X,以便可以轻松识别真正的 X 错误。    3.1. 在 RTL 检测被掩蔽的 X 错误      尽管 X 乐观和 X 悲观问题都可能出现在 RTL 仿真中,但 X 悲观并不是主要问题,因为它不会掩盖错误,设计人员可以更改他们的 RTL 代码来消除这种虚假的 X。因此,对于 RTL 模拟,我们的方法侧重于识别被 X 乐观掩盖的 X。由于 X 乐观因素造成 RTL X bug, 造成RTL 仿真中消失的 X,我们 称为 X。在下面的讨论中,我们将在条件为 X 时采用的分支称为“X-默认分支”。对于“if”语句,X-default 分支是“else”分支。对于“case”,它是带有“default”标签的分支。      图 2 说明了检测 RTL X 错误的流程。在流程中,我们可以选择应用 X-prescreener 来选择回归套件中应该通过 X 分析的测试。这一步的原因是执行 X 分析需要时间和精力。当回归套件中的测试数量很大时,分析所有测试可能不切实际。因此,选择一些可以覆盖大多数 X 场景的测试用例进行进一步的 X 分析将是有用的。如果用户已经知道应该分析哪些测试用例或者测试用例数量很少,则可以跳过该步骤。

Image

选择测试用例后,我们应用XOPT Formal,它使用形式符号仿真来检测逻辑仿真中被X-optimism屏蔽的X。此外,我们可以在运行回归测试时应用 XOPT Sim 来创建与 X-default 不同的场景,以暴露 X 错误。XOPT Sim 智能地存储值来替换 Xs,以便仿真偏向于采用非 Xdefault 分支,这会改变逻辑模拟的执行路径,并可能暴露隐藏的 X 错误。XOPT Formal 已在第 2.2 节中介绍。X-prescreener 和 XOPT Sim 将在下一节详细介绍。

3.2. 在门级删除假 X     

 如果使用AND、OR、XOR、INV等基本门类型对网表进行建模,那么门级仿真有一个特殊的特性,即模拟组合逻辑只能产生X-悲观问题,不能产生X-乐观问题.原因是对于每个门,它的所有输入都将在模拟过程中被评估,并且门的输出是悲观地确定的——只有当输入上的 X 保证不会传播到输出时,它才会产生一个已知值。因此,门级仿真中的非 X 值总是正确的,而 X 可能是错误的。在我们的 X 悲观去除算法中,我们利用这个特性来减少形式分析,与纯形式方法相比,它可以提供可观的性能提升。由于单元库中的组合逻辑单元是通常由此类基本的门组成,大多数设计都具有此特性。因为在门级仿真中没有 X 乐观,所有 X 错误都会暴露出来。然而,真正的 X 错误可能会被 X 悲观主义产生的大量 X 掩埋。因此,对于门级,我们专注于去除假 X,以便暴露真正的 X 问题。我们在门级仿真中消除错误 X 的方法如图 3 所示。在流程中,我们应用Safe Deposit分析(可选)来识别不影响设计操作的 X——这些 X 可以用随机值替换而不屏蔽任何错误。通过减少初始 X 的数量,将产生更少的假 X,从而减少进一步 X 分析的工作量。然后我们应用 SimXACT,保证消除所有组合错误 X。删除假 X 后,所有剩余的 X 都是真实的,应进行检查。

Image

4. RTL X 检测方法     

 在本节中,我们将详细描述我们在 RTL 上检测 X 问题的新方法。

4.1. X-预筛选器

X-prescreener 的目的是从回归套件中选择少量可以覆盖最多 X 场景的测试用例。X-prescreener 的工作原理如下:

1) 当在 if/case 条件中遇到 X 时,创建一个节点来记录{文件名、行号、层次名称到实例}。每个节点代表仿真过程中遇到的唯一 X 条件。

2) 运行测试后,测试期间创建的所有节点都将被保存并与测试关联。

3) 在分析完所有测试后,形成并解决最大覆盖率问题,以返回覆盖所有节点的少量测试用例。

目前,我们使用一个比较贪心的算法通过在每一步选择覆盖最多节点的测试用例来解决最大覆盖率问题。需要注意的是,由于non-X值的不同,同一节点的仿真路径对于不同的测试用例可能还是不同的。因此,不能保证所选测试用例将涵盖所有测试中遇到的所有可能情况。但是,如果运行进一步 X 分析的资源有限,所选测试用例应涵盖大多数 X 场景,并为要分析的测试用例提供一个良好的起点。

4.2. XOPT 模拟

XOPT Sim 是我们的创新,它使逻辑仿真偏向于采用非 X-default 分支来暴露 RTL X 错误,其工作原理如下。

1) 在执行“if”或“case”等条件语句之前,先检查条件是否为X。

2) 如果条件不是 X,则什么都不做。否则,可以选择性地将非 X 值存入条件中涉及的变量,这会在条件上产生非 X 值。是否存入值以及存入哪些值将在后面讨论。

3) 由于条件具有非 X 值,因此它可能采用与 X-default 不同的分支,这会改变仿真行为并可能暴露 X 错误。

以图4为例。当有效时钟沿到来时,假设变量 cond 是 X,那么“cond == 1”也是 X。在这种情况下,我们可以将一个值存入 cond。假设我们将 1 存入 cond,那么逻辑仿真将采用“if”分支并将 1 分配给 a。这会改变模拟结果,因为 b 不再是 1。如果正确的行为要求 b 为 1,那么由于 XOPT Sim 所做的更改,错误将暴露出来。

Image
目前,对于步骤(2),XOPT Sim 支持三种模式来确定是否存入数值以及存入哪些数值。在第一种模式中,随机值总是分配给条件中涉及的变量,使条件不再是X。条件可能有任何值,因此逻辑仿真可能会也可能不会采取与X-default不同的分支.在第二种模式中,形式求解用于求解值,以便始终采用不同于 X-default 分支的分支。对于“if”条件,条件必须是1。对于“case”,它可以是与任何非默认条件标签匹配的任何值。在第三种模式下,XOPT Sim 随机决定是否存值。如果要存放值,则使用形式求解来选择不是 X-default 的分支。这种模式会产生进一步的随机化,因为 Xs 可能会在以后被替换,允许仿真探索更多种类的场景。     

另一个需要解决的问题是哪些变量应该成为数值存入的目标。目前支持两种模式。在第一种模式中,XOPT Sim 将值存入直接涉及条件的变量中,无论变量是连线还是寄存器。在第二种模式中,XOPT Sim 仅将值存入寄存器或主要输入。在换句话说,它跟踪相关变量的驱动因素,直到它到达寄存器或数值存入的主要输入。以图 5 为例,模式 1 将一个值存入 cond,而模式 2 跟踪 cond 的驱动程序并将一个值存入 d,因为 d 是一个寄存器。
Image
通常,模式 2 是首选,因为它取代了存储设备或主要输入中的 X,这更接近于数字电路行为。但是,模式 1 仍然有用,因为它可能会创建更多种类的执行路径,因此更有可能暴露设计错误。另一方面,模式 1 可能会增加误报的数量,因为存储在线路上的值可能需要寄存器中的冲突值,而这些值永远不会在实际硬件中生成。     

XOPT Sim 为检测被 X 乐观问题掩盖的设计错误提供了一种启发式方法。另一种常用的暴露 RTL X 错误的启发式方法称为随机Deposit,是将 X 替换为随机选择的 0/1 值,然后照常执行逻辑仿真。与后一种方法相比,XOPT Sim 更容易发现错误,因为它允许 Xs 传播并且可以使仿真偏向于选择不是 X-default 的分支,而随机Deposit完全基于概率。然而,XOPT Sim 通常比随机Deposit慢,因为必须涉及形式化求解和额外的代码执行跟踪。     

与形式方法相比,XOPT Sim 具有优势,因为它基于逻辑仿真;因此,它比形式方法更具可扩展性,并且工程师的验证环境没有变化。因此,它比纯形式工具更容易设置和使用。但是,XOPT Sim 不能像形式方法那样提供全面的分析。为了解决这个问题,XOPT Sim 可以通过使用不同随机种子的回归测试来运行,以便可以探索尽可能多的现实操作场景。     

一些现代仿真器为用户提供了更改 X-default 分支的选项。与 XOPT Sim 类似,此功能允许启发式地暴露 X 错误。但是,更改 X-default 分支而不用具体值替换 X 可能会产生太多误报,因为暴露的错误可能需要对 X 进行冲突的值分配,而这在实际硬件中是不可能的。通过求解改变仿真执行路径的具体值,XOPT Sim 减少了误报的数量。

5. Safe deposit分析     

Safe deposit分析的目的是找到不影响任何状态寄存器的 X——这些 X 可以被随机值替换而不会掩盖任何错误。应用此分析的一个常见场景是分析重置序列以识别将在重置后消除的设计 X。通过减少初始 X 的数量,在仿真过程中会产生更少的 X 悲观问题,从而减少 X 分析工作。     

Safe deposit分析算法如图6所示,算法的输入是要分析的电路 (ckt) 和输入迹线 (trace)。该算法返回其 X 可以安全存放的寄存器,因为在跟踪仿真期间消除了这些 X。

Image
该算法首先向设计中的每个寄存器注入一个具有 X 值的符号。然后执行符号模拟以模拟第 3-4 行中的输入轨迹。在每个循环中,我们收集电路输出处的符号轨迹并将它们保存到轨迹中以捕获将传播到电路之外的 X。在模拟输入迹线后,我们在设计寄存器中收集符号迹线并将它们添加到第 7-8 行的迹线中以捕获仍然存在于电路中的 X——这些 X 可能会影响未来的设计操作。在第 9-11 行中,我们使用常规的check_ x 来分析每个符号轨迹以查看它是否具有真实的 X。这是通过构建斜接器来实现的,以查看Xs能否在符号跟踪[5]的输出上产生不同的值。如果 X 是真实的,我们使用 strace.get regs() 获取 X 来自的寄存器并将返回的寄存器添加到 unsafe regs 中,因为这些寄存器中的 X 不会通过仿真输入跟踪消除,并且无法安全存放.在第 12 行,我们剔除寄存器设计中具有 X 值的所有寄存器中的不安全寄存器,并将结果保存到安全寄存器。安全寄存器中的寄存器具有 X 值,这些值将被输入跟踪消除。这样的 X 不影响设计操作并且可以安全地沉积。最后,安全 regs 作为算法的输出返回。

6. SimXACT 假 X 消除方法

在本节中,我们将介绍用于纠正门级仿真中的 X 悲观问题的 SimXACT 流程。

6.1. 总的流程     

我们的 X 悲观消除流程的输入是用于跟踪的输入激励、门级网表和应该第一次检查 X 以确定它们是否为假的开始时间。输出是辅助代码,当遇到相同的 X 悲观条件时,那些错误的 X 将被正确的值替换。  我们的方法如下:

1) 在开始时,我们检查寄存器数据输入(通常表示为“d”)中的 X 以确定它们是否为假。

2) 对于每个假 X,我们跟踪寄存器输入的扇入电路,以找到其中的一部分,称为子电路,其输入是实 X,输出是假 X。

3) 我们根据子电路生成假X消除解决方案和辅助代码来消除此类X。

4) 产生的修复代码被自动用于修复前的仿真值。Auto-monitor 然后找到需要在整个模拟过程中检查的更多 X。

跟踪分析完成后,生成的辅助代码可以用于以后的仿真,以消除假X。该流程允许门级仿真产生正确的结果。

流程中的前三个步骤在 [1] 中提出并在第 2 节中进行了回顾。在本节的其余部分中,我们将描述我们的创新、自动监控和自动修复,然后提供一些讨论。

6.2. 自动修复和自动监控

在我们的流程中使用自动修复来立即应用生成的修复来修复仿真结果。自动修复的工作原理如下:只要在 SimXACT 运行期间生成修复,我们就会开始监控修复条件的仿真值,并在条件匹配时将非 X 值存入以替换目标变量上的假 X。当值不再符合条件时,Force 值被释放。这可以通过仿真器的编程接口来实现。在每个循环中,我们的方法保证修复所有假 X,因为假 X 的数量是有限的,并且我们的程序在每次迭代中至少修复一个假 X。因此,修复过程最终将结束。然后,自动修复允许我们的方法在一次通过中找到所有假 X,因为在当前周期修复假 X 可以在后续循环中暴露更多假 X。由于我们的 X 分析和修复方法可以在任何给定周期内找到并修复所有错误的 X, 通过自动修复,我们可以保证在所有周期内的所有假 X的痕迹将被修复。

Auto-monitor 检查仿真活动并将 X 分析应用于可能具有错误 X 的变量。更具体地说,它监视寄存器 D 输入的扇入逻辑上的门级仿真值,并在其扇入逻辑中的值发生变化并且 D 输入具有X 值。换句话说,如果变量具有 X 值并且其扇入锥中的变量值发生变化,则会再次检查该变量。

自动监控消除了选择时间点以执行 X 分析的负担,并大大简化了 SimXACT 流程的应用。由于我们在变量有扇入变化时再次检查变量,我们可以确保不会遗漏错误的 X,从而确保我们分析的完整性。通过自动修复和自动监控,如果 X 分析的开始时间在模拟开始时,则可以保证模拟没有组合假 X。

6.3. 讨论

要选择分析的开始时间,一种简单的方法是在仿真开始时开始。这可确保不会遗漏任何错误的 X。但是,重置之前的 X 数量可能很大,从而使分析非常耗时。由于大多数预复位 X 通常不会影响仿真正确性,因此在实践中,我们通常会在复位无效前几个周期开始 SimXACT 分析。

在将我们的解决方案应用于工业设计时,我们发现需要很长时间才能证明的错误 X 通常不会导致门级仿真无法通过验证。进一步的分析表明,这种虚假的 X 通常是“偶然的”。例如,如果加法器的某些输入碰巧为 0 而其余输入为 X,则加法器的进位位可能具有假 X。在 RTL,加法器的输出很可能是 X,X 不会引起仿真问题。由于大多数验证环境是围绕 RTL 构建的,因此门级的错误 X 变得无关紧要。我们利用这一观察来减少分析的运行时间。例如,我们忽略扇入全是 X 或 X 比用户定义的数字多的变量。

尽管 SimXACT 很高效,但分析大型设计的长迹线仍然很耗时。为了加速对大型设计的 SimXACT 分析,可以部署分区流。在流程中,我们对设计进行了分区,以便在每个分区中只分析一部分寄存器。然后我们并行运行所有分区以生成修复程序。然后组合来自所有分区的修复以生成修复文件。然后将修复文件用于未来的仿真。请注意,由于每个分区在每次运行中仅生成部分修复,因此可能需要重复该过程以生成所有修复。

7. 实例探究

本文中描述的方法和技术目前正在商业生产中使用。XOPT Formal 的有效性已在 [2]、[4] 中报告。自工作以来,XOPT Formal 又成功验证了另外 7 个芯片,并发现了 6 个被掩盖的 X-optimism 漏洞。在本节中,我们专注于为我们的新创新 SimXACT 和Safe Deposit分析提供更多详细信息,以证明它们在消除真实工业设计中的虚假 X 方面的有效性。对于 XOPT Sim,我们发现模式 2(寄存器存放)几乎总是首选,因为寄存器是 X 在实际硬件中驻留的地方。但是,编程接口的支持,由于商业逻辑模拟器的局限性,追踪正确的 RTL 扇入逻辑可能很困难。此外,在将值存入寄存器后,无法保证这些值会及时传播到条件中涉及的变量以偏置逻辑仿真。目前,我们能够偏向模拟以在大约 70% 的时间内采用非默认分支。为了使 XOPT Sim 更有用,需要逻辑模拟器的额外支持。

7.1. SimXact

我们使用 Verilog 编程接口将我们的解决方案与商业仿真器集成。我们的正式引擎基于加州大学伯克利分校 [15] 的 ABC 包。所有的基准测试都是在仿真计算阵列中常见的高端工作站上完成的。由于与公司的保密协议,我们无法透露设计及其测试平台的详细信息,但所有设计都有数百万个门并且是真正的工业电路。案例研究的结果总结在表 1 中。

Image

第一种情况大约有 142K 个寄存器。测试平台是基于 VMM 的,仿真器是 VCS。我们分析了从复位解除断言之前的几个周期开始直到第一个事务完成的跟踪,大约有 15K 周期长。运行时间为一个小时,我们发现了 450 个修复程序。由于插入的测试结构,我们发现了真正的 X 问题,否则传统随机Deposit方法会掩盖这些问题。在解决了真正的 X 之后,门级仿真就很干净了。

第二种情况有大约 150K 个寄存器。测试平台采用 VHDL,网表采用 Verilog。NC 用于仿真。我们用半小时分析了设计的重置顺序,并且仿真是干净的修复。

第三种情况有大约 140K 个寄存器。测试平台是简单的 Verilog,它生成了一个 64 个周期长的短硬件复位序列。我们用 10 分钟分析了跟踪结果,发现了 258 个修复。使用修复程序的功能,门级仿真都很干净。

第四个案例有大约 3M 个寄存器。我们在没有分区的情况下分析了 3 天的跟踪结果,并生成了大约 1000 个修复程序。应用修复后通过了门级仿真。

除了这些案例研究之外,SimXACT 已应用于四十多种设计,以解决门级仿真中的 X 悲观问题。它还有助于暴露至少五种设计中的 X 错误。

一般来说,根据我们在这些公司的经验,设置环境通常只需要几分钟,芯片级分析可以在几个小时内完成。这修复 X 悲观问题的代码,允许门级仿真通过验证。对于仍然失败的仿真,总能发现真正的 X 问题。在这里,我们展示了一个从真实设计中发现的 X 错误。X 来自一个信号,该信号指示是否已完成一项计算以及是否可以执行进一步的处理。在应用 SimXACT 之前,使用了随机Deposit,测试顺利通过。然而,使用 SimXACT,Xs 的测试失败了。由于 SimXACT 消除了虚假 X,因此通过跟踪波形中的 X 传播,可以轻松识别 X 的来源。生成 X 的 RTL 代码如图 7 所示。在设计中,cal1 done 已复位,而 cal2 start 没有。在 RTL 模拟中,当 cal1 done 为 X 时,cal2 start 被赋值为 0,所以看起来 cal2 start 工作正常。但是,在实际硬件中,在复位周期 cal2 start 可以是 0 或 1。对于复位后的周期,基于 cal2 start 的计算可能会或可能不会基于 cal2 start 的值开始,这可能会产生不正确的结果损坏数据路径。由于设计中cal1在复位周期完成为1的概率仅为1,随机存款并没有暴露问题。但在实际硬件中,芯片每上电 64 次就会处于故障状态,这是一个严重的问题。为了解决这个问题,设计者为 cal2 start 添加了 reset。在这种情况下,SimXACT 成功阻止了重新设计。

Image

7.2. Safe Deposit分析

Safe Deposit分析是使用名为 Insight [14] 的商业符号仿真器实现的。我们应用它来分析上一节中的第三种情况,运行时间为 2h12m。4930 个寄存器被确定为可安全Deposit。我们在将这些寄存器存入随机值后应用了 SimXACT,修复次数从 258 个减少到 156 个,这表明执行安全存入分析确实可以减少在模拟过程中产生的假 X 的数量。

8. 结论

在这项工作中,我们提出了一种综合方法和多项创新,用于在 RTL 中发现 X 问题并消除门级仿真中的错误 X。我们的第一项创新 XOPT Sim 可以启发式地暴露 RTL 中的 X 错误。我们的第二项创新 SimXACT 可以消除门级仿真中的所有组合错误 X,从而在 X 存在时允许仿真产生正确的结果。通过消除错误的 X,可以暴露真正的 X 问题,并且可以避免代价高昂的重新设计。我们的第三项创新,Safe Deposit分析,可以识别不影响设计操作的 X并且可以安全地存入随机值。通过减少初始 X 的数量,可以减少 X 分析工作。该方法在商业生产中使用,表明其在解决工业设计中的 X 问题方面的有效性。

参考文献

[1] K.-H. Chang and C. Browy, “Improving Gate-level Simulation

Accuracy when Unknowns Exist”, DAC, 2012,

pp. 936-940.

[2] K.-H. Chang, H.-Z. Chou, H. Yu, D. Dobbyn and S.-

Y. Kuo, “Handling Nondeterminism in Logic Simulation

So That Your Waveform Can Be Trusted Again”, IEEE

D&T, DOI:10.1109/MDT.2011.75

[3] K.-H. Chang, Y.-T. Liu, C. Browy and C. Huang, “System

and Method for Correcting Gate-level Simulation

When Unknowns Exist”, United States Patent 8402405,

Mar 19, 2013

[4] H.-Z. Chou, H. Yu, K.-H. Chang, D.Dobbyn and S.-Y.

Kuo, “Finding Reset Nondeterminism in RTL Designs

– Scalable X-Analysis Methodology and Case Study”,

DATE, 2010, pp. 1494-1499.

[5] H. Z. Chou, K. H. Chang, and S. Y. Kuo, “Accurately

Handle Don’t-Care Conditions in High-Level Designs

and Application for Reducing Initialized Registers,”

IEEE TCAD, Apr. 2010, pp. 646-651.

[6] C. Haufe and F. Rogin, “Ad-Hoc Translations to Close

Verilog Semantics Gap,” workshop on DDECS, 2008, pp.

1-6.

[7] K. Liu and R. Sabbagh, “Confidence in the Face of the

Unknown: X-state Verification”, Verification Horizons,

Vol. 9, Issue 2, Jun. 2013

[8] G. Maturana, A. Salz and J. T. Buck, “Method and

Apparatus for Simulating Behavioral Constructs Using

Indeterminate Values”, US Patent 8271914, Sep. 18, 2012

[9] A. Mishchenko, S. Chatterjee, R. Brayton, “DAG-Aware

AIG Rewriting, A Fresh Look at Combinational Logic

Synthesis”, DAC, 2006, pp. 532-535.

[10] R. Nicholas, “System and Method for Improved Logic

Simulation Using a Negative Unknown Boolean State”,

US Patent 7761277, Jul. 20, 2010

[11] O. A. Petlin, “Verification Systems and Methods”, US

Patent Application 2010/0313175 A1, Dec. 9, 2010

[12] L. Piper and V. Vimjam, “X-Propagation Woes: Masking

Bugs at RTL and Unnecessary Debug at the Netlist”,

DVCon, 2012, session 5.3.

[13] A. Salz, G. R. Maturana, I.-H. Moon, L. R. Mcllwain,

“Method and Apparatus for Reducing X-pessimism in

Gate-level Simulation and Verification”, US Patent Ap-

plication 2012/0072876 A1, Mar. 22, 2012

[14] Avery Design Systems Inc., http://www.averydesign.

com

[15] Berkeley Logic Synthesis and Verification Group, ABC:

A System for Sequential Synthesis and Verification,

http://www.eecs.berkeley.edu/alanmi/abc/abc.htm

[16] Jasper Design Automation Inc., http://www.jasperda.

com

Top