基于FPGA的SAT自动一体化求解器

摘要

本发明提供了一种基于FPGA的SAT自动一体化求解器，有效判断CNF是否可满足。首先用C++翻译器将CNF自动翻译成verilog语言，即将合取范式转换成门级电路形式，通过Questasim软件对门级电路进行仿真，检验仿真是否与理论逻辑相同，然后通过Precision软件对电路进行优化与综合，最后调用集成在Precision软件中的QuartusII软件进行引脚配置最后将综合文件下载到FPGA电路板上固化为硬件逻辑，进行验证，并将固化的FPGA芯片嵌入到嵌入式芯片，利用Tcl脚本语言与高级语言c++联合编程实现生成文件调用命令全过程自动化，快速判断CNF是否可满足，将硬件编译配置的时间计入，相比其他硬件SAT求解器更加精确地计算整个流程的时间。

权利要求

1.基于FPGA的SAT自动一体化求解器的建立方法，其特征是该方法包含以下步骤：

1)首先用C++语言编写好的翻译器可以将CNF格式文件内容自动翻译成verilog语言，即将合取范式转换成门级电路形式；

2)通过Precision软件对已优化的电路进行综合，最后将综合文件下载到FPGA开发板上，进行验证；

3)利用硬件脚本语言Tcl编写命令调用Questasim软件对门级电路进行优化，通过Precision对已优化的电路进行综合，以及将综合文件下载到FPGA开发板上进行验证；

4)将FPGA芯片嵌入到ARM系统中，实现生成相关设计文件并调用控制命令全面的自动化。

2.根据权利要求1所述的基于FPGA的SAT自动一体化求解器的建立方法，其特征在于，基于FPGA的编译、仿真、综合、验证、下载自动一体化；能够将从仿真、编译、综合、下载整个流程的时间精确计算出来；基于FPGA的SAT的算法为应用型。

说明书

基于FPGA的SAT自动一体化求解器

一、技术领域：

[0001] 本发明属于专用FPGA芯片设计领域。二、背景技术：

[0002] SAT(satisfiability problem)即(布尔)可满足性问题是计算机理论与应用的核心问题之一，也是第一 个被证明的NP问题。多种实际问题，如程控电话的自动交换技术，机器人动作规划等等，都可转化为SAT 问题来求解。目前，SAT已经应用在计算机系统结构设计、逻辑推理、模型检测、集成电路设计和人工智 能等领域，特别在集成电路设计验证方面，SAT具有极其广泛而深入的应用。

[0003] 随着近几十年电子业的发展，集成电路系统日趋复杂化和大规模集成化，设计复杂程度越来越高，设 计周期越来越短，保证IC设计的正确与否成为设计过程中的关键，SAT问题已经成为电路搜索和验证问 题的基石。为了提高集成电路的设计效率，确保IC功能，缩短开发周期，开发性能卓越SAT求解器，并 将其集成到已有EDA系统，是一种切实有效的办法。

[0004] SAT问题用于判断布尔逻辑公式是否存在一组满足解，即一组可以使布尔公式值为真的布尔变量的赋  值。一般而言，SAT问题的布尔公式的标准形式是合取范式(conjunctive normal form，简称CNF)，判断 CNF公式是否为真的工具被称为SAT求解器。传统的SAT求解器都是软件实现的，其求解算法分为完全 算法和不完全算法，完全算法穷尽搜索SAT公式的解空间，理论上一定可以得出某个SAT公式的满足性 结论，但是SAT问题属于NP问题，其解空间随着公式的变量个数呈指数增长，所以此种算法效率较低， 不适用于求解大规模的SAT问题。不完全算法并不搜索整个解空间，而是采用种种办法搜索部分解空间， 其求解速度较快，但是并不能保证一定能判断SAT问题的可满足性。随着实际SAT问题规模的急剧增大， 软件求解器已经不能快速有效地判定SAT问题的可满足性。硬件SAT求解器可以从根本上解决传统软件 求解器的效率瓶颈，将SAT的求解过程加速到极致。

