[發明專利]基于FPGA的SAT自動一體化求解器

有效

• 申請號: 201410748527.2
• 申請日: 2014-12-10
• 公開（公告）號: CN105740206B
• 公開（公告）日: 2018-11-16
• 發明（設計）人: 何安平;吳盡昭;宋曉宇;毛樂樂;熊菊霞
• 申請（專利權）人: 何安平
• 主分類號: G06F17/15
• 分類號: G06F17/15;G06F8/41
• 代理公司: 暫無信息
• 代理人: 暫無信息

本發明提供了一種基于FPGA的SAT自動一體化求解器，有效判斷CNF是否可滿足。首先用C++翻譯器將CNF自動翻譯成verilog語言，即將合取范式轉換成門級電路形式，通過Questasim軟件對門級電路進行仿真，檢驗仿真是否與理論邏輯相同，然后通過Precision軟件對電路進行優化與綜合，最后調用集成在Precision軟件中的QuartusII軟件進行引腳配置最后將綜合文件下載到FPGA電路板上固化為硬件邏輯，進行驗證，并將固化的FPGA芯片嵌入到嵌入式芯片，利用Tcl腳本語言與高級語言c++聯合編程實現生成文件調用命令全過程自動化，快速判斷CNF是否可滿足，將硬件編譯配置的時間計入，相比其他硬件SAT求解器更加精確地計算整個流程的時間。

一、技術領域：

本發明屬于專用FPGA芯片設計領域。

二、背景技術：

SAT(satisfiability problem)即(布爾)可滿足性問題是計算機理論與應用的核心問題之一，也是第一 個被證明的NP問題。多種實際問題，如程控電話的自動交換技術，機器人動作規劃等等，都可轉化為SAT 問題來求解。目前，SAT已經應用在計算機系統結構設計、邏輯推理、模型檢測、集成電路設計和人工智 能等領域，特別在集成電路設計驗證方面，SAT具有極其廣泛而深入的應用。

隨著近幾十年電子業的發展，集成電路系統日趨復雜化和大規模集成化，設計復雜程度越來越高，設 計周期越來越短，保證IC設計的正確與否成為設計過程中的關鍵，SAT問題已經成為電路搜索和驗證問 題的基石。為了提高集成電路的設計效率，確保IC功能，縮短開發周期，開發性能卓越SAT求解器，并 將其集成到已有EDA系統，是一種切實有效的辦法。

SAT問題用于判斷布爾邏輯公式是否存在一組滿足解，即一組可以使布爾公式值為真的布爾變量的賦 值。一般而言，SAT問題的布爾公式的標準形式是合取范式(conjunctive normal form，簡稱CNF)，判斷 CNF公式是否為真的工具被稱為SAT求解器。傳統的SAT求解器都是軟件實現的，其求解算法分為完全 算法和不完全算法，完全算法窮盡搜索SAT公式的解空間，理論上一定可以得出某個SAT公式的滿足性 結論，但是SAT問題屬于NP問題，其解空間隨著公式的變量個數呈指數增長，所以此種算法效率較低， 不適用于求解大規模的SAT問題。不完全算法并不搜索整個解空間，而是采用種種辦法搜索部分解空間， 其求解速度較快，但是并不能保證一定能判斷SAT問題的可滿足性。隨著實際SAT問題規模的急劇增大， 軟件求解器已經不能快速有效地判定SAT問題的可滿足性。硬件SAT求解器可以從根本上解決傳統軟件 求解器的效率瓶頸，將SAT的求解過程加速到極致。

目前國內外已經開發出幾種SAT硬件求解器，這些求解器均選用了計算能力強的現場可編程門陣列 (FPGA)，作為硬件實現平臺。可以將這些硬件求解器分為兩種類型：實例型算法芯片和應用型算法芯片。

對于實例型方法，其硬件結構針對每一個實例獨立開發、配置和驗證芯片，而后對芯片加電進行SAT 實例的計算。這種方法中，每一個的實例對應不同的硬件結構，每一個芯片只能進行某種實例的求解運算， 這種方法的通用性較差，成本較高，但是這種方法充分發揮了數字電路系統的內在特征，完全避免了上述 軟件和應用型方法面臨的挑戰，將非常適用于大規模的SAT實例。

而應用型方法，其目的在于開發一種通用的SAT硬件芯片，這種方法本質上是對軟件SAT算法的硬 件實現，既使用FPGA實現一些瓶頸算法，最終的求解器工作在軟硬件協同的機制下。這種方法的優點在 于通用性，即只需要進行一次編譯和配置的過程，然后可以對所有實例進行計算。其缺點在于，這種解決 機制本質上并沒有將電路系統的特征引入SAT的求解中來，而僅僅使用了FPGA的可編程特征，所以這種 方案依然會遇到與軟件求解器相同的挑戰。