可满足模理论在软硬件划分领域的应用*

毛乐乐,胡小勤,卢　晨

(广西民族大学,a.广西混杂计算与集成电路设计分析重点实验室；

b.信息科学与工程学院，广西 南宁 530006)



可满足模理论在软硬件划分领域的应用*

毛乐乐a,胡小勤a,卢晨b

(广西民族大学,a.广西混杂计算与集成电路设计分析重点实验室；

b.信息科学与工程学院，广西 南宁 530006)

摘要：软硬件划分是评价软硬件协同设计优劣，甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题，借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案，使得系统的软硬件实现代价最小，经实验验证，针对软硬件划分问题，Z3的综合性能要优于另外两种解决器.采用可满足性问题求解方案，不仅克服了传统启发式算法陷入局部最优解的弊端，同时也弥补了规划类算法不适应于大规模划分问题的不足.

关键词：软硬件协同设计；软硬件划分；可满足模理论；可满足模理论求解器

0引言

在传统的芯片设计中，工程师一般是凭经验进行软硬件划分，但随着电子技术的发展，嵌入式的系统设计变得越来越复杂，设计周期要求越来越短，性能控制也要求越来越高，仅凭经验已经无法满足设计周期，性能控制的要求，而且系统的软硬件划分结果直接影响着后续的软硬件协同设计，因此软硬件划分技术成为当前信息领域的研究热点之一.系统的硬件与软件都有各自的优缺点，硬件执行速度快成本较高的特点与软件执行速度较慢成本却相对较低的特点互补，因此嵌入式系统可以分别交由软件和硬件实现，其中关键部分交由硬件实现，非关键部分交由软件实现.通过此方法可以将系统功能行为最优地分配到软硬件系统结构上.因此目前大部分嵌入式系统都要经过软硬件划分以获得高性能、低成本的优化效果.

国外从20世纪90年代开始探索软硬件划分方法, 在初期研究者将整数线性规划等规划类方法应用于软硬件划分并进行求解.文献[1-2]提出应用贪婪算法实现.文献[3]提出将所有的系统任务节点首先映射到将系统功能实现从全硬件功能逐步划分到软件功能软件，然后将部分任务节点逐步映射到硬件的方法实现软硬件划分.但是应用于软硬件划分问题的规划类算法执行时间较长，一般适用于较小规模的软硬件划分问题，当问题规模较大时，并不适用并且全局搜索能力较差.2000年，国内开始着手解决软硬件划分问题的相关研究，为了更好地解决软硬件划分问题，国内学者也在不断尝试，不断探索，2002年刘功杰等人提出遗传算法(GA)[4]的软硬件划分算法，2004年邹谊等人将量子遗传算法(QGA)[5]应用到软硬件划分;2007年郭荣华等人提出混合量子遗传算法(HQGA)[6]用于求解大模的系统软硬件划分问题;2010年，刘安等人将遗传算子引入到粒子群优化算法(PSO)[7]中应用于软硬件划分.上述提出的软硬件划分算法较复杂，运行时间较长, 而且传统启发式算法建模相对复杂，同时还有一个共同的弊端：容易陷入局部最优.

文章首次将软硬件划分问题转化为SMT问题，即将可满足模理论应用到软硬件划分问题并借助可满足问题解决器Z3、CVC4与MathSAT5解决器求得最优的软硬件划分方案，使得系统的软硬件实现代价最小.利用可满足模理论不仅克服了传统启发式算法陷入局部最优解的弊端，同时也弥补了规划类算法不适应于大规模划分问题的不足.而且应用表现优秀的SMT解决器,建立的软硬件划分模型也相对简单.通过对比三种SMT解决器执行相同变量求得全局最优解的时间以及软硬件的实现代价,得出Z3的综合性能要优于另外两种解决器，划分问题规模越大，效果越明显.这篇文章从新角度尝试探索解决软硬件划分问题的新途径.

1软硬件划分问题的描述与数学模型

软硬件划分是软硬件协同设计的重要环节和组成部分，其主要任务是在满足各项设计约束的条件下，把系统功能划分到目标结构中的软件和硬件部分上，并为系统提供最佳的软硬件划分方案.

这篇文章利用可满足模理论在短时间内生成一套执行时间少，系统总代价小的高质量划分方案.

求解软硬件划分问题时，通常使用无向图来描述任务流图.

