4.1 断言与属性规范语言（SVA）基础
4.1.1 问题背景：怎样把协议规范“告诉”形式化引擎？
在仿真验证中，断言是“监视器”：它观察信号行为，发现违规时报告。但在Questa Formal中，断言的定位发生了质变——它们是形式化引擎的输入规范。引擎以断言为证明目标，通过数学推理穷举所有输入序列，验证属性在整个状态空间中是否成立。
因此，SVA（SystemVerilog Assertions）不只是“加几句检查”，它是形式化验证的建模语言。你需要用SVA精确表达“协议允许什么、禁止什么、信号之间应该在什么时序下相互响应”。