芯片验证的挑战之一：理论上无限的验证空间

以一个简单的交通灯控制器为例。在经过一些市场调研之后，我们明确了交通灯控制器的原始需求：

1、当十字路口繁忙时，传感器要检测到这两条街上的交通状况。特定的时间内，两条公路上的交通灯应该是公平的。

2、每个方向灯应保持绿色1分钟。

在下图这个有缺陷的设计中，Main street上如果一直都有车辆在行驶，那么会无限锁死Elm street的交通。（这种问题在总线设计中可能很容易发生）。当然，这导致了Elm street的一场噩梦。验证工程师的工作是发现这些设计缺陷，确保最终产品符合预期。

数字芯片由很多上述这样的逻辑门组成，验证工程师的工作就是通过复杂的仿真检测出RTL实现和规格不一致的地方。

验证工程师面临的第一大挑战就是：RTL设计巨大的状态空间。

芯片中存储的内容（例如register和memory）称为芯片当前的状态，其和芯片当前的输入组合成巨大的验证空间。芯片中的下一状态由当前状态和设计输入决定。为了彻底验证芯片的功能，我们需要覆盖到芯片当前状态和设计输入的组合。

同样以上面提到的交通灯为例，只有2bit的内部状态，以及5个输入端口，所以总的验证空间为4*32个。

为了解决验证空间随着设计规模爆炸的问题，和其它解决复杂问题一样验证工程师采用各个击破的策略。一个典型的数字芯片可能有几十万个当前状态和输入信号。验证时没有必要只以整个芯片为研究对象，而是对设计进行划分，然后在设计、验证、物理实现各个方面分别处理，最后进行集成，方便管理，同时不管是在设计、验证还是物理实现上都处理地更加周全。

此外，芯片中可能还有许多状态是非法场景，即理论上或者业务上设计不可能进入的设计状态。例如上面的交通灯控制器的输出只可能是2’b01或者2’b10，即总的4*32个验证空间只有一半是合法的。

通过分析非法空间能够减少验证的工作量，同时定义illegal场景有时也能够断言出设计的故障。