【作者】 金乃咏；

【导师】 何积丰；

【作者基本信息】 华东师范大学 ， 系统分析与集成， 2006， 博士

【摘要】 为更好地描述分析嵌入式系统的行为,近年来出现了系统级描述语言。但系统级程序通常是目标平台无关的。为了挖掘程序最大的运行性能,需要在设计空间中进行探索,将程序模块映射到各目标器件上,并且将各种有关实现细节的决策在新的程序文本中体现出来。这一“探索—决策—重写”的过程是一个不断地从抽象到具体的精化过程。而无论“探索”和“决策”的结果如何,对“重写”而言,都必须保证不在“重写”的过程中引入有违高层规范的实现错误。这需要有与之匹配的理论与工具的支持。 本文继承了用数学方法研究编译器设计的传统,以UTP为理论工具,着重探讨了与硬件综合相适应的有资源的指称语义理论框架。 在该理论框架中,静态资源模型给出了资源约束的“质”的一面。它指出只有当程序满足资源特性的时候,程序才能正常运行。否则,程序就会发生错误。该模型把所有有违资源特性的错误程序都归结为“取消作业”。这样处理的好处是便于构造正确性可证明的编译器设计的理论基础。在此基础上,我们给出了编译器设计的一般规范和三个应用。 资源不但有质的特性,也有量的特性。其后的有限资源模型是第一个模型在“量”的方面的扩展。它刻画了系统可用资源的数量将随程序的运行而减少,直至可用资源全部耗尽这一现象。同时我们发现在有限资源环境下资源重用带来的程序行为的不确定性,并探讨了消除这些不确定性的方法。 为了提高资源的利用率,我们通常会让几个并发进程共享资源。我们结合了CSP,UTP,Action Trace和Separation Logic等理论工具给出了统一解决资源冲突和访问冲突的并发进程共享资源模型,并用该方法讨论了资源共享中常见的冲突消解和死锁等问题。 除了正确性,好的编译器还应有较高的效率。编译器也是个程序,我们把程序比较的方法扩展到编译器比较上来,构造了“资源性能模型”。在考察了目标芯片的技术特性之后,我们给出了在预编译阶段,资源分配阶段,代码生成阶段和器件选型阶段等多个时期的硬件编译优化算法。理论和试验证明了这些方法的有效性。经优化,我们的综合器给出了小而快的网表。 这些资源预编译子句和资源分配算法为我们提供了高性能的资源定制和可靠的资源调度方法。而基于资源模型的硬件综合方法的本质是一个将程序从无资源约束环境转换到有资源约束环境的映射,它具有普遍的理论意义和应用价值。它不仅适用于硬件综合,也可用于软件编译,特别是可重定向软件编译器设计。更多还原

【Abstract】 System level design languages(SLDL) are designed for better describing and analyzing the behavior of Embedded Systems. Programs coded in SLDL usually abstract from target computing resources. To get the optimal execution performance, one needs to explore the design spaces, make decisions on implementation details, and express those decisions in transformed programs. Such a continuous "exploration-decision-rewriting" process refines the source programs. And no matter what the results of exploration and decision are, one shall make sure that errors are not introduced in rewriting. That depends on the support of corresponding theories and tools.This paper inherits the tradition of designing compilers by mathematic methods. Founded on UTP, it focuses on a denotational resource model framework for hardware synthesizer design.In this framework, static resource model depicts the "quality" aspect of resource constraints. A program can terminate correctly only when resource constraints are satisfied. That model reduces all errors caused by resource constraint violations to "abort". The benefit is that one can build up the theory of correctness provable compiler easily. In light of that, we propose a specification for pre-compilers and demonstrate three applications.Besides "quality", "quantity" is another important aspect of resources. The following limited resource model expands the first static resource model. It aims to depict the phenomena that resources may get less and less along with the execution of programs. Meanwhile, we discover the non-determinacy in resource reuse and propose methods for removing non-determinacy.Sharing resources among several parallel processes is an effective approach to promote resource efficiency. Armed with CSP, UTP, Action Trace and Separation Logic, we propose a shared resource model which unifies solutions to resource conflicts and access conflicts. Conflicts and deadlocks are prone to happen and destructive to parallel systems when we share resources. We discuss methods to resolve these problems as well.In addition to correctness, we prefer a compiler with better performance. We apply the method for program comparison on compiler comparison and propose a resource performance model. After investigating features of our target chips, we get a series of optimization algorithms. Theory and practice justifies their effectiveness. And they contribute us quick and small chips.The essence of resource model based hardware synthesizer design method is a map from non resource constraint environment to resource constrained environment. That view has general theoretical and practical value. Its application is not just limited to hardware synthesis, but also to software compilation, especially to retargetable compiler design.更多还原