Resource Models And Hardware Synthesis For System Level Design Language

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.