附录 A术语表

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

英文术语	中文	说明
`Abstraction`	抽象	移除不相关逻辑以简化形式证明的技术。
`Assertion`	断言	描述设计必须满足的行为的 SVA/PSL 语句（assert）。
`Assumption`	假设	描述输入环境约束的语句（assume），限定合法输入空间。
`BMC (Bounded Model Checking)`	有界模型检测	将证明问题展开为 k 步 SAT 问题，寻找有限长度内的反例。
`BPS`	行为属性综合	Behavioral Property Synthesis，从仿真波形自动生成属性候选。
`CDC`	时钟域交叉	Clock Domain Crossing，信号在不同时钟域之间传递的情况。
`COI (Cone of Influence)`	影响锥	影响某个属性的所有逻辑集合，JasperGold 自动缩减 COI 提高效率。
`Convergence`	汇聚	多个 CDC 信号汇聚到同一逻辑，需要保证数据一致性。
`Counterexample`	反例	违反断言的输入序列，JasperGold 生成波形用于调试。
`Cover`	覆盖	描述设计应该能到达的状态（cover），用于衡量验证完备性。
`CSR`	控制状态寄存器	Control/Status Register，通过 CSV 自动验证寄存器行为。
`Cut Point`	切割点	在形式验证中切断信号以减少复杂度的技术。
`Design Under Verification (DUV)`	待验证设计	正在被验证的硬件设计。
`Divergence`	发散	一个信号分发到多个同步器，可能导致不一致延迟。
`Dynamic Formal`	动态形式验证	结合仿真和形式验证的混合技术。
`Engine`	证明引擎	执行形式证明的算法模块（BMC/PDR/K-Induction/BDD 等）。
`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`	毛刺	组合逻辑输出上的短暂脉冲，在跨时钟域时可能被错误采样。
`High-Level Requirements`	高层需求	架构级别的设计规格。
`Induction`	归纳法	先证基础情况（初始状态成立），再证归纳步骤（若 k 成立则 k+1 成立）的证明方法。
`Interface Requirements`	接口需求	模块接口的协议规格。
`Justify`	正当化	在形式验证中证明某个值或路径是合法可达的。
`Liveness Property`	活性属性	描述好事情最终会发生的属性（如：请求最终会被授权）。
`LPV`	低功耗验证	Low Power Verification，验证 UPF/CPF 电源管理。
`Manual Abstraction`	手动抽象	用户手动定义抽象模型来简化证明。
`Metastability`	亚稳态	触发器在建立/保持时间违例时输出进入不确定状态。
`Model Checking`	模型检测	自动验证有限状态系统是否满足时序逻辑属性的技术。
`Mutually Toggle Exclusive (MUTEX)`	互斥切换	多个信号互斥切换（同一时间只有一个激活）。
`Non-Temporal Assertion`	非时序断言	不涉及时序关系的断言（组合逻辑检查）。
`Overconstraint`	过约束	假设太强，排除了合法输入行为，可能导致空洞证明。
`Partial Proof`	部分证明	在有界范围内成立但未完全证明的属性。
`Proof Accelerators (PAs)`	证明加速器	Cadence 预构建的常见硬件结构验证模型（Cache/FIFO/Scoreboard 等）。
`Proof Orchestration`	证明编排	JasperGold 自动选择和调度多个引擎的策略。
`Proof Cache`	证明缓存	缓存证明结果以加速重跑。
`ProofGrid`	分布式证明	在服务器集群上并行运行多个证明引擎。
`Property`	属性	用形式语言描述的设计行为规范（assert/assume/cover）。
`PSL`	属性规格语言	Property Specification Language，IEEE 标准断言语言。
`Quasi-Static`	准静态信号	变化极慢（如配置寄存器），在 CDC 分析中不认为是跨时钟域问题。
`Reset Domain Crossing (RDC)`	复位域交叉	不同复位域之间的信号交叉。
`Safety Property`	安全属性	描述坏事情永远不会发生的属性（不变量检查）。
`SEC`	时序等价检查	Sequential Equivalence Checking。
`SPV`	安全路径验证	Security Path Verification，验证信息不泄露到非安全域。
`SVA`	SystemVerilog 断言	SystemVerilog Assertions，最广泛使用的断言语言。
`Superlint`	超级 Lint	结合静态 Lint 和形式证明的设计检查。
`Synchronizer`	同步器	处理跨时钟域信号的电路（如 2-FF、FIFO、Handshake）。
`UNR`	覆盖率不可达分析	Coverage Unreachability，形式证明未覆盖点不可达。
`Visualize`	波形调试	JasperGold 集成波形调试环境。
`X-Propagation`	未知态传播	X 值在设计中传播导致的问题检测。

来源文档

glossary.pdf