介绍使用SVA的几个优势

1. SVA支持多时钟域（clock domain crossing (CDC)）逻辑，例如异步FIFO。

2. SVA是一种描述语言，可读性比较强。

3. 可以方便描述可执行的设计规格，而不是一些模棱两可的自然语言。

4. 可用来检查设计不允许的异常场景，或者设计必须满足的规格等等 

5. 支持开发参数化的check ，在不同模块或者不同项目之间复用，甚至在Formal工具和EDA仿真工具之间复用。

6. 可以通过“bind”方式加载到RTL上，不需要修改RTL。

7. 相比黑盒用例，SVA更容易定位。

8. “assert”可用于Formal属性证明。

9. “assume”可用于Formal输入场景约束

10. “cover”可用于Formal覆盖率

最后，验证环境中每一个约束都应该是一个assert，需要在集成验证环境或者周边模块验证环境中检查。

审核编辑：刘清