形式化方法综述

论文题目

硬件设计的形式化验证研究进展及趋势

• 形式化验证是确保硬件电路设计正确性的关键技术，它通过数学方法系统地验证硬件设计满足特定功能或特性要求。与基于测试的验证方法相比，形式化验证可以更完备的检查和发现潜在的错误，从而对于硬件系统的正确性给出更好的保证，提高产品质量与可信度。

微电子芯片设计的形式化验证工具

• Cadence公司的JasperGold
• Synopsys公司的VC Formal和Hector
• Siemens EDA公司（原MentorGraphics公司）的Questa Formal等

硬件设计的形式化验证的基础方法

• 约束求解
• 模型检测
• 定理证明

系统级验证

• 互联协议验证：使用高抽象层次模型。这个层次的形式化验证通常不涉及硬件电路细节，而是关注系统组件之间的高层次互联和通信协议的正确性。

行为级验证

• 形式化属性验证

门级验证

• 通常通过逻辑等价性检查（Logic Equivalence Checking）来确保门级电路优化前后，或者门级电路与行为级电路的逻辑功能一致性。

RTL级验证

• 可以使用基于模型检测或符号仿真技术的形式化属性验证（Formal Property Verification）或符号轨迹求值（Symbolic Trajectory Evaluation）等方法。

约束求解

• 包括SAT（布尔可满足性）求解器和SMT（可满足性模理论）求解器。
• SMT求解器：可以利用word-level的高层推理技术。位向量(BV)和算术理论是SMT的两种重要的背景理论，BV可自然的描述硬件和其上的操作，算术理论则可自然的描述软件上的不变式约束关系。

SAT串行求解技术

• 代表：冲突驱动的子句学习技术（Conflict-Driven Clause Learning，简称CDCL）。在过去的二十多年中，CDCL在框架层面变化不大，但其求解性能得到了大幅提高。这主要得益于各组件的提出和优化。
• 最近的热门求解器算法：深度混合求解算法。

SMT串行求解技术

• 求解技术为系统搜索算法且大幅依赖SAT求解。
• 可以分为积极和惰性算法：
  • 积极算法：将SMT问题经过高层化简之后直接转化为SAT公式求解，又被称为位展平（bit-blasting）。位向量SMT问题主要采用该类方法。
  • 惰性算法（目前用于求解SMT问题最常用的方法）：从SMT公式上抽象出一个命题逻辑骨架，采用CDCL算法求解该骨架，并在合适的时机调用相关的理论求解器。
• Boolector和其改进版本Bitwuzla是专注于求解SMT(BV)公式的求解器

并行求解技术

• 主流方法可以分为基于策略组合的方法和基于分治的方法： 对于SAT方法，目前效果最好的–>基于策略组合的方法。它在每个线程上调用不同的求解器或者同一个求解器的不同配置，来同时求解同一个SMT公式，利用了算法和策略间的互补性。 但是该技术的主要缺陷为无法从本质上减少问题求解难度，最优性能受到最优求解器参数的能力限制,比较典型的求解器有Mallob和PaInLeSS系列求解器,中科院蔡少伟团队ParKissat-RS与其自研框架改进版PRS求解器

• 基于分治法的SAT求解技术主要为cube-and-conquer技术。它利用look-ahead求解器将公式划分为众多子问题，然后采用CDCL求解器于不同线程各自求解子问题，在重划分技术的帮助下负载不均衡现象得以缓解，近期的代表求解器为德国Armin Biere团队的paracooba求解器

• SMT问题的并行研究较少，可以划分为基于策略组合的方法和基于分治的方法。与SAT不同的是，SMT领域的并行研究大多集中于分治策略，策略组合的方法研究较少，并且有人发现两者的混合技术能进一步改进求解能力

• 对于位向量问题，代表求解器为PBoolector，研究了基于bit-level和term-level的划分方法。算术理论方面， OpenSMT2包含了一种按需划分的方法，也引入了一种子句分享的技术；CVC5则引入了scattering/cube-and-conquer分治法和基于策略组合的方法。前述划分方法均主要基于bit-level，没有考虑到背景理论本身的结构性设计分割技术，近期，中科院蔡少伟团队提出了一套基于变量层级的分割技术AriParti，大幅提高了并行求解性能。

模型检测与形式化验证

1. 模型检测

模型检测（Model Checking）是一种将待验证的设计建模为状态机模型的技术。通过对状态空间的全面搜索，模型检测可以验证设计是否满足特定规格或属性。

