基于伪布尔可满足性的纳米CMOS电路单元配置

王先建 王伦耀 储著飞 夏银水

(宁波大学信息科学与工程学院 宁波 315211)

1 引言

CMOL电路是结合纳米技术和传统 CMOS工艺的 CMOS/纳米线/分子混合(CMOS/nanowire/MOLecular hybrid, CMOL)电路结构[1]，而且文献[2]从理论上证明了 CMOL电路进行单元配置可实现电路逻辑功能的完备性。由于CMOL电路结构既保留了目前成熟的CMOS工艺，同时又具有纳电子器件所具有的高密度特点而受到研究者们的广泛关注，其研究内容包括 CMOL存储器[3]、CMOL FPGA[4]以及神经元电路[5]等等。而在有关 CMOL CAD的研究中，CMOL的单元配置方法一直是一个重要内容[4,6-8]，因为它是 CMOL电路实现特定功能必经的步骤。

目前对 CMOL电路的单元配置方法已经开展了一些研究。这些方法包括基于逻辑簇(Tile)的设计方法[4]，基于力矢量算法[6]，启发式算法[7]以及电路等效变换法[8]等，并发展出了CMOL自动综合工具CMOL FPGA CAD 1.0[4]。

CMOL电路的单元配置问题实际上也可以被描述成一个可满足性问题(Satisfiability Problem)，因此可以利用布尔可满足性(Boolean Satisfiability,SAT)来解决 CMOL电路的单元配置问题。但在已发表的利用SAT实现CMOL电路单元配置的方法中[9]，由于采用二项式编码[10]，使得子句的个数过多、中间处理文件过大，影响了算法的效率和处理电路大小的能力。相比于用合取范式(Conjunctive Normal Form, CNF)表示的约束，伪布尔(Pseudo-Boolean, PB)约束更加容易表示[11-15]。目前伪布尔可满足性(Pseudo-Boolean Satisfiability, PBS)法[11]已被成功应用于低功耗状态分配[12]和最大电路开关性估计[13]等领域中。本文提出利用 PBS法来解决CMOL电路的单元配置问题，该方法在不增加额外的布尔变量集个数的条件下，通过降低编码过程中的约束个数[10,11]达到减少中间处理文件大小的目的。实验结果表明，相比于文献[9]的基于传统SAT的CMOL单元配置方法，本文采用的方法能有效减少中间处理文件大小，达到加快算法速度和提高求解电路规模的目的。

2 CMOL FPGA结构

在CMOL电路中，纳米线以一定的长度周期性断开，纳米线的这种特点使得每一个CMOL单元只能与周围M=2r(r-1)-1个其它 CMOL单元相连，其中r为连通域半径。以图1为例，其中r为3，图中深灰色单元C只能与周围 11个浅灰色单元连通，这些浅灰色单元构成了深灰色单元的连通域。此外，CMOL电路中的两点相对位置常用曼哈顿距离来表示。如在图1中，C,D两个CMOL单元的坐标分别为C(x1,y1),D(x2,y2)，则它们之间的曼哈顿距离为|x1-x2|+|y1-y2|。利用连通域半径和曼哈顿距离就可以确定某一CMOL单元的连通域。以图1为例，在图1中坐标原点在C上，坐标轴将图1分为4块，分别为第1至第4象限，则当图1中某一点D与C的曼哈顿距离分别不大于r,r-1,r-2 及r-1时，那么满足这些曼哈顿距离约束条件的CMOL单元D的个数就是CMOL单元C的连通域大小。

图1 CMOL FPGA

3 CMOL单元配置问题的PBS描述

3.1 伪布尔可满足性

SAT是用来解决给定的布尔方程是否存在一组变量赋值使问题为可满足。而布尔方程的描述常采用CNF来表示。在CNF中，由m个子句w1,…,wm的合取组成；而子句由k个文字的析取组成。其中一个文字即为一个变量或者其反变量。因此，为了满足一个式子，每一个子句必须至少有一个文字的值为真。

随着SAT法的快速发展，SAT求解器被扩展用来处理PB约束，即为带整数系数的线性不等式。伪布尔可满足性问题可表示为 PB约束的合取，其中PB约束可表示为

