毛乐乐,胡小勤,卢　晨

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

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



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

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

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

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

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

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

0引言

在传统的芯片设计中，工程师一般是凭经验进行软硬件划分，但随着电子技术的发展，嵌入式的系统设计变得越来越复杂，设计周期要求越来越短，性能控制也要求越来越高，仅凭经验已经无法满足设计周期，性能控制的要求，而且系统的软硬件划分结果直接影响着后续的软硬件协同设计，因此软硬件划分技术成为当前信息领域的研究热点之一.系统的硬件与软件都有各自的优缺点，硬件执行速度快成本较高的特点与软件执……