集成电路设计的复杂程度和设计规模呈指数增长,验证技术已经成为整个集成电路设计领域的瓶颈,利用BDD技术的形式验证方法在面对小规模以及中等规模电路时能够显示出优势,大规模电路呈指数增长的情况下并不适用。随着近些年计算机领域研究者对可满足性问题的深入研究并取得巨大进展,使得实践和理论当中的很多之前无法解决的问题能够转化为SAT问题后再进行解决。但以zChaff、DPLL等求解可满足问题的算法程序为基础的软件SAT求解器对大规模电路以及特定领域问题效果不佳。本文采用硬件模拟的办法来求解SAT问题,将SAT问题映射为现场可编程门阵列(FPGA)芯片,由FPGA芯片自主求解此问题。具体而言,我们研究了针对实际系统的CNF公式实例,自动化地定制编译和转换为FPGA芯片,由这种SAT求解芯片自主求解SAT问题的技术。论文中提出的流程构成了一个从CNF公式到电路的转换、FPGA芯片仿真、综合、验证、配置、下载和自主验证的统一框架,可以方便快速判断CNF式是否可满足,在自动化设计分析与验证领域具有深远意义。