高度可配置寄存器生成器的自动形式化验证

SoC 中 IP 块的寄存器执行各种功能，其中大多数是 SoC 运行所必需的。相较于其他设计模块，寄存器实现的复杂度相对较低。然而，寄存器数量庞大且它们可以执行的各种潜在功能导致在使用手动方法时实现工作量巨大，尤其是当需要高度可配置时。因此，设计团队提出了一个内部寄存器生成器，以减少寄存器实现的手动工作量。该内部寄存器生成器不仅生成寄存器块，还生成总线相关块。同时，为支持各种需求，该生成器使用 41 种生成选项，具有高度可配置性。从验证角度来看，对于所有选项组合，手动方法无法获得完整的验证结果。除了可配置性带来的复杂性之外，寄存器验证仍然耗时，因为它面临两个广为人知的问题：规格的可靠性差以及多样化访问策略带来的复杂性。为处理高度可配置的特征以及这两个寄存器验证问题，我们提出了一种遵循模型驱动架构（MDA）的自动寄存器验证框架。基于我们的结果，寄存器验证中的人力工作量可以显著减少，从每个配置的 20 人天（20PD）降低到 3 人天，并且可以实现 100% 代码覆盖率。在项目执行期间，提出的验证框架发现了 11 个新的设计缺陷。