如果一个属性表达式存在一个冗余的子表达式，子表达式没有影响到整个属性表达式的正确性，那么这个属性就叫空泛性属性。

例子：
      a |-> b，如果信号a无效，整个属性表达式仍然成立，那么这个属性表达式就叫空泛性属性。

1）属性本身具有歧义，子表达式的约束可能过紧，或者断言属性描述的设计不精确；

2）属性的问题有可能导致验证忽略了错误结果;

断言属性的例子如下：

AveMC的报告将显示：由于A1和A2这两个assumption约束属性冲突，导致了P0,P1,P2和P3都是空泛性断言属性。

空泛性断言属性可能会导致错误的证明结果，并且浪费了时间和精力，甚至会导致无法发现设计缺陷。AveMC的独有引擎（专利申请中）是检查空泛性属性，提高断言属性质量的完美解决方案。

检查内容分为两类：

1.软件可以自动生成覆盖率进行检查，也可以通过客户自定义生成覆盖率进行检查；

2.软件分析断言属性相关信号的每个状态和状态转移，检查断言属性自身的覆盖率漏洞；

奥卡思微电科技有限公司的PPC APP采用独有的引擎能够精确的分析断言属性的所有状态和跳转情况，为整个形式化验证提供了一个细颗粒度的属性质量分析方法。 PPC的结果可以用于形式化验证 signoff 和 bug hunting，帮助用户提高形式化验证的质量。