[0005] 目前国内外已经开发出几种SAT硬件求解器，这些求解器均选用了计算能力强的现场可编程门阵列 (FPGA)，作为硬件实现平台。可以将这些硬件求解器分为两种类型：实例型算法芯片和应用型算法芯片。

[0006] 对于实例型方法，其硬件结构针对每一个实例独立开发、配置和验证芯片，而后对芯片加电进行SAT 实例的计算。这种方法中，每一个的实例对应不同的硬件结构，每一个芯片只能进行某种实例的求解运算， 这种方法的通用性较差，成本较高，但是这种方法充分发挥了数字电路系统的内在特征，完全避免了上述 软件和应用型方法面临的挑战，将非常适用于大规模的SAT实例。

[0007] 而应用型方法，其目的在于开发一种通用的SAT硬件芯片，这种方法本质上是对软件SAT算法的硬 件实现，既使用FPGA实现一些瓶颈算法，最终的求解器工作在软硬件协同的机制下。这种方法的优点在 于通用性，即只需要进行一次编译和配置的过程，然后可以对所有实例进行计算。其缺点在于，这种解决 机制本质上并没有将电路系统的特征引入SAT的求解中来，而仅仅使用了FPGA的可编程特征，所以这种 方案依然会遇到与软件求解器相同的挑战。

[0008] 但传统应用型芯片大多数只实现了软件的SAT算法，例如DP算法，同时自动化程度也较低，但我们 的芯片采用将CNF公式转换为电路形式解决SAT问题，将FPGA的内在结构同SAT问题的求解自然地合 为一体，除此之外，我们基于芯片的SAT求解框架自动化程度更高，实现了SAT问题翻译、FPGA编译和 配置等各个环节的自动化。三、发明内容：

[0009] a)发明目的

[0010] 随着SAT应用规模的深入，表达目标系统的CNF式中变量的数目激增，已经达到百万量级，基于软 件求解器面临巨大挑战。另一方面，随着FPGA技术的突破性发展，已达到四千五百万逻辑门的水平，其 逻辑能力已上升到处理当前SAT应用规模的程度。那么研发FPGA专用芯片，快速有效求解SAT问题， 就成了一种快速可行的方案。

[0011] 我们设计的SAT专用芯片系统，采用自动一体化的求解框架，将SAT问题中的CNF编译，FPGA芯 片仿真、综合和验证，及FPGA配置、下载和计算，统一起来，为用户提供了一键式的快捷使用方法，可 以方便快速地判断7K变量，190k个子句CNF式是否可满足。

[0012] b)技术方案

[0013] 为了兼顾验证效率和规模，本发明应用FPGA技术对SAT问题进行判定，编译、仿真、综合、验证、 下载，将判定CNF式是否可满足的流程封装到一起，发明出了SAT的一体化求解器，结构如图1所示。 此求解器首先读取CNF文件，将其自动翻译成Verilog语言，随后对Verilog程序所对应的电路进行优化并 通过专用软件仿真、综合与下载，最后加电判断其满足性。除了一键式的自动化验证功能之外，作为一体 化求解器，本发明还可将硬件编译配置的时间计入，将整个流程的时间精确计算出来。

[0014] SAT问题指的是判定命题公式是否存在一组可满足解的问题，依据布尔代数理论，每一个命题公式在 逻辑上等同于一个特定的合取范式(coniunctive normal form，简称CNF)，所以方便起见，SAT问题一般 采用CNF式表示。CNF形式上表示为若干个布尔变量(或逆变量)构成析取式的逻辑合取，称布尔变量 为文字，布尔变量的非为逆文字，文字与逆文字构成的析取式为子句，所以CNF可以表示为子句的集合。 CNF式的构成规则可以形式化描述如为，布尔变量x及其否定 x构成了文字与逆文字，若干个文字(逆 文字)的逻辑析取(∨)构成子句，若干个子句的合取(∧)最终组成合取范式，SAT问题最终由CNF 式描述。

