设计的状态空间主要由设计内部的时序单元和输入数量决定，包括触发器、锁存器和存储器。
理论上，对于一个具有n个寄存器、m个输入的设计而言，其状态空间就是2^（m+n）。
举个例子，对于具有10个寄存器、10个输入的设计而言，那么状态空间就是2^20。一般实际的设计中的状态空间要比这个多得多。
我们可以想象现实设计中可能存在的时序单元数量以及处于所有状态下的输入。鉴于这个巨大的状态空间，当前的Formal EDA 工具通常可以在大约 40,000 个触发器的设计上运行 FPV，可以分析数百周期的设计行为。
RTL设计的实际仿真行为可以看作是从复位开始通过某些状态空间的曲折路径。
- 对于EDA仿真工具，每次都会遍历状态空间中的一个点到另一个点，形成一条轨迹。
- 对于Formal工具则会并行地分析所有状态轨迹。
从上图可以看出，一次EDA仿真过程中设计从复位状态（R）开始，第一个周期后到达状态{1} ，第二个周期后到达状态{2} ，直到达到最终状态。FPV则会探索每个时钟周期中所有可能的状态，如图中不断增长的椭圆所示。
如果FPV工具达到了full proof，就说明它已经有效地探索了所有这些周期，以及覆盖了所有可能状态空间。如果FPV无法做到full proof（仅仅是有界证明，Bounded proof），其覆盖的状态空间依然比EDA仿真要多得多。
上图中最外圈就是FPV证明边界，也就是最大周期数。
由于逻辑的复杂性不同，图中的每个周期对应的区域都不相等。例如一个设计初始化需要256个周期，之后就进行一个周期的复杂操作已完成设计功能，这样前256个周期的就会遍历地非常快速，最后的周期的状态空间就会爆炸。
这种呈指数增长的状态空间是FPV复杂度问题的主要来源，这也是阻碍我们使用FPV进行完全收敛sign off的罪魁祸首。
相比FPV，一般FEV所需要处理的复杂度相对比较小，但是依然是一个非常大的计算量和内存空间。
作者：验证哥布林
来源：芯片设计验证微信号
推荐阅读
更多数字IC设计技术干货等请关注数字芯片实验室专栏。添加极术小姐姐（微信：aijishu20)微信可申请加入IC设计交流群。