分类

• 硬件模型检测：验证输入模型是布尔迁移系统（Boolean Transition System），即系统中的所有变量取值为0或1。
• 软件模型检测：接收其他类型输入模型的检测技术。

状态空间爆炸

模型的状态空间与其规模呈指数增长关系，这个问题被称为“状态空间爆炸”（State Space Explosion）。

符号化模型检测

20世纪90年代，研究者提出了模型的符号化（symbolic）方法，引入了更为紧凑的数据结构，如二进制决策图（Binary Decision Diagram，简称BDD）。

限界模型检查

限界模型检查（Bounded Model Checking，BMC）是首个将SAT技术引入模型检查的工作。该方法将模型和规范表示为符号化迁移系统，构造布尔公式并使用SAT求解器验证。

K-induction与插值模型检查

为了克服BMC的不完备性，研究者提出了两种改进方法：

• K-induction：通过K步推导验证系统的安全性。
• 插值模型检查（IMC）：在反例检测的基础上引入数学插值模型，用于判定模型满足规范。

IC3/PDR技术

IC3/PDR是一种新型的硬件模型检查技术，其优势在于不构造长的布尔公式，输入给SAT求解器的公式大小恒定，但数量较多。该方法还提供有限的正确性证明。

2. 定理证明

定理证明，尤其是交互式定理证明，是基于数学逻辑的形式化验证方法。通过与用户交互，逐步构建设计的数学证明，确保逻辑正确性。

应用与优势

• 应用：复杂硬件设计的验证，尤其是高安全性和可靠性要求的系统。
• 优势：高度灵活性和强大的表达能力，但学习成本和人力成本较高。

3. 硬件形式化验证

硬件形式化建模

• 处理器指令集建模：使用Sail、GRIFT、Forvis等语言进行指令集架构建模。
• 专用加速器建模：用类似于指令集建模的方法构建领域专用加速器的形式模型。
• 互联和存储建模：多核处理器系统的互联与存储形式化建模，用于验证性能和效率。

自动化建模

自动化建模方法如断言挖掘技术，能够高效生成形式化断言。

4. 门级验证

门级电路验证主要考虑逻辑等价性检查（Logical Equivalence Checking，LEC），分为以下两类：

• 组合电路检查（CEC）：基于BDD或SAT求解。
• 时序电路检查（SEC）：利用电路结构相似性或模型检测进行求解。

近年来，SAT求解器性能提升，使基于SAT的方法成为主流。

算术电路验证

算术电路（如乘除法器）验证是一个挑战，主要方法包括：

• 代数重写方法（SCA）：利用代数方法验证电路。
• 等价图方法：使用等价图建模电路，实现高层次的逻辑等价性检查。

5. 寄存器传输级验证

寄存器传输级验证以形式化属性验证为主，近年来的研究集中在以下方面：

1. 属性生成方法：基于高层次规约或机器学习生成验证属性。
2. 属性排序与分组：通过断言排序与分组优化验证效率。
3. 其他方法：符号轨迹求值、符号执行、合执行测试等方法。

自动生成属性

例如，RISC-V Formal用于生成指令集架构模型的形式化属性。普林斯顿大学的RTLCheck工具自动生成内存一致性模型的验证断言。

符号仿真技术

符号轨迹求值在工业界应用广泛，特别适用于浮点运算和存储单元的验证。

高层次验证

• 关于HLS（高层次综合）的验证。

系统级验证

• 组合验证（Compositional Verification）方法对于解决系统级验证中的规模问题尤为重要。在系统级的验证中，通常更多关注系统互联、协议验证等问题, 如片上网络、缓存一致性协议的验证等问题

安全验证

• 对于硬件安全属性的验证也是一个主要的形式化验证应用场景，近年来也有许多研究提出了多种方法来应对来自安全的挑战。对于瞬态执行侧信道的检测，其本质是检查信息流性质，即是否存在设计之外的信息流，除了模型检测方法之外，也有一些研究利用符号执行方法检查硬件设计中的信息流

国内研究现状

• 基础算法研究进展：
  • 约束求解。
  • 模型检测。
• 硬件形式化验证应用研究进展：
  • 建模与规约。
  • 逻辑等价性检查。
  • 寄存器传输级验证。
  • 高层次验证。

发展趋势与展望

• 自动化程度的提升。
• 人工智能的应用。
• 面向应用设计与调整验证方法。