引言
随着集成电路设计的复杂性不断增加，确保硬件系统的正确性和可靠性变得愈发重要。传统的验证方法往往依赖于仿真技术，这种方法在覆盖率和效率上存在局限。而形式化验证作为一种基于数学逻辑的验证技术，提供了一种系统化的方法来证明设计的正确性。在 CIRCT 生态中也有两款相关工具，它们分别是逻辑等价性检测工具–circt-lec 和有界模型检测工具–circt-bmc，这些工具为硬件设计的验证提供了有效的支持。
形式化验证概述
形式化验证（Formal Verification）是一种利用数学分析方法来验证硬件设计行为与规定标准一致性的技术。与依赖测试和仿真的传统验证方法不同，形式化验证通过数学证明确保硬件设计在所有可能场景下均能正确运行。这意味着它会分析所有可能的状态和输入组合，以识别设计中潜在的违反预期行为的情况。而传统方法则是一种概率性策略，旨在测试尽可能多的场景，但受限于时间和资源，通常只能覆盖硬件设计行为的一部分。
虽然形式化验证的目的是验证硬件设计中所有可能的行为，但由于硬件资源和设计复杂性等因素，这一过程面临挑战。尤其是在大规模硬件设计中，由于这些限制，并非所有断言都能得到充分证明。因此，形式化验证通常被有选择性地应用于关键组件，而对其余部分则采用仿真测试。尽管如此，形式化验证在发现潜在错误方面，尤其是在仿真中可能被遗漏的边界情况时，展现出显著优势，从而提供更高的安全性、可靠性和正确性。
以下是两种常见的形式化验证模式：
- 逻辑等价性检测（Logical Equivalence Checking，LEC）
逻辑等价性检测可用于比较两个相同或不同抽象层次的设计，以识别它们在功能上的差异。LEC 可以进一步细分为两个主要领域：
- 组合逻辑等价性检测（Combinatorial equivalence checking，CEC）：CEC 主要用于验证经过逻辑综合后的电路设计是否与输入的 RTL 描述相同。它确保在进行逻辑综合或其他门级变换后，电路的功能未受到影响，主要比较的是转换后的电路设计中的寄存器与原始寄存器在组合逻辑行为上是否保持一致；
- 时序逻辑等价性检测（Sequential equivalence checking，SEC）：SEC 是一种新兴技术，用于比较两个在时序上完全不同的电路设计。即使两个设计在时序上存在显著差异，SEC 仍然能够评估它们在功能上的等价性。该技术允许将未定时或部分定时的模型与 RTL 模型进行比较，以及用于比较经过重定时以改善功耗或其他特性的 RTL 模型。由于 SEC 允许在不同的时序下进行比较，因此在 HLS 的应用中显得尤为重要
LEC 作为一种重要的形式化验证技术，通过比较相同或不同抽象层次的设计，确保它们在功能上的等价性。CEC 专注于逻辑综合后的设计与原始 RTL 描述之间的等价性，而 SEC 则关注具有不同时间特性的电路是否等价。这两种方法共同促进了电路设计中的正确性和可靠性。
- 有界模型检测（Bounded Model Checking，BMC）
有界模型检测的基本思想是限制执行路径的长度，通过设定一个整数 k 来搜索可能的反例，即系统错误。如果在当前边界 k 下未发现反例，则增加 k 的值，直到发现反例或到达某个预先设定的上限。即，BMC 通过将模型检测问题转化为可满足性问题，并利用现代 SAT 求解器的强大能力，为系统验证提供了一种高效且实用的方法。通过设定边界并逐步增加，BMC 能够有效地识别潜在缺陷，同时避免传统模型检测方法中常见的状态空间爆炸问题。
形式化验证在硬件设计中具有重要性，主要体现在以下几个方面：
- 验证空间完备性：当所有输入端的每个信号，每一时钟周期都只有 0 或 1 两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对 RTL 转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历；
- 验证环境简单高效：不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述 Property，进而进行输入场景遍历和推导证明；
- 覆盖率收集自动化：形式化验证工具能够自动完成覆盖率收集，基于算法和模型的方案无需人工定义功能覆盖。这种自动化大大降低了因人为失误导致覆盖率准确度不高的风险；
- 提供最小反例：当形式化验证发现设计缺陷时，它能够迅速提供一个最小反例，描述导致错误状态所需的最小条件。这一特性使得设计者能够更高效地调试和修正问题，减少了传统仿真方法中反复尝试的时间成本；
- 适应性强：形式化验证不仅适用于简单电路，也能有效应对大规模和复杂系统中的安全性和功能性问题。它为开发人员提供了强有力的支持，使他们能够在高集成度的环境中保持设计的正确性。
综上所述，形式化验证通过提供全面、准确和高效的验证手段，在现代硬件设计中扮演着不可或缺的角色，确保了设计的可靠性和安全性。
逻辑等价性检测
LEC 工作原理可以分为几个关键步骤：
- 设置模式：在这一阶段，设计者需要定义待比较的两个电路模型。这些模型可以是相同或不同抽象层次的设计，例如，一个是 RTL 描述，另一个是经过逻辑综合后的电路。设置模式确保输入信号和输出信号的映射关系明确；
- 映射模式：接下来，LEC 工具会对两个电路进行关键点映射，即识别出电路中重要的逻辑节点和信号。这些关键点通常包括寄存器的输入和输出、时钟信号等。通过确保这些关键点的一致性，设计者可以初步判断两个电路的逻辑结构是否相似；
- 比较模式：在比较阶段，LEC 工具会使用数学方法，如布尔代数、真值表或决策图对两个电路进行详细比较。这一过程通常涉及构建一个 Miter 连接电路，将待比较电路的输出通过异或门连接，以检测其输出是否始终为零。如果 XOR 门的输出在所有输入情况下都为零，则说明两个电路在功能上是等价的；否则，工具将提供反例，指出不等价的输入条件。
LEC 的优势之处：
- 高效性：LEC 能够显著加快验证过程，与传统门级仿真相比，能够在数倍的速度下完成对百万门级 ASIC 和 FPGA 的全面验证。这种高效性使得设计者能够更快地发现和修复潜在缺陷；
- 降低缺陷遗漏风险：通过独立的验证技术，LEC 能够有效降低遗漏严重缺陷的风险。它可以在设计流程的各个阶段进行功能验证，确保每个设计版本都符合规格要求；
- 全面覆盖：LEC 通过比较不同抽象层次的设计，确保它们在功能上的等价性。这种全面性使得设计者能够验证逻辑综合后的电路是否与原始 RTL 模型相符，从而提高了设计的可靠性；
- 适应复杂电路：LEC 能够处理复杂的数据通路和逻辑结构，确保即使在高度复杂的电路中也能实现准确的等价性检查，这对于现代集成电路设计至关重要；
- 自动化与简化：现代 LEC 工具通常具有自动化功能，可以减少人工干预，降低人为错误的可能性。通过算法和模型自动收集覆盖率，进一步提高了验证的准确性和效率。
LEC 的不足之处：
- 状态空间限制：尽管 LEC 可以处理复杂电路，但在某些情况下，特别是当电路规模非常大时，状态空间可能会变得庞大，从而导致计算资源消耗过高，验证时间延长；
- 对输入敏感：LEC 对输入信号的一致性要求较高。如果待比较的两个电路在输入端存在差异，例如增加了新输入，则可能导致等价性检查失败，而实际上这并不意味着电路本身存在问题；
- 依赖于模型质量：LEC 的有效性依赖于输入模型的准确性。如果输入模型存在错误或不完整，那么即使使用了 LEC，也无法保证检测结果的可靠性。
LEC 的应用场景：
- 集成电路设计验证：在芯片设计过程中，设计者需要确保经过逻辑综合的电路与原始的 RTL 描述在功能上等价。例如，许多半导体公司使用 LEC 工具来验证其复杂电路设计，以确保在逻辑综合和优化过程中没有引入错误；
- 硬件故障检测：LEC 可以用于检测硬件故障，通过比较正常工作状态下的电路与故障状态下的电路，确保故障不会导致功能上的不一致。这种方法在制造过程中可以帮助识别潜在的生产缺陷；
- 自动化测试生成：在软件和硬件共同开发的环境中，LEC 可以用于生成测试用例，确保软件与硬件接口的一致性。通过验证软件控制下的硬件行为与预期的一致性，减少了手动测试的工作量；
- 设计变更验证：在电路设计迭代过程中，LEC 被用于验证设计变更是否影响了原有功能。通过比较修改前后的电路，可以确保新版本仍然满足原有规格。
有界模型检测
BMC 工作原理可以概括为以下几个步骤：
- 模型表示：首先，将待验证的系统建模为有限状态机，通过状态间的转换关系来描述系统的行为。这个模型通常包括状态集、状态之间的转换关系以及每个状态上使一组原子命题为真的集合；
- 设定边界：在进行验证时，设定一个整数 k 作为边界，表示检查系统在 k 步内是否存在违反性质的路径。这个边界限制了搜索的深度，使得验证过程变得可控；
- 构建逻辑公式：将系统的状态转换关系与待验证的性质结合，构建一个布尔逻辑公式。该公式通常是通过将状态转换与线性时序逻辑或其他时序逻辑规范结合而成；
- 编码为 SAT 问题：将构建的布尔公式编码成可满足性问题。这一步骤是 BMC 的核心，利用 SAT 求解器来判断该公式是否可满足。如果 SAT 求解器能够找到一个可满足的解，则说明存在一个反例，即在 k 步内找到了违反性质的路径；
- 反例分析：如果 SAT 求解器返回可满足解，BMC 将生成一个反例，描述导致错误状态所需的输入条件。这一反例可以帮助设计者快速定位问题并进行修复；
- 增加边界：如果在当前边界 k 下未发现反例，则增加 k 的值，重复上述步骤，直到找到反例或达到预设的上限。这种逐步增加边界的方法使得 BMC 能够有效地探索设计空间，同时避免传统模型检测中的状态爆炸问题。
BMC 的优势之处：
- 高效利用 SAT 求解器：BMC 能够将验证问题编码为可满足性问题，充分利用现代 SAT 求解工具的特性。这种方法有效地提升了模型检验的变量数，使得处理更大规模的设计成为可能；
- 快速发现反例：BMC 采用深度优先搜索策略，能够迅速找到路径最短的反例。这一特性使得设计者能够更快地定位和修复潜在问题，从而提高开发效率；
- 克服状态爆炸问题：通过设定边界阈值 k，BMC 有效地限制了搜索空间，避免了传统模型检测方法中常见的状态爆炸问题。这使得 BMC 在处理复杂系统时更加高效和实用；
- 自动化与简化：BMC 不需要复杂的验证环境，能够自动化执行验证过程。这种自动化特性降低了人工干预的需求，减少了人为错误的可能性，提高了验证的准确性和可靠性；
- 适应多种应用场景：BMC 不仅适用于硬件设计，还广泛应用于软件验证、网络协议安全性分析等多个领域。这种灵活性使得 BMC 成为一种通用的验证工具；
- 支持增量验证：BMC 允许逐步增加边界 k 的值，从而可以在不同复杂度下进行验证。这种增量方法使得设计者可以根据需要调整验证深度，以便在合理时间内获得有效结果。
BMC 的不足之处：
- 有限的验证能力：BMC 主要用于验证有限步行为，能够检查的性质相对有限。它通常只能验证全称属性，如线性时序逻辑（Linear Temporal Logic）和计算树逻辑（Computation Tree Logic），而对于更复杂的性质可能不适用；
- 依赖于边界设置：BMC 的有效性高度依赖于边界 k 的选择。如果选择不当，可能导致无法发现潜在缺陷，或是需要多次调整边界以找到反例，从而影响效率。
BMC 的应用场景：
- 硬件设计验证：BMC 广泛应用于集成电路的设计验证，确保逻辑综合后的电路与原始设计在功能上的一致性。例如，许多半导体公司利用 BMC 工具验证复杂的 ASIC 和 FPGA 设计，以快速发现潜在缺陷；
- 软件验证：在嵌入式系统中，BMC 被用于验证 C/C++ 程序的正确性。例如，CBMC 工具能够直接对嵌入式软件进行验证，检查实现中的可能漏洞，并确保程序符合规范。这种方法避免了传统模型检测中需要抽象建模的问题，提高了验证效率；
- 网络协议分析：BMC 被应用于无线抄表路由协议的验证，通过对协议实现进行模型检测，确保其网络层接收函数与协议规范相符。这种应用展示了 BMC 在网络安全和可靠性分析中的重要性；
- 故障检测与测试：有界模型检测也用于片上网络的固定型故障在线测试。通过在扩展有限状态机上运行 BMC，生成引导序列并自动生成测试向量，从而实现对固定型故障的高覆盖率检测。这一方法显著提高了故障检测的效率和准确性；
- 实时调度系统：BMC 还被应用于实时调度算法的验证，通过对调度策略进行模型检测，确保系统能够在规定时间内完成任务，提高了实时系统的可靠性。
CIRCT 中的形式化验证
相关背景知识
-
Z3：Z3 是一种 SMT（Satisfiability Modulo Theories）求解器，能够检查逻辑表达式的可满足性。它支持多种数据类型，如布尔值、整数、实数、数组和位向量等。Z3 在工业界和学术界都有广泛应用，包括软件/硬件验证、程序分析、安全性分析、混合系统分析等。它也被用于 CTF（Capture The Flag）竞赛中的密码学和逆向工程问题；
-
SMT-LIB：该项目旨在通过提供标准化的工具和资源，推动可满足性模理论及其求解器的发展。以及通过定义一种用于描述和交互 SMT 问题的通用语言，使得不同的 SMT 求解器能够更容易地进行比较和评估。SMT-LIB 的主要组成部分如下：
- 输入输出语言规范：它定义了求解器所需遵循的输入输出格式。这使得用户可以使用相同的语法与不同的求解器进行交互；
- 背景理论：它建立了一系列背景理论，如算术、数组、位向量等，这些理论增强了 SMT 公式的表达能力。背景理论允许用户在更复杂的逻辑框架下建模问题；
- 基准测试库：它还提供了一个包含大量测试用例和基准问题的库，用于评估和比较不同 SMT 求解器的性能；
尽管 SMT-LIB 格式是被所有 SMT 求解器所支持的标准化格式，但是依旧存在以下不足之处：
-
这种格式是静态化的，并且难以与其他求解器进行交互，以及难以使后续针对结果添加的新的断言依赖于当前求解器的输出；
-
该格式无法有效地结合符号执行、具体执行和调试工具；
-
该格式还无法有效地利用 LLVM JIT 编译以直接获取结果，而是需要调用外部的求解器（如 Z3），或者为其添加编译时依赖；
-
SMT 方言：该方言旨在为 MLIR 提供统一的接口，以便直接表达 SMT 问题，从而实现与其他 MLIR 方言和优化过程的无缝集成。它遵循 SMT-LIB standard 2.6，并包含一些除该标准之外的常用的 SMT 求解器的特性。相较于将 SMT 问题直接打印输出为 SMT-LIB 格式或输出到求解器，定义 SMT 方言以表示 SMT 问题有以下优势：
- 通过利用 MLIR 中的 passes、操作构建器和重写模式，能够更加高效地构建和优化 SMT 公式；
- 不需要为 CIRCT 添加对 SMT 求解器的链接依赖，只需为 JIT 运行器提供库的路径作为其参数，或者手动将生成的二进制文件与指定的库进行链接；
- 在 CIRCT 中，为 SMT 问题提供统一的中间表示，且可与其他方言混合使用，以及使添加新的后端更加容易；
CIRCR 中的 LEC 工具：circt-lec
.sv 源代码：
module mulByTwo(input int in,
output int out);
assign out = in * 2;
endmodule
module add(input int in,
output int out);
assign out = in + in;
endmodule
转换为 Core 方言后：
// RUN: circt-verilog --ir-hw %s
module {
hw.module @mulByTwo(in %in : i32, out out : i32) {
%c2_i32 = hw.constant 2 : i32 // 这里是乘2
%0 = comb.mul %in, %c2_i32 : i32
hw.output %0 : i32
}
hw.module @add(in %in : i32, out out : i32) {
%0 = comb.add %in, %in : i32
hw.output %0 : i32
}
}
执行 --construct-lec Pass 后：将 CIRCT 中的核心方言转换为 LEC 问题
// RUN: %circt-opt --construct-lec="first-module=mulByTwo second-module=add insert-main=true" %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @mulByTwo() {
%0 = verif.lec first { // first 是mulByTwo module, second 是add module
^bb0(%arg0: i32):
%c2_i32 = hw.constant 2 : i32
%4 = comb.mul %arg0, %c2_i32 : i32
verif.yield %4 : i32
} second {
^bb0(%arg0: i32):
%4 = comb.add %arg0, %arg0 : i32
verif.yield %4 : i32
}
%1 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%2 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%3 = llvm.select %0, %1, %2 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
func.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
call @mulByTwo() : () -> ()
%0 = llvm.mlir.constant(0 : i32) : i32
return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
}
执行 --convert-hw-to-smt Pass 后：将 hw 方言转换为 smt 方言
// RUN: circt-opt --convert-hw-to-smt %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @mulByTwo() {
%0 = verif.lec first {
^bb0(%arg0: i32):
%c2_bv32 = smt.bv.constant #smt.bv<2> : !smt.bv<32> // hw方言被转换为了 smt方言
%4 = builtin.unrealized_conversion_cast %c2_bv32 : !smt.bv<32> to i32
%5 = comb.mul %arg0, %4 : i32
verif.yield %5 : i32
} second {
^bb0(%arg0: i32):
%4 = comb.add %arg0, %arg0 : i32
verif.yield %4 : i32
}
%1 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%2 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%3 = llvm.select %0, %1, %2 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
func.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
call @mulByTwo() : () -> ()
%0 = llvm.mlir.constant(0 : i32) : i32
return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
}
执行 --convert-comb-to-smt Pass 后：将 comb 方言转换为 smt 方言
// RUN: circt-opt --convert-comb-to-smt %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @mulByTwo() {
%0 = verif.lec first {
^bb0(%arg0: i32):
%4 = builtin.unrealized_conversion_cast %arg0 : i32 to !smt.bv<32>
%c2_bv32 = smt.bv.constant #smt.bv<2> : !smt.bv<32>
%5 = smt.bv.mul %4, %c2_bv32 : !smt.bv<32> // comb方言转换为了 smt方言
%6 = builtin.unrealized_conversion_cast %5 : !smt.bv<32> to i32
verif.yield %6 : i32
} second {
^bb0(%arg0: i32):
%4 = builtin.unrealized_conversion_cast %arg0 : i32 to !smt.bv<32>
%5 = smt.bv.add %4, %4 : !smt.bv<32>
%6 = builtin.unrealized_conversion_cast %5 : !smt.bv<32> to i32
verif.yield %6 : i32
}
%1 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%2 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%3 = llvm.select %0, %1, %2 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
func.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
call @mulByTwo() : () -> ()
%0 = llvm.mlir.constant(0 : i32) : i32
return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
}
执行 --convert-verify-to-smt Pass 后：将 verif 方言转换为 smt 方言
// RUN: circt-opt --convert-verify-to-smt %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @mulByTwo() {
%0 = smt.solver() : () -> i1 { // verif方言转换为 smt方言
%4 = smt.declare_fun : !smt.bv<32>
%5 = builtin.unrealized_conversion_cast %4 : !smt.bv<32> to i32
%6 = builtin.unrealized_conversion_cast %5 : i32 to !smt.bv<32>
%c2_bv32 = smt.bv.constant #smt.bv<2> : !smt.bv<32>
%7 = smt.bv.mul %6, %c2_bv32 : !smt.bv<32>
%8 = builtin.unrealized_conversion_cast %7 : !smt.bv<32> to i32
%9 = builtin.unrealized_conversion_cast %4 : !smt.bv<32> to i32
%10 = builtin.unrealized_conversion_cast %9 : i32 to !smt.bv<32>
%11 = smt.bv.add %10, %10 : !smt.bv<32>
%12 = builtin.unrealized_conversion_cast %11 : !smt.bv<32> to i32
%13 = builtin.unrealized_conversion_cast %8 : i32 to !smt.bv<32>
%14 = builtin.unrealized_conversion_cast %12 : i32 to !smt.bv<32>
%15 = smt.distinct %13, %14 : !smt.bv<32>
smt.assert %15
%false = arith.constant false // smt方言与 MLIR上游的 arith方言混合使用
%true = arith.constant true
%16 = smt.check sat {
smt.yield %false : i1
} unknown {
smt.yield %false : i1
} unsat {
smt.yield %true : i1
} -> i1
smt.yield %16 : i1
}
%1 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%2 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%3 = llvm.select %0, %1, %2 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
func.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
call @mulByTwo() : () -> ()
%0 = llvm.mlir.constant(0 : i32) : i32
return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
}
执行 --canonicalize Pass 后：对每个定义了 fold 函数或 canonicalize 函数的 Operation 进行相应的优化操作
// RUN: circt-op --canonicalize %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @mulByTwo() {
%0 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%1 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%2 = smt.solver() : () -> i1 {
%true = arith.constant true
%false = arith.constant false
%c2_bv32 = smt.bv.constant #smt.bv<2> : !smt.bv<32>
%4 = smt.declare_fun : !smt.bv<32>
%5 = smt.bv.mul %4, %c2_bv32 : !smt.bv<32>
%6 = smt.bv.add %4, %4 : !smt.bv<32>
%7 = smt.distinct %5, %6 : !smt.bv<32>
smt.assert %7
%8 = smt.check sat {
smt.yield %false : i1
} unknown {
smt.yield %false : i1
} unsat {
smt.yield %true : i1
} -> i1
smt.yield %8 : i1
}
%3 = llvm.select %2, %1, %0 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
func.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
%0 = llvm.mlir.constant(0 : i32) : i32
call @mulByTwo() : () -> ()
return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
}
执行 --lower-smt-to-z3-llvm Pass 后：将 smt 方言转换为 llvm IR 并调用 Z3 API
// RUN: circt-opt --lower-smt-to-z3-llvm %s
module {
llvm.func @Z3_solver_check(!llvm.ptr, !llvm.ptr) -> i32
llvm.func @Z3_solver_assert(!llvm.ptr, !llvm.ptr, !llvm.ptr)
llvm.func @Z3_mk_distinct(!llvm.ptr, i32, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_bvadd(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_bvmul(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_fresh_const(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_unsigned_int64(!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_bv_sort(!llvm.ptr, i32) -> !llvm.ptr
llvm.func @Z3_del_context(!llvm.ptr)
llvm.func @Z3_solver_dec_ref(!llvm.ptr, !llvm.ptr)
llvm.func @Z3_solver_inc_ref(!llvm.ptr, !llvm.ptr)
llvm.func @Z3_mk_solver(!llvm.ptr) -> !llvm.ptr
llvm.func @Z3_del_config(!llvm.ptr)
llvm.func @Z3_mk_context(!llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_config() -> !llvm.ptr
llvm.mlir.global internal @ctx() {addr_space = 0 : i32, alignment = 8 : i64} : !llvm.ptr {
%0 = llvm.mlir.zero : !llvm.ptr
llvm.return %0 : !llvm.ptr
}
llvm.mlir.global internal @solver() {addr_space = 0 : i32, alignment = 8 : i64} : !llvm.ptr {
%0 = llvm.mlir.zero : !llvm.ptr
llvm.return %0 : !llvm.ptr
}
llvm.func @printf(!llvm.ptr, ...)
llvm.func @mulByTwo() {
%0 = llvm.mlir.addressof @solver : !llvm.ptr
%1 = llvm.mlir.addressof @ctx : !llvm.ptr
%2 = llvm.mlir.addressof @"c1 != c2\0A" : !llvm.ptr
%3 = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
%4 = llvm.call @Z3_mk_config() : () -> !llvm.ptr
%5 = llvm.call @Z3_mk_context(%4) : (!llvm.ptr) -> !llvm.ptr
llvm.store %5, %1 : !llvm.ptr, !llvm.ptr
llvm.call @Z3_del_config(%4) : (!llvm.ptr) -> ()
%6 = llvm.call @Z3_mk_solver(%5) : (!llvm.ptr) -> !llvm.ptr
llvm.call @Z3_solver_inc_ref(%5, %6) : (!llvm.ptr, !llvm.ptr) -> ()
llvm.store %6, %0 : !llvm.ptr, !llvm.ptr
%7 = llvm.call @solver_0() : () -> i1
llvm.call @Z3_solver_dec_ref(%5, %6) : (!llvm.ptr, !llvm.ptr) -> ()
llvm.call @Z3_del_context(%5) : (!llvm.ptr) -> ()
%8 = llvm.select %7, %3, %2 : i1, !llvm.ptr
llvm.call @printf(%8) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
llvm.return
}
llvm.func @main(%arg0: i32, %arg1: !llvm.ptr) -> i32 {
%0 = llvm.mlir.constant(0 : i32) : i32
llvm.call @mulByTwo() : () -> ()
llvm.return %0 : i32
}
llvm.mlir.global private constant @"c1 == c2\0A"("c1 == c2\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @"c1 != c2\0A"("c1 != c2\0A\00") {addr_space = 0 : i32}
llvm.func @solver_0() -> i1 {
%0 = llvm.mlir.constant(-1 : i32) : i32
%1 = llvm.mlir.undef : !llvm.array<2 x ptr>
%2 = llvm.mlir.constant(1 : i32) : i32
%3 = llvm.mlir.constant(2 : i32) : i32
%4 = llvm.mlir.zero : !llvm.ptr
%5 = llvm.mlir.constant(2 : i64) : i64
%6 = llvm.mlir.constant(32 : i32) : i32
%7 = llvm.mlir.constant(false) : i1
%8 = llvm.mlir.constant(true) : i1
%9 = llvm.mlir.addressof @ctx : !llvm.ptr
%10 = llvm.mlir.addressof @solver : !llvm.ptr
%11 = llvm.load %10 : !llvm.ptr -> !llvm.ptr
%12 = llvm.load %9 : !llvm.ptr -> !llvm.ptr
%13 = llvm.call @Z3_mk_bv_sort(%12, %6) : (!llvm.ptr, i32) -> !llvm.ptr
%14 = llvm.call @Z3_mk_unsigned_int64(%12, %5, %13) : (!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
%15 = llvm.call @Z3_mk_bv_sort(%12, %6) : (!llvm.ptr, i32) -> !llvm.ptr
%16 = llvm.call @Z3_mk_fresh_const(%12, %4, %15) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%17 = llvm.call @Z3_mk_bvmul(%12, %16, %14) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%18 = llvm.call @Z3_mk_bvadd(%12, %16, %16) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%19 = llvm.alloca %2 x !llvm.array<2 x ptr> : (i32) -> !llvm.ptr
%20 = llvm.insertvalue %17, %1[0] : !llvm.array<2 x ptr>
%21 = llvm.insertvalue %18, %20[1] : !llvm.array<2 x ptr>
llvm.store %21, %19 : !llvm.array<2 x ptr>, !llvm.ptr
%22 = llvm.call @Z3_mk_distinct(%12, %3, %19) : (!llvm.ptr, i32, !llvm.ptr) -> !llvm.ptr
llvm.call @Z3_solver_assert(%12, %11, %22) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> ()
%23 = llvm.call @Z3_solver_check(%12, %11) : (!llvm.ptr, !llvm.ptr) -> i32
%24 = llvm.icmp "eq" %23, %2 : i32
llvm.cond_br %24, ^bb1, ^bb2
^bb1: // pred: ^bb0
llvm.br ^bb7(%7 : i1)
^bb2: // pred: ^bb0
%25 = llvm.icmp "eq" %23, %0 : i32
llvm.cond_br %25, ^bb3, ^bb4
^bb3: // pred: ^bb2
llvm.br ^bb5(%8 : i1)
^bb4: // pred: ^bb2
llvm.br ^bb5(%7 : i1)
^bb5(%26: i1): // 2 preds: ^bb3, ^bb4
llvm.br ^bb6
^bb6: // pred: ^bb5
llvm.br ^bb7(%26 : i1)
^bb7(%27: i1): // 2 preds: ^bb1, ^bb6
llvm.br ^bb8
^bb8: // pred: ^bb7
llvm.return %27 : i1
}
}
执行 JIT 测试：使用 mlir-cpu-runner 工具运行 JIT，并且添加 Z3 依赖 --shared-libs=%libz3.so 作为其参数
// RUN: mlir-cpu-runner -e mulByTwo --entry-point-result=void --shared-libs=%libz3.so %s
Result: c1 == c2
也可以直接使用 circt-lec 工具进行 JIT 测试，如下：
.mlir:
module {
hw.module @mulByOne(in %in : i32, out out : i32) {
%c2_i32 = hw.constant 1 : i32 // 这里是乘1
%0 = comb.mul %in, %c2_i32 : i32
hw.output %0 : i32
}
hw.module @add(in %in : i32, out out : i32) {
%0 = comb.add %in, %in : i32
hw.output %0 : i32
}
}
输出结果：
// RUN: circt-lec %s --c1=mulByOne --c2=add --shared-libs=/usr/lib/x86_64-linux-gnu/libz3.so
Result: c1 != c2
CIRCR 中的 BMC 工具：circt-bmc
.mlir：
module {
hw.module @same(in %i0: i1, in %i1: i1) attributes {num_regs = 0 : i32, initial_values = []} {
%or0 = comb.or %i0, %i1 : i1
%or1 = comb.or %i1, %i0 : i1
%cond = comb.icmp eq %or0, %or1 : i1 // 判断相等
verif.assert %cond : i1
}
}
执行 --lower-to-bmc Pass 后：将 CIRCT 中的核心方言转换为 BMC 问题
// RUN: circt-opt --lower-to-bmc="top-module=same bound=5" %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @same() {
%0 = verif.bmc bound 10 num_regs 0 initial_values [] init {
} loop {
} circuit {
^bb0(%arg0: i1, %arg1: i1):
%4 = comb.or %arg0, %arg1 : i1
%5 = comb.or %arg1, %arg0 : i1
%6 = comb.icmp eq %4, %5 : i1
verif.assert %6 : i1
}
%1 = llvm.mlir.addressof @resultString_0 : !llvm.ptr
%2 = llvm.mlir.addressof @resultString_1 : !llvm.ptr
%3 = llvm.select %0, %1, %2 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
llvm.mlir.global private constant @resultString_0("Bound reached with no violations!\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @resultString_1("Assertion can be violated!\0A\00") {addr_space = 0 : i32}
}
将 Core 方言与 Verif 方言转换为 SMT 方言后：
// RUN: circt-opt --convert-hw-to-smt --convert-comb-to-smt --convert-verif-to-smt --canonicalize %s
module {
llvm.func @printf(!llvm.ptr, ...)
func.func @same() {
%0 = llvm.mlir.addressof @resultString_1 : !llvm.ptr
%1 = llvm.mlir.addressof @resultString_0 : !llvm.ptr
%2 = smt.solver() : () -> i1 {
%true = arith.constant true
%false = arith.constant false
%c10_i32 = arith.constant 10 : i32
%c1_i32 = arith.constant 1 : i32
%c0_i32 = arith.constant 0 : i32
func.call @bmc_init() : () -> ()
smt.push 1
%4 = smt.declare_fun : !smt.bv<1>
%5 = smt.declare_fun : !smt.bv<1>
%6:3 = scf.for %arg0 = %c0_i32 to %c10_i32 step %c1_i32 iter_args(%arg1 = %4, %arg2 = %5, %arg3 = %false) -> (!smt.bv<1>, !smt.bv<1>, i1) : i32 {
smt.pop 1
smt.push 1
func.call @bmc_circuit(%arg1, %arg2) : (!smt.bv<1>, !smt.bv<1>) -> ()
%8 = smt.check sat {
smt.yield %true : i1
} unknown {
smt.yield %true : i1
} unsat {
smt.yield %false : i1
} -> i1
%9 = arith.ori %8, %arg3 : i1
func.call @bmc_loop() : () -> ()
%10 = smt.declare_fun : !smt.bv<1>
%11 = smt.declare_fun : !smt.bv<1>
scf.yield %10, %11, %9 : !smt.bv<1>, !smt.bv<1>, i1
}
%7 = arith.xori %6#2, %true : i1
smt.yield %7 : i1
}
%3 = llvm.select %2, %1, %0 : i1, !llvm.ptr
llvm.call @printf(%3) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
return
}
llvm.mlir.global private constant @resultString_0("Bound reached with no violations!\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @resultString_1("Assertion can be violated!\0A\00") {addr_space = 0 : i32}
func.func @bmc_init() {
return
}
func.func @bmc_loop() {
return
}
func.func @bmc_circuit(%arg0: !smt.bv<1>, %arg1: !smt.bv<1>) {
%c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
%c0_bv1 = smt.bv.constant #smt.bv<0> : !smt.bv<1>
%0 = smt.bv.or %arg0, %arg1 : !smt.bv<1>
%1 = smt.bv.or %arg1, %arg0 : !smt.bv<1>
%2 = smt.eq %0, %1 : !smt.bv<1>
%3 = smt.ite %2, %c-1_bv1, %c0_bv1 : !smt.bv<1>
%4 = smt.eq %3, %c-1_bv1 : !smt.bv<1>
%5 = smt.not %4
smt.assert %5
return
}
}
执行 --lower-smt-to-z3-llvm Pass 后：将 smt 方言转换为 llvm IR 并调用 Z3 API
// RUN: circt-opt --lower-smt-to-z3-llvm %s
module {
llvm.func @Z3_solver_assert(!llvm.ptr, !llvm.ptr, !llvm.ptr)
llvm.func @Z3_mk_not(!llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_ite(!llvm.ptr, !llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_unsigned_int64(!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_eq(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_bvor(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_solver_check(!llvm.ptr, !llvm.ptr) -> i32
llvm.func @Z3_solver_pop(!llvm.ptr, !llvm.ptr, i32)
llvm.func @Z3_mk_fresh_const(!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_bv_sort(!llvm.ptr, i32) -> !llvm.ptr
llvm.func @Z3_solver_push(!llvm.ptr, !llvm.ptr)
llvm.func @Z3_del_context(!llvm.ptr)
llvm.func @Z3_solver_dec_ref(!llvm.ptr, !llvm.ptr)
llvm.func @Z3_solver_inc_ref(!llvm.ptr, !llvm.ptr)
llvm.func @Z3_mk_solver(!llvm.ptr) -> !llvm.ptr
llvm.func @Z3_del_config(!llvm.ptr)
llvm.func @Z3_mk_context(!llvm.ptr) -> !llvm.ptr
llvm.func @Z3_mk_config() -> !llvm.ptr
llvm.mlir.global internal @ctx() {addr_space = 0 : i32, alignment = 8 : i64} : !llvm.ptr {
%0 = llvm.mlir.zero : !llvm.ptr
llvm.return %0 : !llvm.ptr
}
llvm.mlir.global internal @solver() {addr_space = 0 : i32, alignment = 8 : i64} : !llvm.ptr {
%0 = llvm.mlir.zero : !llvm.ptr
llvm.return %0 : !llvm.ptr
}
llvm.func @printf(!llvm.ptr, ...)
llvm.func @same() {
%0 = llvm.mlir.addressof @resultString_1 : !llvm.ptr
%1 = llvm.mlir.addressof @resultString_0 : !llvm.ptr
%2 = llvm.mlir.addressof @solver : !llvm.ptr
%3 = llvm.mlir.addressof @ctx : !llvm.ptr
%4 = llvm.call @Z3_mk_config() : () -> !llvm.ptr
%5 = llvm.call @Z3_mk_context(%4) : (!llvm.ptr) -> !llvm.ptr
llvm.store %5, %3 : !llvm.ptr, !llvm.ptr
llvm.call @Z3_del_config(%4) : (!llvm.ptr) -> ()
%6 = llvm.call @Z3_mk_solver(%5) : (!llvm.ptr) -> !llvm.ptr
llvm.call @Z3_solver_inc_ref(%5, %6) : (!llvm.ptr, !llvm.ptr) -> ()
llvm.store %6, %2 : !llvm.ptr, !llvm.ptr
%7 = llvm.call @solver_0() : () -> i1
llvm.call @Z3_solver_dec_ref(%5, %6) : (!llvm.ptr, !llvm.ptr) -> ()
llvm.call @Z3_del_context(%5) : (!llvm.ptr) -> ()
%8 = llvm.select %7, %1, %0 : i1, !llvm.ptr
llvm.call @printf(%8) vararg(!llvm.func<void (ptr, ...)>) : (!llvm.ptr) -> ()
llvm.return
}
llvm.mlir.global private constant @resultString_0("Bound reached with no violations!\0A\00") {addr_space = 0 : i32}
llvm.mlir.global private constant @resultString_1("Assertion can be violated!\0A\00") {addr_space = 0 : i32}
llvm.func @bmc_init() {
llvm.return
}
llvm.func @bmc_loop() {
llvm.return
}
llvm.func @bmc_circuit(%arg0: !llvm.ptr, %arg1: !llvm.ptr) {
%0 = llvm.mlir.constant(1 : i64) : i64
%1 = llvm.mlir.constant(0 : i64) : i64
%2 = llvm.mlir.constant(1 : i32) : i32
%3 = llvm.mlir.addressof @ctx : !llvm.ptr
%4 = llvm.mlir.addressof @solver : !llvm.ptr
%5 = llvm.load %4 : !llvm.ptr -> !llvm.ptr
%6 = llvm.load %3 : !llvm.ptr -> !llvm.ptr
%7 = llvm.call @Z3_mk_bvor(%6, %arg0, %arg1) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%8 = llvm.call @Z3_mk_bvor(%6, %arg1, %arg0) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%9 = llvm.call @Z3_mk_eq(%6, %7, %8) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%10 = llvm.call @Z3_mk_bv_sort(%6, %2) : (!llvm.ptr, i32) -> !llvm.ptr
%11 = llvm.call @Z3_mk_unsigned_int64(%6, %1, %10) : (!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
%12 = llvm.call @Z3_mk_bv_sort(%6, %2) : (!llvm.ptr, i32) -> !llvm.ptr
%13 = llvm.call @Z3_mk_unsigned_int64(%6, %0, %12) : (!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
%14 = llvm.call @Z3_mk_ite(%6, %9, %13, %11) : (!llvm.ptr, !llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%15 = llvm.call @Z3_mk_bv_sort(%6, %2) : (!llvm.ptr, i32) -> !llvm.ptr
%16 = llvm.call @Z3_mk_unsigned_int64(%6, %0, %15) : (!llvm.ptr, i64, !llvm.ptr) -> !llvm.ptr
%17 = llvm.call @Z3_mk_eq(%6, %14, %16) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%18 = llvm.call @Z3_mk_not(%6, %17) : (!llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.call @Z3_solver_assert(%6, %5, %18) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> ()
llvm.return
}
llvm.func @solver_0() -> i1 {
%0 = llvm.mlir.constant(-1 : i32) : i32
%1 = llvm.mlir.constant(true) : i1
%2 = llvm.mlir.constant(false) : i1
%3 = llvm.mlir.constant(10 : i32) : i32
%4 = llvm.mlir.constant(0 : i32) : i32
%5 = llvm.mlir.constant(1 : i32) : i32
%6 = llvm.mlir.zero : !llvm.ptr
%7 = llvm.mlir.addressof @solver : !llvm.ptr
%8 = llvm.mlir.addressof @ctx : !llvm.ptr
%9 = llvm.load %8 : !llvm.ptr -> !llvm.ptr
%10 = llvm.load %7 : !llvm.ptr -> !llvm.ptr
llvm.call @bmc_init() : () -> ()
llvm.call @Z3_solver_push(%9, %10) : (!llvm.ptr, !llvm.ptr) -> ()
%11 = llvm.call @Z3_mk_bv_sort(%9, %5) : (!llvm.ptr, i32) -> !llvm.ptr
%12 = llvm.call @Z3_mk_fresh_const(%9, %6, %11) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%13 = llvm.call @Z3_mk_bv_sort(%9, %5) : (!llvm.ptr, i32) -> !llvm.ptr
%14 = llvm.call @Z3_mk_fresh_const(%9, %6, %13) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
llvm.br ^bb1(%4, %12, %14, %2 : i32, !llvm.ptr, !llvm.ptr, i1)
^bb1(%15: i32, %16: !llvm.ptr, %17: !llvm.ptr, %18: i1): // 2 preds: ^bb0, ^bb10
%19 = llvm.icmp "slt" %15, %3 : i32
llvm.cond_br %19, ^bb2, ^bb11
^bb2: // pred: ^bb1
%20 = llvm.load %8 : !llvm.ptr -> !llvm.ptr
%21 = llvm.load %7 : !llvm.ptr -> !llvm.ptr
llvm.call @Z3_solver_pop(%20, %21, %5) : (!llvm.ptr, !llvm.ptr, i32) -> ()
llvm.call @Z3_solver_push(%20, %21) : (!llvm.ptr, !llvm.ptr) -> ()
llvm.call @bmc_circuit(%16, %17) : (!llvm.ptr, !llvm.ptr) -> ()
%22 = llvm.call @Z3_solver_check(%20, %21) : (!llvm.ptr, !llvm.ptr) -> i32
%23 = llvm.icmp "eq" %22, %5 : i32
llvm.cond_br %23, ^bb3, ^bb4
^bb3: // pred: ^bb2
llvm.br ^bb9(%1 : i1)
^bb4: // pred: ^bb2
%24 = llvm.icmp "eq" %22, %0 : i32
llvm.cond_br %24, ^bb5, ^bb6
^bb5: // pred: ^bb4
llvm.br ^bb7(%2 : i1)
^bb6: // pred: ^bb4
llvm.br ^bb7(%1 : i1)
^bb7(%25: i1): // 2 preds: ^bb5, ^bb6
llvm.br ^bb8
^bb8: // pred: ^bb7
llvm.br ^bb9(%25 : i1)
^bb9(%26: i1): // 2 preds: ^bb3, ^bb8
llvm.br ^bb10
^bb10: // pred: ^bb9
%27 = llvm.load %8 : !llvm.ptr -> !llvm.ptr
%28 = llvm.or %26, %18 : i1
llvm.call @bmc_loop() : () -> ()
%29 = llvm.call @Z3_mk_bv_sort(%27, %5) : (!llvm.ptr, i32) -> !llvm.ptr
%30 = llvm.call @Z3_mk_fresh_const(%27, %6, %29) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%31 = llvm.call @Z3_mk_bv_sort(%27, %5) : (!llvm.ptr, i32) -> !llvm.ptr
%32 = llvm.call @Z3_mk_fresh_const(%27, %6, %31) : (!llvm.ptr, !llvm.ptr, !llvm.ptr) -> !llvm.ptr
%33 = llvm.add %15, %5 : i32
llvm.br ^bb1(%33, %30, %32, %28 : i32, !llvm.ptr, !llvm.ptr, i1)
^bb11: // pred: ^bb1
%34 = llvm.xor %18, %1 : i1
llvm.return %34 : i1
}
}
执行 JIT 测试：使用 mlir-cpu-runner 工具运行 JIT，并且添加 Z3 依赖 --shared-libs=%libz3.so 作为其参数
// RUN: mlir-cpu-runner -e same --entry-point-result=void --shared-libs=%libz3.so %s
Bound reached with no violations!
也可以直接使用 circt-bmc 工具进行 JIT 测试，如下：
.mlir：
module {
hw.module @diff(in %i0: i1, in %i1: i1) attributes {num_regs = 0 : i32, initial_values = []} {
%or0 = comb.or %i0, %i1 : i1
%or1 = comb.or %i1, %i0 : i1
%cond = comb.icmp ne %or0, %or1 : i1 // 这里是判断不相等
verif.assert %cond : i1
}
}
输出结果：
// RUN: circt-bmc %s -b 100 --module=diff --shared-libs=/usr/lib/x86_64-linux-gnu/libz3.so
Assertion can be violated!
综上所述，在实际硬件领域，BMC 和 LEC 工具各自具有不同的应用场景和优势，前者专注于比较两个设计（如 RTL 和门级网表）是否在功能上等价。LEC 确保在相同输入下，两个设计产生相同的输出，适用于验证设计修改后是否保持原有功能。而后者主要用于验证系统在有限步数内是否满足特定性质。它通过设定一个边界 k，检查系统在 k 步内的行为是否符合预期，这也使得 BMC 特别适合于检测反例。
总结
形式化验证在现代硬件设计中扮演着不可或缺的角色，尤其是在复杂系统中，通过使用 circt-bmc 和 circt-lec 等工具，设计者能够在早期阶段发现潜在的设计缺陷，从而降低后期修改的成本。在硬件设计流程中，这两种工具可以互补使用，以提高验证的全面性和有效性。随着技术的不断发展，形式化验证将继续推动硬件设计的可靠性和安全性，为未来的电子产品奠定坚实基础。
参考资料: