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

A Satisfiability Modulo Theories Method For Software And Hardware Division

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

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 knowl-edge, itwouldbe thefirsttime to apply the SMT, as well as the SMT solvers including Z3, CVC4 and Math- SAT5, 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.