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