定义1R={R0,R1,…,Rn}代表划分系统的所有任务节点集合,其中Ri表示第i个任务节点，其中i=0,1,2,…,n.图中的一个节点就是对应划分系统的一个任务，每个节点包含其软件、硬件代价信息,例如采用硬件时的运行时间和采用软件时在处理器上执行时间.

定义2系统总代价由软件代价和硬件代价组成，即系统总代价为软件代价与硬件代价之和，第m次划分后系统总代价用Vm+1表示，其中m=0,1,…,n.即没有进行划分时系统总代价为V1，第一次划分后的系统总代价为V2，系统每进行一次划分便得到一次优化，系统总代价将减小，因此V2≤V1.

定义3软硬件划分问题中我们可以得出x=(x0,x1,x2,…,xn)是划分系统任务流图的一个可行解，代表对系统的一种划分，xi{0,1}，xi=1代表Ri由软件实现，xi=0代表Ri由硬件实现，其中i代表第i个节点, i=0,1,2,…,n.

定义4 软件代价si是在[0,10]中随机产生并服从均匀分布，硬件代价hi是在[0 ,10]中随机产生服从均匀分布，其中i=0,1,2,…,n.

1.1软硬件划分问题定义

软硬件划分实质是对节点集合做划分，即将原节点集合R={R0,R1,…,Rn}划分为两个子集，即Q=(Rh,RS)，其中Rh∪RS=R且Rh∩RS=Φ.

软硬件划分问题：在满足性能约束的条件下，将一个节点集合R划分，分别映射到软件和硬件实现，映射到软件实现需要消耗软件代价，同理映射到硬件实现需要消耗硬件代价，划分后的系统硬件代价和软件代价的形式化定义分别为式(1),式(2).

HR=∑Ri∈Rhhi

(1)

式中，hi，si分别表示第i个节点交由硬件实现或软件实现所消耗的代价.

SR=∑Ri∈RSsi

(2)

给定软件代价函数,硬件代价函数,以及约束Vm+1，由于软硬件代价大于零，所以Vm+1>0，求解一种软硬件划分，使得系统的开销最小.

用x=(x0,x1,x2,…,xn)表示一个划分即划分系统任务流图的一个可行解，xi=1代表Ri由软件实现，xi=0代表Ri由硬件实现，则系统的软件代价和硬件代价可分别表示为式(3)，式(4).

(3)

(4)

在第m次软硬件划分后，满足

S(x)+ H(x)

(5)

即

(6)

软硬件划分问题：在满足性能约束的条件下，将一个节点集合R={R0,R1,…,Rn}进行划分，分别映射到软件和硬件实现，系统的软硬件划分完成后可以使得系统的软硬件代价最小，整个问题转化成规划问题：

目标函数MinCost(x)

约束函数Cost(x)

系统经过每一次软硬件划分后，都会产生一个新的系统代价，并且新的系统代价要比上一次的系统代价小.若进行m次划分后的系统总代价用Vm+1表示，则Vm+2≤Vm+1，如此不断划分寻找满足条件的最小值Vm+1.

1.2基于SMT的软硬件划分模型

可满足性理论(SatisfiabilityModuloTheories,SMT)是布尔可满足问题的扩展，它是对多类型一阶逻辑公式进行可满足性判定的理论.

假设要进行判定的SMT公式如下：

φ∶=(x1∧x2)∨x3

(7)

若x1,x2,x3为布尔量用SMT-LIB[8]标准语言描述公式φ，有smt2文件：

(declare-constx1Int)

(declare-constx2Int)

(declare-constx3Int)

(assert(or(= x10) (= x11)))

(assert(or(= x20) (= x21)))

(assert(or(= x30) (= x31)))

(assert(or(andx1x2) x3))

(check-sat)

(get-value(x1x2x3))

将此smt2文件作为SMT解决器的输入参数，经过SMT解决器处理后可以判断出SMT公式是可满足的还是不可满足的，以及输出当公式可满足时x1,x2,x3的值.

因此我们要将软硬件划分问题转化为SMT问题，必须将软硬件划分模型形式化为smt2文件形式.

将软硬件划分问题转化为SMT问题分为以下几个步骤：

第一步：在软硬件划分中将原节点集合R={R0,R1,…,Rn}划分为两个子集，即Q=(Rh,RS)，其中Rh∪RS=R且Rh∩RS=Φ，x=(x0,x1,x2,x3,…,xn)是划分系统任务流图的一个可行解，整数xi为1或为0，当xi=1时代表Ri交由软件实现，xi=0时代表Ri交由硬件实现，即将系统划分为软硬件两部分.