[0015] 给定一个CNF式，SAT求解器用于求出变量的一组赋值，以此赋值为输入，公式的值为真，即公式 可满足。我们SAT专用芯片系统的技术方案如下：

[0016] 1.专用编译器软件将CNF公式文件编译为数字电路的Verilog输入文件。

[0017] CNF格式文件的语法简单明了，第一行描述变量和子句的个数，从第二行直到文件结束，每一行描述 一个子句，如下面的例子：

[0018]

[0019] 250表示变量数目，1065表示此CNF公式中包含的子句数目，-159-2341970为第一个子句，-71 13 194 0 为第二个子句，-159表示第159个变量对应的逆文字，0表示结束子句。

[0020] 子句内各文字间是逻辑析取的意义，即∨联接各文字组成子句；子句间的关系为逻辑合取，用逻辑连 结词∧联接。CNF公式与寄存器传输级(RTL)级数字电路的定义是一致的，而事实上布尔逻辑是RTL 级电路设计的基础理论，将CNF公式表示为逻辑电路是一种自然和有效的方法。如CNF公式

[0021]

[0022] 可以非常有效地表示成图2所示的组合电路。

[0023] 判定CNF式的值可以表示为图3，CNF文件中每个变量可以分别取0或1，四个变量取值的组合为 0000-1111共计16种，称这16种取值为状态，那么判定CNF公式是否可满足的SAT问题，就等效于在 变量的状态空间中找出一个状态，状态的赋值可以满足此CNF公式。图2所示组合电路的一组赋值：x0＝1， x1＝1，x2＝0，x3＝1，作为上述CNF公式的输入时，可以求得公式的值y为1，即上面的CNF公式是可满足 的。

[0024] 2.C++编译器软件编写的脚本文件自动生成本发明所需相应变量的sat.v、sat_tb.v、fsm.v、cnf.v文件， 实现程序文件自动生成，本发明的硬件模块图如图4所示，本发明设计文件由三个设计文件组成，即sat.v、 fsm.v、cnf.v，每个文件分别对应相应的模块，其中fsm模块可以用穷举法遍历CNF式中所有变量组合。 例如输入变量个数为四，则fsm模块可遍历0000-1111。fsm模块的变量组合赋值到cnf模块根据理论逻 辑判断出是否可满足。

[0025] 3.sat模块作为顶层模块调用cnf模块和fsm模块，在初期阶段把1、2两步骤中的cnf.v、sat.v、sat_tb.v、 fsm.v文件输入到Questasim软件，对门级电路进行仿真、优化，调试后若观察仿真波形无误，则可证明程 序设计是正确的。此步骤在后期阶段中不需再执行，因为此步骤成功后可证明我们编写的程序是没有错误 的，无需每次进行验证。

[0026] 4.将1、2两步骤的cnf.v、sat.v、fsm.v文件输入到Precision软件中对已优化的电路进行综合，再调 用Quartus II软件将综合文件下载到FPGA电路板上进行验证，将输出y连接到蜂鸣器或LED灯的引脚上。 根据输出结果进行判定，如图4根据fsm模块中的变量赋值到cnf模块，q端会根据理论逻辑输出低电平 或高电平，如果q端一直输出低电平，则y输出低电平，q端输出一旦出现高电平，则y端一直输出为高 电平，继而蜂鸣器响或LED灯亮，则证明可满足，否则证明不可满足。

[0027] 5.为实现本发明自动化，编写脚本程序，Tcl(tool command language)是一种用于控制和扩展应用程 序的动态脚本语言，可以很容易整合到应用到程序中，是工业界普遍使用的测试规范语言。使用Tcl语言 编写的测试脚本即使进行了修改也不需要重新编译即可调用Tcl解释器执行，从而节省时间，提高测试效 率。由于Tcl易学功能强大，经常被用于快速原型开发，脚本编程。

[0028] 利用硬件脚本语言Tcl将1、2、4步骤的翻译器自动翻译，通过Precision软件对已优化的电路进行综 合，再将综合文件下载到FPGA电路板上实现全过程自动化，最后将整个系统操作嵌入到ARM中，实现 更全面的自动化。

