使用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，需要在集成验证环境或者周边模块验证环境中检查。

Every design assumption is an assertion