将原节点集合划分问题转化成SMT问题即用SMT-LIB标准语言描述得下式：

(declare-constxiInt)

(8)

(assert(or(= xi0) (= xi1)))

(9)

即将第i个节点交由软件或硬件实现.将软硬件划分中约束函数

转化成SMT问题描述如下：

(assert(<(+ (* xisi) (* (- 1 xi) hi)) Vm+1))

(10)

SMT-LIB描述几个最基本的理论有抽象函数等式，线性算数，差分逻辑，位向量以及数组等，这篇文章应用到线性算数理论.

线性算数(LinearArithmetic,LA)是算数函数只有“+”“-”的理论，谓词符号一般只有(=、≤、<)，只允许数与变量的乘法，如整数的3·x，在实数上也允许分子形式的数乘，根据处理的类型不同可以分为整数上和实数上的LA理论.LA公式的一般形式为：

X1+3X2≤6X3

(11)

在smt2文件中LA理论应用于

(assert(<(+ (* xisi) (* (- 1 xi) hi)) Vm+1) )

第二步：分别调用Z3、CVC4、MathSAT5解决器处理并判断公式(10)是可满足的还是不可满足的，并在可满足时输出一组x=(x0,x1,x2,…,xn).

将此组x=(x0,x1,x2,…,xn)带入公式(12):