[0029] 本发明采用实例型的方法研究SAT求解系统，主要针对这种方法通用性差的特征，研究和开发一体化 的实例型自动求解机制和框架。主要思路为针对大规模实际系统的CNF公式实例，自动地定制化编译和 转换为FPGA芯片，由FPGA硬件完成系统的SAT满足性求解过程。

[0030] 与本发明相关的现有技术或平台有：

[0031] 数字电路基础、模型检测理论、可满足性理论、和Questasim、Precision、QuartusII等工具平台构成了 本发明的理论基础。

[0032] FPGA即现场可编程逻辑器件，它是在CPLD等可编程器件的基础上进一步发展的产物。它是作为专 用集成电路(ASIC)领域中的一种半定制电路而出现的，解决了定制电路的不足，又克服了原有可编程器 件电路有限的缺点，并且内部连接模式和逻辑结构可以根据不同的需要改变，可以实现基于硬件可编程逻 辑的高难度算法。

[0033] Questasim是Mentor公司的综合性FPGA开发软件，支持VHDL、VerilogHDL、SystemC、SystemVerilog 等多种设计输入形式，QuestaSim具备强大的模拟仿真功能，在设计、编译、仿真、测试，调试开发过程 中，操作比较灵活，可以通过菜单和命令的方式进行工作。本发明可以通过此软件进行编译仿真，所选用 的是QuestaSim10.2c。

[0034] Precision是Mentor公司生产的利用综合工具套件对硬件语言(VHDL，Verilog，SystemVerilog)进行综 合的软件，是应用于CPLD和FPGA，SOC设备的综合平台。可在Windows XP，Windows7，LinuxCentos， UNIX平台应用。本发明可以通过此软件进行综合，所选用的是precision2014a.1。

[0035] Quartus II是Altera公司的综合性PLD/FPGA开发软件，支持原理图、VHDL、VerilogHDL以及AHDL (Altera Hardware Description Language)等多种设计输入形式，内嵌自有的综合器以及仿真器，可以完成 从设计输入到硬件配置的完整PLD设计流程，本设计所选用的是Quartus II 9.1。

[0036] c)有益效果

[0037] (1)本发明是基于FPGA的编译、仿真、综合、验证、下载自动一体化，可以把硬件编译配置的时 间计入将整个流程的时间精确计算出来。

[0038] (2)利用C++语言编写好的翻译器将CNF式自动翻译成verilog语言并自动生成相关设计文件。

[0039] (3)可将FPGA芯片嵌入到ARM系统中，利用Tcl硬件脚本语言和高级语言联合编程使全过程实现 自动化，达到方便快捷进行验证的目的。四、附图说明

[0040] 图1：系统架构图

[0041] 图2：电路图

[0042] 图3：验证CNF流程图

[0043] 图4：硬件模块图五、具体实施方式

[0044] 首先用C++语言编写好的翻译器将CNF式自动翻译成verilog语言，即将CNF编译成门级电路形式， 然后通过Questasim软件对门级电路进行仿真，检验仿真是否与理论逻辑相同，然后再通过Precision对电 路进行优化与综合，最后调用集成在Precision中的Quartus II软件进行引脚配置最后将综合文件下载到 FPGA电路板上固化为硬件逻辑，形成CNF的Clause逻辑计算模块，用穷举法进行搜索取值，对实例的 可满足性进行验证，将输出连接到蜂鸣器或LED灯的引脚上，如果输出为高电平，则蜂鸣器响或LED灯 亮，则直观的证明此CNF可满足，否则证明不可满足。通过Precision对电路进行优化与综合，调用集成 在Precision中的Quartus II软件进行引脚配置最后将综合文件下载到FPGA电路板上固化为硬件逻辑，将 固化的FPGA嵌入到ARM系统，利用Tcl硬件脚本语言和高级语言联合编程控制调用命令实现自动化。