4 断言与属性规约基础

4.1 问题背景：为什么总线验证需要断言

AXI/AHB/APB 协议规则大多以“时序图 + 文字描述”的形式存在于规范文档中。若只依赖人工波形比对，跨周期边界、握手中断、状态非法切换等问题极易遗漏。断言（Assertion）将协议时序规则转换为机器可自动判定的属性（Property），在仿真与形式化验证中持续监控信号行为，一旦违规立即报告。

本章聚焦断言与属性规约的底层原理，帮助你在总线验证项目中建立清晰、可维护的 SVA（SystemVerilog Assertions）检查架构。

4.2 核心概念：五个关键词

• 断言（Assertion）：对属性实例的检查执行体，负责监控、判定并输出违规报告。
• 属性（Property）：由布尔表达式与时间运算符共同描述的一段完整时序行为。
• 序列（Sequence）：最基本的时序事件匹配单元，描述信号沿时钟周期展开的变化。
• 时钟与采样：SVA 所有时序建立在时钟事件上；信号在时钟边沿前的采样点被捕获，避免竞争。
• 覆盖与验证：cover property 回答“场景是否发生”，assert property 回答“规则是否成立”。