Study on Language Processing for Plastic Cell Architecture

我们研究了一个基于FPGA芯片的sat求解器的设计与实现。虽然有许多SAT求解器在软件中实现，但我们的目标是通过制造一台直接解决SAT问题的机器来提高求解器的性能。采用Verilog HDL硬件描述语言对机器进行描述，并将其编程到FPGA芯片上。它执行模型生成方法，并进行了一些修改，以提高其性能。通过并行执行值传播和可满足性测试，实现了较高的速度。然而，我们失去了空间效率，因为每个公式都是由顺序电路表示的，每个公式都通过组合电路连接到其他公式。尽管效率不高，但实验结果表明，在解决一些基准SAT问题时，性能得到了显著提高。为了提高空间效率，我们改进了这种早期设计。我们发现在数据表示和推理引擎状态等方面存在大量冗余。因此，我们试图通过以下方法来消除冗余：(1)通过修改介词变量状态的表示方法来减少寄存器的数量；(2)将推理引擎的状态数量从10个减少到6个；(3)引入BCBE（Burning Candle at Both Ends）电路以实现有效的隐含；(4)通过划分竞赛电路来缩短关键路径，该电路选择一个介词变量进行大小写分割。实验结果表明，新实现在执行时间和电路尺寸上都优于旧实现。

We studied the design and implementation of a SAT-solver on an FPGA chip. While there are many SAT-solvers implemented in software, we aimed to improve the solver's performance by making a machine that solves SAT problems directly.The machine was described by the Verilog HDL hardware description language and programmed onto a FPGA chip. It performs the model generation method with some modifications that enhance its performance. We achieved high speed by parallel executions of value propagation and satisfiability tests. However, we lost space efficiency because every formula is represented by a sequential circuit and each formula is connected to other formulas via combinatorial circuits. In spite of this inefficiency, experimental results show significant performance gains in solving some benchmark SAT problemsIn order to improve space efficiency, we refined this early design. We found much redundancy in data representation and states of the inference engine, etc. Thus, we tried to eliminate the redundancy by (1)decreasing the number of registers by modifying the representation method of prepositional varaible's state, (2)decreasing the number of states of the inference engine from 10 to 6, (3)introducing the BCBE(Burning Candle at Both Ends) circuit for efficient implication, and (4)shortening the critical path by dividing the tournament circuit which chooses a prepositional variable for case splitting. Experimental results show that the new implementation outperforms the old one with regard to both execution time and circuit size.