形式验证简介：分类、发展与适用场景
本文介绍了形式验证（Formal Verification）的基本概念、分类、发展历程以及适用场景。形式验证是一种通过数学分析的方法，对待测设计的状态空间进行穷尽分析的验证技术。相比于动态仿真，形式验证属于静态验证，不需要手动灌入激励，通过数学分析的方式对待测设计进行检查。
形式验证的分类
形式验证主要分为两大分支：
- 等价检查（Equivalence Checking）：用于检查不同设计阶段（如RTL代码和网表）之间的逻辑等价性。
- 属性检查（Property Checking）：基于PSL/SVA断言语言，通过对属性的假设、覆盖和断言语句分析，建立黄金模型，进行属性验证。
形式验证的发展
形式验证初次被EDA工具采用可以追溯到90年代，最初应用于RTL代码和门级代码的等价检查。随着技术的发展，形式验证逐渐衍生出适用于不同场景的各类工具，如组合等价检查、时序等价检查和事务等价检查等。
形式验证的适用场景
形式验证适用于以下场景：
- 小模块验证：适用于寄存器数量在40,000以内的模块验证。
- 可控模块：如有限状态机（FSMs）。
- 可观测模块：便于断言的书写，如AXI总线。
常见的适合形式验证的模块包括仲裁器、调度器、FIFO、中断控制器、DMA控制器、内存控制器、电源管理单元、时钟编程单元、总线、总线桥、总线结构（如CrossBar、NoC等）、缓存、缓存一致性协议建模与验证、数据传输、Pinmux、时钟控制器、复位控制器、系统死锁等。
总结
形式验证作为一种静态验证手段，通过数学分析的方法，能够穷尽分析所有可能的状态空间，适用于小模块的验证。随着设计复杂度的增加，形式验证在芯片设计中的应用越来越广泛，特别是在安全关键和高可靠性要求的场景中。