式(1)中ai和b为整数常数；li为一个文字，可表示为变量xi和其反变量，即li=xi或者li=，其中xi∈{0,1},；“▷”为关系操作符，可表示“=”，“＞”，“≥”，“＜”或者“≤”。若式(1)中的|ai|都为同一个数a0时，则式(1)对应的 PB约束称为基数约束(cardinality constraints)，即

假设一个PB式子F为PB约束的合取。对于PBS问题，如果存在一组配置解x1,…,xm满足所有的PB约束使得F为真，则表示F可满足，这一组解即为可配置解。

例如，给定一个F(x1,x2,x3)=(2x1-2x2≥1)∧(x1+x2+3≥1)，它由3个布尔变量，5个文字，2个 PB约束组成。{x1=1,x2=0,x3=1}和{x1=1,x2=0,x3=0}等都为可满足配置解。

3.2 CMOL单元配置问题的PBS描述

由于CMOL电路仅适于“或非/非”逻辑电路，因此在进行 CMOL单元配置之前需要对原始电路进行转换，该转换可以借助逻辑综合工具SIS将由“与/或/非”逻辑电路转换成“或非/非”逻辑电路。而 CMOL单元配置过程就是通过设置可配置纳米二极管的状态，将一个给定的逻辑电路功能用CMOL FPGA实现的过程。

在CMOL单元配置过程中，一般将电路输入输出端口放在CMOL电路的四周。因此对于一个由行(row)，列(column)构成的CMOL单元阵列，令C表示该阵列的CMOL单元集合，||C||表示集合C中的元素个数；C1表示位于C边界上的 CMOL单元集合，||C1||表示集合C1中的元素个数；C2表示位于非C边界上的CMOL单元集合，||C2||表示集合C2中的元素个数。则有

由于CMOL电路结构存在连通域约束，因此对于一个CMOL单元c,c∈C,D(c)为构成c的连通域的CMOL单元的集合，则有

给定一个基于“或非/非”逻辑的电路K，电路K可被看作是一个无环有向图(Directed Acyclic Graph, DAG)，即K=(G,E)。其中G为对应于“或非/非”门的节点集合，E=G×G表示连接的门与门的边的集合。对于电路中的任意门g,g'∈G，要想得到(g,g')∈E，当且仅当门g的输出与门g'的输入相连，亦即

根据逻辑门在逻辑电路中所处的位置的不同，可以将逻辑门集合G分为3个子集，即G1,G2和G3，分别表示输入端口的逻辑门集合，输出端口的逻辑门集合和非输入输出端口的逻辑门集合，并用||G1||,||G2||和||G3||表示各子集中包含的元素个数。并且有

CMOL单元配置问题则可描述为将给定的电路逻辑门的集合G配置到 CMOL单元集合C中是否存在可配置解的问题。CMOL单元配置问题可用数学式描述成一个内射函数P，即P:G→C。在进行CMOL单元配置过程中，至少要满足以下4个约束：

(1)与输入、输出端口相连的门必须被配置到阵列边界的CMOL单元上，作为I/O口，即

(2)每个“或非/非”门必须被配置到有且仅有一个CMOL单元上，即

(3)两个或者两个以上不同的门不能被配置到同一个CMOL单元上，即

(4)电路中有连接关系的门单元位于各自的连通域中，即

考虑到 CNF中子句的数量与布尔变量成指数级增加，为此本文在不增加额外的布尔变量集个数的条件下，采用PB约束代替CNF，达到减少约束个数的目的。在描述CMOL单元配置问题时，ai为0或1,b为 1，相关的PB约束可以表示为以下 3种约束，分别为：

(1)关系操作符“▷”为“≤”时，即为“至多一个”基数约束，简称AMO(At-Most-One)约束，即

(2)关系操作符“▷”为“≥”时，即为“至少一个”基数约束，简称ALO(At-Least-One)约束。这种PB约束等价于标准的SAT子句，即

(3)关系操作符“▷”为“=”时，即为“有且仅有一个”基数约束，简称EO(Exactly-One)约束，即

