简介Cadence JasperGold X-Propagation Verification App 用户指南是一份面向数字IC设计验证领域的形式验证官方资料适合芯片验证工程师、设计人员以及打算在项目中引入形式验证的团队参考。X不确定态通常源于未定义逻辑、浮空输入或竞争条件一旦在电路节点间传播就可能使系统行为偏离预期因此需要在设计早期仔细排查。该指南系统讲解了在JasperGold环境中自动检测X传播路径、开展深度分析与可视化、生成根因定位报告以及获得优化修复建议的完整流程还对比了形式验证与仿真验证在错误发现能力、设计周期和成本上的差异并明确了工具使用的版权与许可事项。资源包内为1份PDF格式的用户手册大小约2.6MB完整覆盖2020.03版本内容目录章节从X-Propagation基本概念一直延伸到具体操作细节便于按需查阅。目前已有337人学习下载适合作为形式验证入门学习和JasperGold工具实践的常备参考资料。 没用过 JasperGold 的 xprop 模式之前我一直觉得 X 态问题属于那种“仿真时骂两句、综合后烧把香”的玄学。直到有一次做 CDC 跨时钟域验证仿真前仿后仿结果总是对不上RTL 里一票 X 态从亚稳态寄存器一路扇出到状态机最后手工追了整整一周才定位到源头。从那以后我就把 xprop 当成正式验证流程里的常备工具。如果你也在跟 X 态搏斗或者正在看这份jaspergold_xprop_userguide.pdf但被里面一堆选项搞得头大这篇文章应该能帮你省不少时间。我会按自己的使用路径来写先说 xprop 到底在解决什么问题再拆它的核心原理接着给一套能直接抄的实操流程最后是我在项目里踩过的一些坑和排查思路。1. 先搞清楚 xprop 到底解决什么问题1.1 X 态是什么为什么让人头疼X 态Unknown state在数字电路里是个很有意思的存在。仿真器用它表示“不知道当前是 0 还是 1”的情况比如未初始化的寄存器、异步复位释放瞬间、跨时钟域的亚稳态采样结果或者是存储器的未定义输出。四态仿真里 X 会传播一个 X 进了加法器出来的可能是 X进了比较器结果也可能是 X再连着几级逻辑整个数据通路都会变灰。听起来好像很合理仿真器在告诉我们“这里状态不确定”。但问题在于真实芯片里不存在 X 这个东西。芯片一上电每个触发器最终都会落到某个确定的 0 或 1只是我们事前不知道是哪个。所以 X 是仿真模型里的抽象不是物理事实。这个抽象在两种场景下特别容易咬人前仿RTL simulation里X 传播开以后状态机可能跳到非法状态计数器可能错乱然后仿真结果跟预期不符但你又分不清是设计 bug 还是 X 态导致的“假错误”。后仿gate-level simulation里综合工具默认把未初始化寄存器复位到 0很多 X 会消失于是一些在前仿里被 X 掩盖的问题在后仿里又暴露出来。于是同一个设计前仿全红后仿全绿或者反过来你根本没法判断真实行为是什么。xprop 想解决的就是这个“X 态到底会不会影响设计功能”的判断问题。1.2 传统手段为什么不够用我以前在项目里的做法基本是“暴力法”。先在仿真波形里找到 X 出现的时刻然后追扇出看一下 X 穿过了哪些逻辑最后人工判断这些路径有没有可能影响关键功能。这套做法在小模块里还能忍一旦设计规模上来X 的扇出可以夸张到几十上百条路径人眼根本看不过来。还有工程师会用 lint 工具或者仿真器的 X 传播选项来做粗略检查比如某些仿真器有-xprop之类的仿真选项能帮你把 X 传播的结果打出来。但仿真本身有个天然局限仿真向量覆盖到的只是所有可能输入序列里极小的一个子集没跑到场景不代表不会出事。尤其对于 X 态来说如果仿真根本没激励出那条会采到亚稳态的路径那 X 的传播问题就被完美地隐藏了。1.3 形式化方法在这里的优势JasperGold 的 xprop 模式核心思路是把 X 态传播问题变成一个形式化验证问题给定设计中的一组 X 源穷举所有输入序列和初始状态看 X 会不会传播到某些关键节点上。不需要写测试向量不需要指定输入变化的具体时间点只要约束设得合理它对状态的枚举是完备的。这也决定了 xprop 的定位它不是仿真器的替代品而是一个“仿真想查但查不干净”的问题的补充手段。适合在 CDC 验证、复位释放检查、低速接口数据通路以及任何对 X 态敏感的模块上使用。对于做数字前端验证或形式验证的工程师xprop 应该常驻在工具链里。2. 核心原理JasperGold 的 xprop 在做什么2.1 从“传播分析”到“可观测差异”我在第一次看 xprop 的 user guide 时被一堆术语绕得有点晕什么x-source、x-effect、observability、bounded mode。后来我用自己的话把它捋了一遍其实 xprop 干的事情可以分解成三步找到设计中的 X 源。所谓 X 源就是仿真时会产生未知状态的节点比如没有复位端的触发器、黑盒输出、存储器的未初始化输出等。你可以让工具自动找也可以手动指定。在形式化引擎里把 X 源“置为自由变量”。也就是说这些节点不是固定 0 或 1而是在每个周期都可以独立取 0 或 1。检查这个 X 值是否会被传播到观察点也就是你关心的关键节点或者断言。关键的区别就在这里。普通的 X 传播仿真是给一个具体的输入序列看 X 在时序逻辑里怎么流动结果依赖你给的激励。而 xprop 是把 X 的变化当作“所有的可能取值”用形式化引擎去穷举只要存在某一种 X 的赋值和某一条输入序列能让 X 的影响传到观察点工具就会给你一个波形反例。我一直觉得“可观测差异”这个词才是理解 xprop 的钥匙工具不关心 X 本身传到哪它关心的是当 X 取 0 和 X 取 1 的时候观察点上的逻辑值是否存在不一致。如果存在那说明这个 X 对下游是“有影响”的这就是一个需要处理的隐患。2.2 悲观性与乐观性的博弈用形式化方法查 X 态很容易走向两个极端。太保守的话报告里全是“X 传播到这里了”但实际上 X 被后续逻辑掩蔽mask了根本不影响输出这种报告看着吓人其实没多少有效信息。太乐观的话工具会根据某些假设把 X 过滤掉结果漏报了真正有问题的路径。xprop 在这中间做了一个取舍它引入了布尔约束求解的机制X 源被建模成自由变量后工具会对观察点做等价性检查。如果x0和x1两种情况下观察点完全一样就认为该 X 不可观测unobservable不会报出来。如果存在差异才判定为可观测的 X 效应。这么一来那种“X 穿过了三排逻辑但最后被与门掩蔽掉”的路径不会被误报能大幅减少人工筛报告的时间。但这里也有个注意点可观测性检查本身是在一定的“状态空间边界”内做的如果你限制了 cycle 数或者没有把某些 X 源建模进去那报告可能会偏乐观。理解悲观和乐观的边界在哪是使用 xprop 能不能报出有效结果的核心。2.3 与仿真 X 传播的互补关系我以前犯过一个错误觉得既然有了 xprop就可以完全不用关心仿真器里的 X 传播报告了。后来发现两者其实是在解决不同层面的问题。仿真器里的 X 传播告诉你“在当前输入序列下X 确实影响到了这些信号”这是实际行为的快照。而 xprop 告诉你“在所有可能的输入序列下X 有没有可能影响到这些信号”这是一个能力边界。对验证工程师来说这两类信息是互补的。如果仿真里 X 传播得很凶但 xprop 认为不可观测说明这条路径上大多数 X 效应会被掩蔽不需要过度紧张。反过来如果 xprop 报了一条不可达的路径那说明设计里可能存在一个潜在的 X 敏感点即使现在的测试向量没踩到将来改版或者换约束时也可能踩到。所以 xprop 更适合用来做“设计体检”而不是单纯替代仿真调试。3. 跑通一次 xprop从读设计到看报告3.1 准备工程文件与读入设计刚上手 xprop 的时候我建议直接从 JasperGold 自带的示例工程开始跑通了再换自己的设计。jaspergold_xprop_userguide.pdf里给的示例基本都是用read_file读 RTL然后elaborate来例化设计。具体到 Tcl 命令初始化一个工程大概是这样的set project_name xprop_demo set top_module dut_top read_file -format sverilog -vcs {-f filelist.f} elaborate -top $top_module注意几个点read_file的时候如果设计里有 IP 或者第三方库一定要把库文件路径加进filelist.f否则会在 elaborate 阶段报一堆未定义的模块。还有-format sverilog要跟你实际代码语言匹配用systemverilog有三种写法用-vcs传入编译选项能省掉很多语法兼容的麻烦。elaborate 成功之后建议先用get_design_info看一眼顶层模块的例化层次和信号数量确认设计被正确读入。我见过有人跳过这步直接跑 prove结果折腾半天发现读的设计根本不是自己想的那个纯粹浪费时间。3.2 设置约束、时钟与复位xprop 虽然是形式化验证但同样需要时钟和复位约束。时钟用 create_clock 创建create_clock -name clk -period 10 [get_ports clk]复位的话一般建议不要直接把它设成常数 0 或 1而是用add_reset命令把复位行为建模成“先有效再释放”这样 X 态分析会更接近实际上电场景。如果设计中有些信号是固定的配置位比如 mode 选择、地址映射基址可以用add_assume或者set_constant锁成固定值减少状态空间。这里有个小坑如果你不约束某些输入xprop 会认为它可以取任意值那状态空间会爆炸跑起来特别慢。所以正式跑之前建议花点时间把设计里“正常情况下不应该变化”的输入全部用约束固定下来。约束越合理跑得越快结果也越聚焦。3.3 跑 xprop 的核心命令序列JasperGold 跑 xprop 的主流程其实很简洁核心就是setup、prove、analyze三连set_xprop_mode -auto_source_detection {rst clk} setup -mode xprop -xprop_sources {unresolved_triggers uninitialized_flops} prove -mode xprop analyze -mode xpropsetup -mode xprop负责配置 X 源类型-xprop_sources是你想分析的 X 来源。常用选项里uninitialized_flops是指没有复位端的触发器unresolved_triggers是指跨时钟域采样点上的亚稳态触发器。你可以只分析其中一种也可以一起分析。prove -mode xprop是真正调用形式化引擎去求解的阶段。它会自动把 X 源建模成自由变量然后用 SAT 或者 BDD 相关的引擎做可观测性分析。这里的运行时间通常不会太短如果设计比较大建议在服务器上跑或者先用-bounded限制分析的 cycle 数比如prove -mode xprop -bounded 100先看前 100 个周期内有没有问题再决定要不要全量跑。analyze -mode xprop则是把证明结果整理成报告。跑完之后工具会在工程目录下生成xprop_report.txt里面会列出 X 源、传播路径、观察点以及每个报告项的性质pass / inconclusive / fail。3.4 解读报告的关键信号报告拿到手之后先看两个地方一是xprop_source列表二是xprop_effect列表。前者告诉你有多少个 X 源参与了分析如果数量是 0说明你根本没有触发任何 X 源的检测问题可能出在复位约束或者综合设置上。后者告诉你哪些 X 源传播到了哪些可观测点每条 effect 记录通常包含源信号、影响信号、路径深度和反例波形编号。我个人的查看顺序是先扫一遍所有 effect 的严重级别优先处理跨模块传播的 X因为它们影响范围最大然后对每条 effect 打开对应的反例波形看在什么周期、什么条件下 X 会穿透到观测点最后回到 RTL看那段逻辑里有没有做保护比如是否有 casez 忽略项是否应该加 mask 逻辑或者是否需要加复位复位端。有些报告的inconclusive项看起来很吓人但其实可能只是分析的 cycle 数不够或者某些 X 源之间的交互关系没法在限定条件下判定。遇到这种情况不要慌先用prove -mode xprop -bounded跑一个有界范围确认一下再看要不要扩大范围。4. 常见问题与排查技巧实录4.1 仿真与 xprop 结果不一致先查约束和建模这是我最常被问到的问题也是我自己踩过最大的坑。明明 xprop 报告里 X 传播已经到状态机了可仿真里从头到尾没出现过一次 X或者反过来仿真里 X 满天飞xprop 却什么都不报。遇到这种不一致第一步永远是回头检查约束。xprop 里如果有个输入信号被错误地设成了常数那很多路径就永远不会被激活X 自然传不过去。反过来如果复位信号被建模成永远有效那设计一直处于复位状态X 当然不会影响功能但这种结果没有任何意义。另外要注意 X 源的建模方式。有些设计里用了带initial的寄存器仿真器在 0 时刻会把它初始化为某个值但 xprop 默认可能把这类寄存器也当成 X 源处理导致 xprop 比仿真“更悲观”。这种不一致不是 bug而是两者的初始状态假设不同。解决办法是在 setup 阶段明确设置-xprop_sources把不需要当作 X 源的寄存器排除掉。4.2 报告里的 X 传播链条又长又乱怎么快速定位xprop 报告有时候会给出一个很长的路径从一个触发器开始穿过组合逻辑又进另一个触发器再穿一堆逻辑最后到观察点。要手工分析这种路径特别费力气。我的习惯是反过来看从观察点往前追。观察点通常是状态寄存器的输入、输出使能信号、关键数据路径上的比较器输出。拿到反例波形之后先看观察点上 X 出现的周期然后倒推看哪些信号在那个周期也出现了 X再顺着这条链找到最早的那一级。这样通常比从头往后追快得多。还有一个技巧是用 JasperGold 的visualize界面或者把反例波形导到 Verdi 里看。我自己在命令行模式下干活比较多但遇到复杂的跨时钟域 X 传播时图形化界面确实能帮你更快看清时序关系。4.3 memory 和黑盒带来的 X 态烦恼memory 和 IP 黑盒是 xprop 用起来最别扭的地方。如果设计中有一个大的 SRAMxprop 默认会对它的存储单元建模状态空间会爆炸分析时间可能直接从几分钟变成几小时。而如果把它设成黑盒或者抽象模型X 源的定义又变得不精确。我的处理方法是如果不是验证重点就把 memory 抽象成一个带 X 输出的模型让它只输出一个自由变量看看这个 X 会不会污染下游逻辑如果 memory 本身就是要验证的模块那就老老实实把读端口和写端口的约束建好用 bounded 模式限制分析的周期通常能压住状态空间。还有一类情况是设计中调用了库里面的标准单元比如CLK_GATE_X2、DELAY_CELL这类单元如果库里没有对应的行为模型xprop 会把它当成黑盒。黑盒的输入输出之间没有逻辑关系约束工具就会保守地把输出也当 X 源导致大量误报。解决办法是在库文件里补充这些单元的抽象模型或者在 setup 阶段手动指定它们为 transparent 模型。4.4 性能调优从全量分析到分组拆解xprop 跑得太慢是所有用过它的人都会遇到的事。全量分析当然最理想但代价是状态空间可能大到完全跑不完。我调试时常用的降复杂度手段有三个。第一个是-bounded限制分析的 cycle 数。X 态这种东西通常不会会在几百个周期后才传播出来如果 50 个周期内都没有 effect那再往后出现问题的概率也很低所以先用一个有界范围做筛选是个高性价比的做法。第二个是分组分析。设计里 X 源往往有好几百个全放进去一起求解SAT 引擎的压力很大。我的做法是把 X 源按功能分组比如只分析“来自 UART 接收模块的 X 源”或者只分析“来自时钟域 A 的跨时钟域触发器”。分组之后每个任务的状态空间都小一个数量级跑完再把结果汇总。第三个是利用partition或者abstraction命令做层次化验证。把底层模块的验证结论当作上层模块的约束这样上层模块跑 xprop 时就不需要重复枚举底层内部的所有状态。这种方法一般在顶层模块特别大、底层模块已经单独验证过的情况下用能显著提速。几个值得长期养成的习惯最后再分享几个我后来一直坚持的用法。第一每次跑 xprop 前都把约束文件用 git 管起来因为约束变化对结果的影响比设计改动还大记录历史能帮你快速排查回归失败。第二别只跑一次全量证明建议从 bounded 跑到 unbounded 分阶段推进每轮都留好脚本方便回归。第三把 xprop 查出来的 X 传播问题跟设计团队对齐时一定要带上反例波形和观察点说明单纯贴一份 report 文本设计同学往往不知道从哪下手改。xprop 不是一个跑完就出结论的工具它更像是帮你把所有 X 态隐患系统性地逼到墙角再由你用 design knowledge 逐个判断它是假的干扰还是真的风险。这套方法我在几个项目里用下来X 态相关的前后仿对齐问题明显少了很多。如果你的验证流程里还没有这一环建议下次回归之前加上它。本文还有配套的精品资源点击获取