(assert(=(+ (* xisi) (* (- 1 xi) hi)) Vm+2)

(12)

可以得到一个新的软硬件代价Vm+2.

第三步：重复执行第二步骤，直至不可满足时，停止迭代，则在不可满足的情况下之前的一组x=(x0,x1,x2,…,xn)即为全局最优解.

1.3求解过程

基于SMT软硬件划分的伪代码如下：

Init( h, s,v1, v2);

result1=result2=z3(h, s, v2);

while(1)

{

result1=result2;

result2=output(z3);

v1=v2;

v2=new_v(r2, h, s);

if(result2.sat= =1)

{

z3(h, s, v2);

}

if(result2.sat==0)

{

break;

}

}

Record result1;

首先初始化软硬件代价系数h，s和总代价v1，v2.然后生成z3的输入文件，调用z3，求得新的划分，将划分的结果保存到result1和result2中.其中v1表示前一个划分下的软硬件代价的总和，v2表示当前划分下的软硬件代价的总和.result1表示前一个划分的结果，result2表示当前划分的结果.接着循环调用z3直到result2不可满足时，result1即为所求得的划分结果.

2仿真实例与分析

操作系统：64位centos 6.3，CPU：Intel(R)Core(TM)i5-3470，RAM：12.00 GB.

所使用的编程语言：C++,gccg++.

运用的SMT解决器:Z3、CVC4、Mathsat5.

Z3[9]是微软公司研发的一个高效、可扩展与表达性强的SMT求解器.曾在SMT-COMP竞赛中表现不俗，是到目前为止综合求解能力最强的SMT求解器.

CVC是由纽约大学和爱荷华大学共同领导开发，具有给出证明和模型的推导能力等优点.最新的CVC系列的解决器是CVC4.

MathSAT是由FBK(Fondazione Bruno Kessler)和特伦托大学联合研发，MathSAT的DPLL的引擎是基于一个高效的SAT解决器.最新MathSAT系列的解决器是MathSAT5.

以节点为4为例,即i=4得约束函数公式：

s0*x0+h0*(1-x0)+s1*x1+h1*(1-x1)+s2*x2+h2*(1-x2)+s3*x3+h3*(1-x3)

(13)

用SMT-LIB标准语言描述公式(13),即将软硬件划分问题转化为SMT问题建立模型如下:

(declare-constx0Int)

(declare-constx1Int)

(declare-constx2Int)

(declare-constx3Int)

(assert(or(= x00) (= x01)))

(assert(or(= x10) (= x11)))

(assert(or(= x20) (= x21)))

(assert(or(= x30) (= x31)))

(assert(<(+ (+ (+ (+ (+ (+ (+(* x0

3.85) (* (- 1 x0) 4.32)) (* x13.63)) (*

(- 1 x1) 1.13)) (* x21.74)) (* (- 1 x2)1.9))

(* x31.75)) (* (- 1 x3) 1.09)) 17.6) )

(check-sat)

(get-value (x0x1x2x3))

此Benchmarks是SMT-LIB用于比较各SMT解决器的求解效率而编写的用例，随后调用Z3求解得x0=0,x1=1,x2=0和x3=0.执行时间为0.356523 s，系统软硬件代价为14.6.此外我们还作了大量的实例分析，部分结果如表1所示.

对比表1中的统计数据可以得出，调用MathSAT解决器在变量为0～15范围内比Z3和CVC4解决器较快.调用Z3解决器在变量为15～178范围内比MathSAT5、CVC4较快，系统的软硬件实现总代价较小.CVC4解决器在各变量范围内执行时间最长，系统的软硬件实现代价最大.Z3在这篇文章的测试中具有时间开销小，系统软硬件开销小的性能特点，具有较强的求解实力，CVC4在求解可满足解时求解能力欠佳，MathSAT5在求解不可满足解时求解能力欠佳.

表1　实验结果

3结语

文章首次将可满足模理论应用于软硬件划分问题，并借助SMT解决器Z3、CVC4与MathSAT5求得最优的软硬件划分方案，使得软硬件实现代价最小.实验证明文中提出的方法是有效可行的，为研究软硬件划分问题提供了新的思路，同时证明Z3的综合性能是最好的.但是随着嵌入式系统的软硬件设计越来越复杂，在软硬件划分研究中将迎来更多挑战，需进一步完善可满足理论在软硬件划分问题上的应用，增加更多的参数到软硬件划分，例如通信代价等.

[参考文献]

[1]R. K. Gupta.Co-synthesis of hardware and software for digital embedded systems[D].PhDthesis,Stanford University, December 1993.

[2]P.Arato,S.Juhasz,Z.A.Mann.Hardware-software partitioningin embedded system design[A].WISP2003, Budapest,Hungary,September，2003:197-222.

[3]R.Ernst,J.Henkel,T.Benner.Hardware-softwarecosynt-hesis for microcontrollers[J].IEEE Design Test Comput，1993,10(4):64-75.

[4]G.Liu,L.Zhang,S.Li.Genetic algorithm inhardware/software partitioningapplications[J].Journal of National University of Defense Technology，2002, 24(2):64-68.

[5] 邹谊，庄镇泉，李斌.基于量子遗传算法的嵌入式系统软硬件划分算法[J].电路与系统学报,2004,9(5):1-7.

[6]R.Guo,B.Li,Y.Zou,Z.Zhuang.Hybrid quanturnprobabilistic coding genetic algorithm forlargescale hardware-software co-synthesis of embedded system [J].IEEE Congress on Evolutionary Computation,2007:3454-3458.

[7]A.Liu,J.Feng,X.Liang,X.Yang.Based on Geneticparticleswarm optimization of embedded system hardware-software partitioningalgorith[J].Journal of computer aided design and graphis,2010,22(6):927 -933.

[8]The Satisfiability ModuloTheories Library[EB/OL]. http://www.smt-lib.org/.

[9]Project Hosting For Open Source Software[EB/OL]. http://z3.codeplex.com/.

[责任编辑苏琴]

[责任校对黄招扬]

A Satisfiability Modulo Theories Method For Software And Hardware Division

MAO Le-lea,HU Xiao-qina,LU Chenb

(a.GuangxiKeyLaboratoryofHybridComputationandICDesignAnalysis；b.CollegeofInformationScienceandEngineering,

GuangxiUniversityforNationalities,Nanning530006,China)

Abstract:The hardware/software partition is one of the standard of evaluating the software/hardware co-design,a bad partition might make a worse co-design, or even a fail design. Inthispaper,The hardware/softwarepartitionproblemwas modeled with formulas of Satisfiability Modulo Theory (SMT).In our knowledge,itwouldbe thefirsttime to apply the SMT,as well as the SMT solvers including Z3,CVC4 and MathSAT5,tohardware/softwarepartitionproblem.According to the experiments,the optimizedpartition with the SMT and solvers,more-over,the Z3 solver is proved as the more efficient for hardware/software partition.In short,in terms of the SMT and its solvers,the method avoid the local optimized solution of the partition problem,as well as the method could be applied in the large scale of the co-design.

Key Words:Software/hardware；Co-design；The hardware/softwarepartition；SMT；SMT solvers

中图分类号：TP301.6

文献标识码：A

文章编号：1673-8462(2016)01-0078-05

作者简介：毛乐乐(1989-)，河北衡水人，广西民族大学信息科学与工程学院硕士研究生，研究方向：大规模集成电路验证.

基金项目：广西民族大学研究生教育创新计划(gxun-chxs2015097).

收稿日期：2015-10-16.