CMOL单元配置问题主要由这3种基数约束来表示，从3种基数约束可以看出，只须对AMO约束进行改进即可。传统的SAT法针对AMO约束采用二项式编码法，即

在本文中，布尔变量表示将门g配置到CMOL单元c中，其中g∈G和c∈C。因此给定一个电路G和CMOL单元阵列，符合式(7)-式(10)的CMOL单元配置可以被编码成以下几种类型的PB约束：

(1)当门g必须被配置到有且仅有一个 CMOL单元c上，即可编码成

(2)当CMOL单元c至多被一个门g配置，即可编码成

(3)当门g'配置在CMOL单元c上，那么与门g'的输入线有连接关系的门g应该配置在CMOL单元c的连通域范围内，即可编码成

将式(15)-式(17)中的PB约束集导入PBS求解器中。针对CMOL单元配置时碰到的实际问题，可导入更多其它的PB约束。例如，任意的“或非/非”门可以配置到满足以上 PB约束的任意的CMOL单元上。考虑到属于G1和G2的门被要求配置在阵列边界当作I/O口，因此可设置 Σc∈C1=1。这样能够通过PB约束传播达到简化CMOL单元配置问题。

PBS法的具体步骤为：

步骤 1 通过 SIS逻辑综合工具将原始 BLIF电路网表文件转换成全由“或非/非”门组成的BLIF格式电路文件；

步骤 2 读入基于“或非/非”门的BLIF电路，对输入信号、“或非/非”门等进行标号；

步骤 3 根据标号的个数以及I/O个数来设置CMOL单元阵列大小；

步骤 4 应用PBS法根据式(7)-式(10)的条件约束将基于“或非/非”门的 BLIF电路配置到CMOL单元阵列中；

步骤 5 将步骤 4中的所有 PB约束导入到PBS求解器中，如果有一个解满足所有的PB约束，那这个解就是CMOL单元配置解，反之则无可配置解。

4 实例说明

下面以全加器为例子来说明一个原始的电路是如何利用PBS法配置到CMOL电路中的。

步骤 1 通过 SIS逻辑综合工具对原始全加器的BLIF电路网表文件转换成由“或非/非”门组成的BLIF格式电路文件，如图2(a)所示。

步骤 2 由图 2(a)中可以看出，电路有 3个输入信号A,B,C, 2个输出信号Sum,D，有 15个标号，其中标号1, 2, 3为输入信号，标号11, 15为输出信号门，标号4, 5, 6为“非”门，标号7, 8,9, 10, 11, 12, 13, 14, 15为“或非”门。并将它们之间的连接关系进行记录，例如标号 11的门与标号7, 8, 9, 10的门相连。

步骤 3 此例可设置5×4大小的 CMOL单元阵列，如图2(b)所示。为与传统的SAT法进行公平对比，默认设置连通域半径r也为9。

图2 全加器实例

步骤5 将步骤4中的所有PB约束导入到PBS求解器中，如果有一个解满足所有的PB约束，那这个解就是CMOL单元配置解。即基于“或非/非”门的全加器电路成功配置到CMOL电路中。

5 实验结果

本文中提到的基于PBS的CMOL单元配置法用C语言编程实现，通过GCC编译，在linux操作系统及Intel Pentium Dual-core 3 GHz CPU, 2 GBRAM的PC环境下运行。表1中的数据是采用perl脚本语言对每个测试电路进行20次的实验测试，然后取出相对公平的中间值得到的。

表1 实验结果

从表1可以看出，相对于传统的SAT法，PBS法在没有增加额外的布尔变量集个数的基础上，SAT法中的子句个数平均为PBS法中的PB约束个数的126.29倍，说明PBS法比传统的SAT法更易表示、更简单。CNF大小平均为OPB大小的4.01倍。考虑到OPB文件为PB约束的合取，亦即单元配置过程中产生的中间处理文件，它的减小有利于CAD工具在运行过程中占用更少的内存，或可求解更大的电路。从时间来看，对于 s27, s386及 s444 3个电路，PBS法所用时间稍微比传统的SAT法略长一点，但从平均值角度看，PBS法求解速度要比传统的SAT法求解速度快9.03倍。并且传统的SAT法对于s420及s526两个电路无法求解，而PBS法可以。

