附录 A术语表

以下是 JasperGold 形式验证常用术语的中英文对照和简要说明。

大部分条目来自官方术语表 glossary.pdf。少数术语（亚稳态、同步器、汇聚、发散、毛刺、RDC、准静态、互斥切换、证明缓存、有界模型检测等）并未收录在官方术语表中，其定义改从真正定义它们的 App 手册中提取。凡是逐字核对过出处的条目，都在末尾用 [来源] 标注该出处（[glossary] 即官方术语表本身），具体文档见页面底部的来源卡片。

英文术语	中文	说明
`Abstraction`	抽象	移除不相关逻辑以简化形式证明的技术。
`Assertion`	断言	描述设计必须满足的行为的 SVA/PSL 语句（assert）。
`Assumption`	假设	描述输入环境约束的语句（assume），限定合法输入空间。
`Bounded Model Checking`	有界模型检测	一类在有限深度内搜索反例/覆盖点的算法。例如 bug-hunting 引擎 L 就基于有界模型检测算法与状态选择启发式的组合，在可达状态空间的子集中做智能遍历，从而到达常规有界模型检测算法难以到达的深状态。[Engine Selection]
`BPS`	行为属性综合	Behavioral Property Synthesis，从仿真波形自动生成属性候选。[命令参考 App 开关表]
`CDC`	时钟域交叉	Clock Domain Crossing，信号在不同时钟域之间传递的情况。
`COI (Cone of Influence)`	影响锥	影响某个属性的所有逻辑集合，JasperGold 自动缩减 COI 提高效率。
`Convergence`	汇聚（数据一致性）	一组信号、或同一信号的不同比特，来自相同或不同的时钟域，在同步之后于目的时钟域汇聚进同一块组合逻辑。[CDC UG]
`Counterexample`	反例	违反断言的输入序列，JasperGold 生成波形用于调试。
`Cover`	覆盖	描述设计应该能到达的状态（cover），用于衡量验证完备性。
`CSR`	控制状态寄存器	Control/Status Register，通过 CSV 自动验证寄存器行为。
`Cut Point`	切割点	官方术语表中 cut points 条目指向 `stopat`：即用 `stopat` 切断信号原有的驱动逻辑，使其成为自由变量。[glossary]
`Design Under Verification (DUV)`	待验证设计	正在被验证的硬件设计。
`Divergence`	发散	一路逻辑发散到多条同步路径，可能造成功能错误：传播延迟与不同的亚稳态稳定时间会让本应同时生效的信号在不同时刻才开始起作用。规避办法是先同步、再把单个信号扇出到各个下游。[CDC UG]
`Dynamic Formal`	动态形式验证	结合仿真和形式验证的混合技术。
`Engine`	证明引擎	用于 Visualize 和运行属性证明的 JasperGold 工具模块。产品内置多个证明引擎，任意组合使用以得到证明（proof）、见证（witness）或反例（counterexample）；其中既有 SAT（可满足性）类和 BDD（二元决策图）类引擎，也有在这些方法上做变化的其他引擎。每个引擎可针对某个 engine mode 单独开关。引擎以字母命名，如 B、Hp、Ht、I、K、L、N、Tri 等。[glossary]
`Engine Mode`	引擎模式	一个或多个引擎的组合配置。
`Equivalence Checking`	等价检查	验证两个设计在功能上是否等价（如 RTL vs Netlist）。
`Formal Scoreboard`	形式记分板	在形式验证中自动检查数据传输顺序/完整性的机制。
`Formal Testplan`	形式验证计划	定义形式验证目标和属性的计划文档。
`Formal Verification`	形式验证	使用数学方法穷尽证明设计满足属性的验证技术。
`FSV`	功能安全验证	Functional Safety Verification，面向 ISO 26262 的故障分析。
`Full Proof`	完整证明	属性在所有可达状态下成立（unbounded proof）。
`Functional Safety`	功能安全	系统在故障情况下仍能维持安全操作的能力（ISO 26262）。
`Glitch`	毛刺	CDC 路径上的任何逻辑都可能产生毛刺并在下游造成功能错误：不同路径的延迟差会让信号瞬间跳变，这个跳变可能被采样时钟捕获，导致下游逻辑行为异常。[CDC UG]
`High-Level Requirements`	高层需求	架构级别的设计规格。
`Induction`	归纳法	一种数学原理：让 JasperGold Apps 先分析有界的 trace，再用这些有界 trace 的信息推断出关于任意长 trace 的结论。[glossary]
`Interface Requirements`	接口需求	模块接口的协议规格。
`Justify`	纳入分析区域	把设计逻辑纳入进来、从而构建分析区域的过程，用于 design tunneling（设计隧道）流程。[glossary]
`Liveness Property`	活性属性	描述好事情最终会发生的属性（如：请求最终会被授权）。
`LPV`	低功耗验证	Low Power Verification，验证 UPF/CPF 电源管理。[命令参考 App 开关表 + 平台指南 p36]
`Manual Abstraction`	手动抽象	用户手动定义抽象模型来简化证明。
`Metastability`	亚稳态	每个触发器都有建立时间与保持时间；当建立/保持条件被违反时，触发器输出变得不稳定，并在一段不可预测的延迟后才稳定到 1 或 0，这一现象称为亚稳态。异步设计中无法避免亚稳态，但可以用同步器阻止亚稳态值向前传播。[CDC UG]
`Model Checking`	模型检测	自动验证有限状态系统是否满足时序逻辑属性的技术。
`Mutually Toggle Exclusive (MUTEX)`	互斥切换	把一组源信号（源触发器的输出）声明为互斥，即同一时刻只有其中一个可以翻转。当多个信号汇聚到目的域的同一组合逻辑、但同时最多只有一个会翻转时，据此可以安全地豁免 convergence / re-convergence 违规——声明后工具会尝试自动豁免。命令：`check_cdc -signal_config -add_exclusive {A_reg B_reg C_reg}`。[CDC UG p77]
`Non-Temporal Assertion`	非时序断言	不涉及时序关系的断言（组合逻辑检查）。
`Overconstraint`	过约束	假设太强，排除了合法输入行为，可能导致空洞证明。
`Partial Proof`	部分证明	在有界范围内成立但未完全证明的属性。
`Proof Accelerators (PAs)`	证明加速器	Cadence 预构建的常见硬件结构验证模型（Cache/FIFO/Scoreboard 等）。
`Proof Orchestration`	证明编排	JasperGold 自动选择和调度多个引擎的策略。
`Proof Cache`	证明缓存	SEC 中用于回归运行的机制：尽量复用此前已获得的证明结果以节省资源。SEC 按属性做 COI 校验，要求目标属性的 COI 没有变化；默认关闭，用 `set_sec_autoprove_use_proof_cache true` 开启。[SEC UG]
`ProofGrid`	分布式证明	在服务器集群上并行运行多个证明引擎。
`Property`	属性	用形式语言描述的设计行为规范（assert/assume/cover）。
`PSL`	属性规格语言	Property Specification Language，IEEE 标准断言语言。
`Quasi-Static`	准静态信号	CDC 分析中可声明为常量或准静态的信号，在 configuration 阶段用 `check_cdc -signal_config` 指定（如 `-add_static`）。汇聚（convergence）告警的排查手段之一就是确认其中是否有信号本应是常量或准静态。[CDC UG / CDC Ref]
`Reset Domain Crossing (RDC)`	复位域交叉	复位分析会分析设计的复位树并识别两类问题：① 复位信号从一个时钟域跨到另一个时钟域；② 同一时钟域内触发器之间存在复位域交叉。两种场景都可能引发亚稳态问题，因此都会被报为复位违规。[CDC UG]
`SAT (Satisfiability)`	可满足性	部分证明引擎在 JasperGold Apps 中所采用的一类算法方法。官方术语表中另有 BDD（binary decision diagram）类引擎与之并列。[glossary]
`Safety Property`	安全属性	描述坏事情永远不会发生的属性（不变量检查）。
`SEC`	时序等价检查	Sequential Equivalence Checking。
`SPV`	安全路径验证	Security Path Verification，验证信息不泄露到非安全域。[命令参考 App 开关表]
`SVA`	SystemVerilog 断言	SystemVerilog Assertions，最广泛使用的断言语言。
`Superlint`	超级 Lint	结合静态 Lint 和形式证明的设计检查。
`Synchronizer`	同步器	用于阻止亚稳态值向前传播、避免亚稳态导致的数据丢失或损坏、以及重汇聚相关数据一致性问题的电路结构。CDC App 文档中称之为 Common Synchronization Schemes。[CDC UG]
`UNR`	覆盖率不可达分析	Coverage Unreachability，形式证明未覆盖点不可达。
`Visualize`	波形调试	JasperGold 集成波形调试环境。
`X-Propagation`	未知态传播	X 值在设计中传播导致的问题检测。

来源文档

glossary.pdf（标 [glossary] 的条目）
jaspergold_cdc_userguide.pdf / jaspergold_cdc_reference.pdf（标 [CDC UG] / [CDC Ref] 的条目）
jaspergold_sec_userguide.pdf（标 [SEC UG] 的条目）
jaspergold_engine_selection.pdf（标 [Engine Selection] 的条目）