📄️ SystemVerilog Assertion：从时序描述到可维护的断言
SystemVerilog Assertions（SVA）的价值不在于堆叠复杂语法，而在于把接口在时间上的承诺写清楚：在哪个时钟采样、复位时是否停止检查、什么事件触发检查，以及之后哪些状态必须或禁止出现。
📄️ 形式验证：先建模环境，再证明设计
形式验证（Formal Verification）把 RTL、环境约束与属性转成逻辑问题，尝试在可达状态空间中证明规则恒成立，或给出一条反例路径。它和随机仿真互补：仿真适合运行真实软件场景，形式验证适合检查难以覆盖的极端状态、异常组合和控制路径。