如何降低Formal assertion的复杂性呢？

分解一个复杂端到端断言属性的一种方法是基于模块化分级断言证明，如下图所示：

端到端属性被分解为分别验证每个子模块：

P1 验证 Sub1

P2 验证 Sub2

P3 验证 Sub3

我们使用P1已证明的属性作为P2断言证明的假设，所以模块化分级证明的要点就在于“后级模块的证明假设，一定要有前级断言的证明保证”，即“assume-guarantee”原则，这个原则在EDA仿真验证环境集成时也是适用的。

由于这种“assume-guarantee”原则的保证，上面3个模块如果都完成了证明，那么也相当于端到端的断言属性完成了证明。

分而治之，各个击破的方法，在大规模芯片验证中非常适用，但是也很容易引入质量风险。

审核编辑：刘清