6 结论

针对 CMOL单元配置问题，本文提出了基于PBS的单元配置方法。传统的SAT法在处理CMOL单元配置过程中，因采用二项式编码使得子句的个数过多、中间处理文件过大，影响了算法的效率和处理电路大小的能力。为此，本文在不增加额外的布尔变量集个数的条件下，通过降低约束个数、减小中间处理文件，将问题编码成PBS问题。实验结果表明，PBS法的PB约束个数比传统的SAT法的子句个数平均减少了126.29倍，中间处理文件大小平均减少了4.01倍，CPU运行时间平均快了9.03倍，并且增大了求解规模。

[1]Likharev K K and Strukov D B. CMOL: Devices, Circuits,and Architectures. Introducing Molecular Electronics[M].Berlin: Springer, 2005: 447-477.

[2]Chen Gang, Song Xiao-yu, and Hu Ping. A theoretical investigation on CMOL FPGA cell assignment problem[J].IEEE Transactions on Nanotechnology, 2009, 8(3): 322-329.

[3]Strukov D B and Likharev K K. Defect-tolerant architectures for nanoelectronic crossbar memories[J].Journal of Nanoscience and Nanotechnology, 2007, 7(1): 151-167.

[4]Strukov D B and Likharev K K. CMOL FPGA circuits[C].Proceedings of International Conference on Computer Design,Las Vegas, Nevada, USA, June 26-29, 2006: 213-219.

[5]Afifi A, Ayatollahi A, and Raissi F. CMOL implementation of spiking neurons and spike-timing dependent plasticity[J].International Journal of Circuit Theory and Applications,2011, 39(4): 357-372.

[6]Kim K, Karri R, and Orailoglu A. Design automation for hybrid CMOS-nanoelectronics crossbars[C]. Proceedings of IEEE International Symposium on Nanoscale Architectures,Los Alamitos, CA, USA, October 21-22, 2007: 27-32.

[7]Xia Yin-shui, Chu Zhu-fei, and Hung N N,et al.. An intergrate optimizaiton approach for nano-hybrid circuit cell mapping[J].IEEE Transactions on Nanotechnology, 2011,10(6): 1275-1284.

[8]夏银水, 储著飞, 王伦耀, 等. 纳米CMOS电路逻辑等效转换[J]. 电子与信息学报, 2011, 33(7): 1733-1737.

Xia Yin-shui, Chu Zhu-fei, and Wang Lun-yao,et al.. Logic equivalent transformation for nano-meter CMOS hybrid circuits[J].Jounal of Electronics&Information Technology,2011, 33(7): 1733-1737.

[9]Hung N N, Gao Chang-jian, and Song Xiao-yu,et al.. Defect tolerant CMOL cell assignment via satisfiability[J].IEEE Sensors Journal, 2008, 8(6): 823-830.

[10]Chen Jing-chao. A new SAT encoding of the at-most-one constraint[C]. Proceedings of the Tenth International Workshop on Constraint Modelling and Reformulating, St.Andrews, Scotland, UK, September 6, 2010.

[11]Roussel O and Manquinho V. Pseudo-Boolean and Cardinality Constraints. Handbook of Satisfibility[M].Amsterdam: IOS Press, 2009: 695-733.

[12]Sagahyroon A, Aloul F, and Sudnitson A. Using SAT-based techniques in low power state assignment[J].Journal of Circuits,Systems,and Computers, 2011, 20(8): 1-14.

[13]Mangassarian H, Veneris A, and Najm F N. Maximum circuit activity estimation using Pseudo-Boolean Satisfiability[J].IEEE Transactions on Computer-Aided Design of Intergrated Circuits and Systems, 2012, 31(2): 271-284.

[14]Eén N and Sörensson N. Translating Pseudo-Boolean constraints into SAT[J].Journal of Satisfiability,Boolean Modeling and Computation, 2006, 2: 1-26.

[15]Berre D Le and Parrain A. The Sat4j library, release 2.2 system description[J].Journal on Satisfiability,Boolean Modeling and Computation, 2010, 7: 59-64.