论文部分内容阅读
本文研究了软硬件协同设计中的性能和资源问题，包括系统的资源和时间估计，软硬件划分的性能优化问题等，并把软件形式化方法应用于这个领域，取得了一些成果。
有了描述系统功能的高层规范之后，设计者首先需要分析满足规范的各种设计可能性，根据情况尽早抛弃那些不好的或者违背各方面制约条件的设计，缩小设计空间。这样才能缩短设计周期，提高设计工作的效率，最终得到良好的设计。为了探索可能的设计空间，在高层面上根据规范进行资源和性能估计就显得尤为重要。为此我们设计了两个根据硬件高层规范估计系统的时间性能和硬件资源的算法。时间估计算法是一个利用分枝限界技术的优化算法，其中采用了一些新颖的限界技术，它能快速地动态删除一些不包含最优解的子空间，从而较快得到一个时间性能的最优下界。资源估计算法利用Tabu搜索技术，解决了在时间约束下的硬件运算资源估计问题。算法中把资源估计问题转化为简单的空间搜索问题的技术具有一般意义。实验表明，我们设计的这两个算法具有较好的性能和效率。为优化软硬件协同系统的整体性能，优化的软硬件划分方法起着关键性的作用。我们用时间自动机对软硬件划分方法进行建模，把问题转化为时间自动机的最优可达问题，而后利用模型检查工具(如UPPAAL)，可以得到软硬件划分的最优可行解。为进一步优化系统整体性能，我们在软硬件划分阶段之后设计了一个通信调度算法，它能缩短各通信部件的等待时间。
为了能对协同系统所涉及的时间和资源进行推理，我们基于Hoare&He的程序统一理论，建立了一个有关时间和资源的形式化语义模型，同时用实例说明了如何利用这个模型证明软硬件划分的正确性。
论文最后讨论了可能的进一步工作。