资源模型与系统级描述语言的硬件综合
|
摘要
为更好地描述分析嵌入式系统的行为,近年来出现了系统级描述语言。但系统级程序通常是目标平台无关的。为了挖掘程序最大的运行性能,需要在设计空间中进行探索,将程序模块映射到各目标器件上,并且将各种有关实现细节的决策在新的程序文本中体现出来。这一“探索—决策—重写”的过程是一个不断地从抽象到具体的精化过程。而无论“探索”和“决策”的结果如何,对“重写”而言,都必须保证不在“重写”的过程中引入有违高层规范的实现错误。这需要有与之匹配的理论与工具的支持。
本文继承了用数学方法研究编译器设计的传统,以UTP为理论工具,着重探讨了与硬件综合相适应的有资源的指称语义理论框架。
在该理论框架中,静态资源模型给出了资源约束的“质”的一面。它指出只有当程序满足资源特性的时候,程序才能正常运行。否则,程序就会发生错误。该模型把所有有违资源特性的错误程序都归结为“取消作业”。这样处理的好处是便于构造正确性可证明的编译器设计的理论基础。在此基础上,我们给出了编译器设计的一般规范和三个应用。
资源不但有质的特性,也有量的特性。其后的有限资源模型是第一个模型在“量”的方面的扩展。它刻画了系统可用资源的数量将随程序的运行而减少,直至可用资源全部耗尽这一现象。同时我们发现在有限资源环境下资源重用带来的程序行为的不确定性,并探讨了消除这些不确定性的方法。
为了提高资源的利用率,我们通常会让几个并发进程共享资源。我们结合了CSP,UTP,Action Trace和Separation Logic等理论工具给出了统一解决资源冲突和访问冲突的并发进程共享资源模型,并用该方法讨论了资源共享中常见的冲突消解和死锁等问题。
除了正确性,好的编译器还应有较高的效率。编译器也是个程序,我们把程序比较的方法扩展到编译器比较上来,构造了“资源性能模型”。在考察了目标芯片的技术特性之后,我们给出了在预编译阶段,资源分配阶段,代码生成阶段和器件选型阶段等多个时期的硬件编译优化算法。理论和试验证明了这些方法的有效性。经优化,我们的综合器给出了小而快的网表。
这些资源预编译子句和资源分配算法为我们提供了高性能的资源定制和可靠的资源调度方法。而基于资源模型的硬件综合方法的本质是一个将程序从无资源约束环境转换到有资源约束环境的映射,它具有普遍的理论意义和应用价值。它不仅适用于硬件综合,也可用于软件编译,特别是可重定向软件编译器设计。
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.
本文继承了用数学方法研究编译器设计的传统,以UTP为理论工具,着重探讨了与硬件综合相适应的有资源的指称语义理论框架。
在该理论框架中,静态资源模型给出了资源约束的“质”的一面。它指出只有当程序满足资源特性的时候,程序才能正常运行。否则,程序就会发生错误。该模型把所有有违资源特性的错误程序都归结为“取消作业”。这样处理的好处是便于构造正确性可证明的编译器设计的理论基础。在此基础上,我们给出了编译器设计的一般规范和三个应用。
资源不但有质的特性,也有量的特性。其后的有限资源模型是第一个模型在“量”的方面的扩展。它刻画了系统可用资源的数量将随程序的运行而减少,直至可用资源全部耗尽这一现象。同时我们发现在有限资源环境下资源重用带来的程序行为的不确定性,并探讨了消除这些不确定性的方法。
为了提高资源的利用率,我们通常会让几个并发进程共享资源。我们结合了CSP,UTP,Action Trace和Separation Logic等理论工具给出了统一解决资源冲突和访问冲突的并发进程共享资源模型,并用该方法讨论了资源共享中常见的冲突消解和死锁等问题。
除了正确性,好的编译器还应有较高的效率。编译器也是个程序,我们把程序比较的方法扩展到编译器比较上来,构造了“资源性能模型”。在考察了目标芯片的技术特性之后,我们给出了在预编译阶段,资源分配阶段,代码生成阶段和器件选型阶段等多个时期的硬件编译优化算法。理论和试验证明了这些方法的有效性。经优化,我们的综合器给出了小而快的网表。
这些资源预编译子句和资源分配算法为我们提供了高性能的资源定制和可靠的资源调度方法。而基于资源模型的硬件综合方法的本质是一个将程序从无资源约束环境转换到有资源约束环境的映射,它具有普遍的理论意义和应用价值。它不仅适用于硬件综合,也可用于软件编译,特别是可重定向软件编译器设计。
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.
引文
[1] Accellera. http://www.systemc.org.
[2] Accellera. System Verilog Language Reference Manual,
[3] Accellera. Property Specification Language Reference Manual Version 1.1, June 2004.
[4] Actel Company. Axcelator Family FPGAs Detailed Specification, 2004.
[5] Alfred V. Aho, Ravi Sethi, and jeffery D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, Pearson Education, Inc, 1986.
[6] P. Alexander, R. Kamath, and D. Barton. System specification in rosetta. Proceeding of The IEEE Engineering of Computer Based Systems Symposium, April 2000.
[7] Altera Corporation. Stratix Device Family Data Sheet, 2004.
[8] ANSI. ANSI/EIA Standard 548-1988, EDIF 200.
[9] David F. Bacon, Susan L. Graham, and Oliver J. Sharp. Compiler transformations for highperformance computing. ACM Computing Survey, 26(4): 345-420, 1994.
[10] Stephen Bailey. VHDL does not need the System moniker. Mentor Graphics Corp.
[11] F. Balarin, P. Giusto, and et al. Hardware-Software Co-Design of Embedded Systems: The POLLS Approach. 1997.
[12] P. Bellows and B. Hutchings. Jhdl - an hdl for reconfigurable systems. In IEEE Symposium on FPGAs for Custom Computing Machines, 1998.
[13] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretic Computer Science, 37(1): 77-121, 1985.
[14] Gerard Berry and Georges Gonthier. The esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2): 87-152, 1992.
[15] Jonathan Bowen. Occam resources:http://archive.comlab.ox.ac.uk/occam.html.
[16] Jonathan Bowen. Animating the semantics of verilog using prolog. Technical Report 176, UNU-IIST, 1999.
[17] Jonathan Bowen and He Jifeng. An approach to the specification and verification of a hardware compilation scheme. The Journal of Supercomputing, 19(1): 23-29, 2001.
[18] Jonathan P. Bowen, Martin Franzle, Ernst-Rü diger Olderog, and Anders P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland, pages 176-187, 22-24 June 1993.
[19] Stephen Brookes. Retracing the semantics of csp. In BCS-FACS: 25 Years of CSP, 2004.
[20] Stephen Brookes. A semantics for concurrent separation logic. In Proceeding of CONCUR'O4, 2004.
[21] F. M. Brown. Boolean Reasoning. Kluwer Academic Publishers, 1990.
[22] Stephen Brown and Jonathan Rose. Architecture of fpga and cpld: A tutorial. Technical report, Department of Electral and Computer Engineering, 1997.
[23] Francesco Bruschi and Fabrizio Ferrandi. Synthesis of complex control structures from behavioral systemc models. In In Proceedings of Design, Automation and Test in Europe Conference (DATE'03 Designers' Forum), 2003.
[24] R.E. Bryant. Graph - based algorithms for boolean function manipulation. IEEE Trans. on Comp, 35(8): 677-691, 1986.
[25] R. Burstall and P. Landin. Programs and their proofs: an algebraic approach. Machine Intelligence, 7: 17-43, 1969.
[26] Karl-Heinz Buth. Automated code generator verification based on algebraic laws. Technical Report Keil KHB 5/1, Christian-Albrechts-University Kiel, Germany, 1995.
[27] Lukai Cai, Shireesh Verma, and Daniel D. Gajski. Comparison of specc and systemc languages for system design. Technical Report TR-03-11, Center for Embedded Computer Systems, University of California, Irvine, 2003.
[28] Celoxica Company. Handel-C Language Reference Manual, 2003.
[29] K. Cheng, J.Cong, Y. Ding, A. Kahng, and P. Trajmar. Dog-map:graph-based fpga technology mapping for delay optimization. IEEE Design and Test of Computers), Sept 1992.
[30] J. Cong and Y. Ding. Beyond the combinatorial limit in depth minimization for LUT-based FPGA designs. In Proc. IEEE/ACM International Conference on CAD, 1993.
[31] John Cooley. Vhdl, the new latin. EE Design, April 2003.
[32] Clifford E. Cummings. Systemverilog - is this the merging of verilig & vhdl. In Proceesings of Synapsys User Group, 2003.
[33] CynApps Inc., Santa Clara USA. Cynlib: A C++ library for Hardware Description Reference Manual, 1999.
[34] J. da Silva. Correctness Proofs of Compilers and Debuggers: An approach based on Structural Operational Semantics. PhD thesis, PhD thesis, Department of Computer Science, University of Edinburgh, 1992. ECS-LFCS-92-241 or CST-95-92.
[35] D.Domer, D.D. Gajski, A.Gerstlauer, S.Zhao, and J. Zhu. SpecC: Specification Language and Methodology. Kluwer Academic Publishers, 2000.
[36] J. Despeyroux. Proof of translation in natural semantics. Symposium on Logic in Computer Science, pages 193-205, 1986.
[37] J. Bowen et al. A procos ii project final report: Esprit basic reearch project. Technical report, Oxford University Computing Laboratory, 1996.
[38] J. Eyre and J. Bier. Carmel enables customizable dsp. Microprocessor Report, 12(17), December 1998.
[39] P. L. Flake and Simon J. Davidmann. Superlog, a unified design language for system-on-chip. In Proceedings of the Asia and South Pacific Design Automation Conference, 2000.
[40] I. Panagopoulos G. Economakos, P. Oikonomakos. Behavioral synthesis with systemc.
[41] Paul Gastin and Michael W. Mislove. A truly concurrent semantics for a process algebra using resource pomsets. Theoretic Computer Science, 281(1-2): 369-421, 2002.
[42] Paul Gastin and Dan Teodosiu. Resource traces: a domain for processes sharing exclusive resources. Theoretic Comnputer Science, 278: 195-221, 2002.
[43] R. Gerber and I.Lee. A calculus for communicating shared resources. Concur'90 LNCS 458, Springer Verlag, 1990.
[44] R. Gerber and I.Lee. Specification and analysis of resource-bound real-time systems. Theory in Practice, LNCS 600. Springer Verlag, 1992.
[45] J.A. Goguen. Introducing obj. Technical Report SRI-CSL-92-03, Computer Science Lsboratory, SRI International, California, USA, 1992.
[46] A. Goswami and M. Joseph. A semantics for the specification of real-time processes. Technical Report 121, Department of Computer Science, University of Warwick, 1988.
[47] A. Goswami and M. Joseph. Semantics of real-time distributed programs. In Concurrency'88, 1988.
[48] Thorsten Groteker, Stan Liao, Grant Martin, and Stuart Swan. System Design with System C. Kluwer Academeic Publisher, 2001.
[49] Accellera C/C++ Working Group. Rtl semanics, draft specification. 2001.
[50] C.A. Gunter and J.C. Mitchell. Semantics of Programming Languages. MIT Press, 1992.
[51] Wolfgang Gunther and Rolf Drechsler. Action.combing logic synthesis and technology mapping for mux based fpgas. IEEE EUROMICRO Conference, 2000.
[52] Ali Habibi and Sofiene Tahar. A survey on system-on-a-chip design language. The 3rd IEEE International Workshop on System-on-Chip for Real-Time Application, 2003.
[53] Flemming Nielson Hanne Riis Nielson and. Semantics with Applications and Formal Introduction. John Wiely & Sons, 1992.
[54] Faisal Haque, Jonathan Michelson, and Khizar Khan. The Art of Verification with Vera. Verification Central, 2001.
[55] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
[56] C.A.R. Hoare, I. J. Hayes, He Jifeng, C.C. Morgan, A. W. Roscoe, J.W. Sanders, I.H.Sorensen, J.M. Spivey, and B.A.Sufrin. Laws of programming. Communications of the ACM, 8:672-686, 1987.
[57] C.A.R Hoare and Jifeng He. Unifying Theories of Programming. Series in Computer Science. Prentice-Hall Europe, 1st edition, 1998.
[58] C.A.R. Hoare, Jifeng He, and A. Sampio. Normal form approach to compiler design. Acta Informatica, 30:701-739, 1993.
[59] B. Hutchings and B. Nelson. Using general-purpose programming language for fpga design. Proceedings of Design Automation Conference, 2000.
[60] IEEE. P1076 Standard VHDL Language Reference Manual.
[61] IEEE. IEEE Std. 1364-2001 IEEE Standard for Verilog Hardware Description Language, 2001.
[62] He Jifeng, Ian Page, and Jonathan Bowen. Towards a provably correct hardware implementation of occam. Lecture Notes of Computer Science 683, pages 214-226, 1993.
[63] J.MaCarthy and J.Painter. Correctness of a compiler for arithmetic expressions. In Proceedings of Symposium on Aplied Mathematics, pages 33-41, 1967.
[64] Atsushi Kasuya, Ennis Hawk, and Tesh Tesfaye. Jeda tutorial. 2003.
[65] Bart Kienhuis, Ed F. Deprettere, Pieter van der Wolf, and Kees A. Vissers. A methodology to design programmable embedded systems - the y-chart approach. In Embedded Processor Design Challenges: Systems, Architectures, Modeling, and Simulation - SAMOS, pages 18-37, London, UK, 2002. Springer-Verlag.
[66] D. C. Ku and G. De Michili. High-level synthesis and optimization strangles in hercules/hebe. In Proceedings of the European Event in ASIC Design Conference, 1990.
[67] Paul Lieverse, Todor Stefanov, Pieter van der Wolf, and Ed Deprettere. System level design with spade: an m-jpeg case study. In ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, pages 31-38, Piscataway, NJ, USA, 2001. IEEE Press.
[68] Gavin Lowe. Scheduling-oriented models for real-time systems. The Computer Journal, 38(6), 1995.
[69] M. Meixner, J. Becker, Th. Hollstein, and M. Glesner. Object oriented specification approach for synthesis of hardware-/software systems. In Proc. GI/ITG/GMM Workshop Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 1999.
[70] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
[71] C. Morgan. Programming from Specifications. Series in Computer Science. Prentice-Hall International, 2nd edition, 1994.
[72] F. Morris. Advice on structuring compilers and proving them correct. SIGACT/SIGPLAN Symposium on Principles of Programming Languages, pages 144-152, 1973.
[73] Wolfgang Mueller. The simulation semantics of systemc. In Proceedings of Design, Automation and Test in Europe Conference(DATE), 2001.
[74] Wolfgang Mueller, Rainer Domer, and Andreas Gerstlauer. The formal execution semantics of specc. Technical Report ICS-TR-01-59, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[75] Markus Muller-Olm. Structuring code generator correctness proofs by stepwise abstracting the machine language's semantics. Technical Report Kiel MMO 12/3, Christian-Albrechts- University Kiel, Germany, 1995.
[76] Hanne Riis Nielson and Flemming Nielson. Semantics With Applications, A Formal Introduc tion. John Wiely and Sons, 1999.
[77] Ralf Niemann. Hardware/Software Co-Design for Data Flow Dominated Embedded Systems. Kluwer Academic Publisher, 1998.
[78] P. W. O'Hearn. Resources, concurrency, and local reasoning. In Proceeding of CONCUR'04, 2004.
[79] S. Owicki and D.Gries. Verifying properties of parallel programs: An axiomatic approach. Comm.ACM., 19(5):279-285, 1976.
[80] G. D. Plotkin. A structural approach to operational semantics. Daimi-fn-19, Aarhus University, 1981.
[81] W. Polak. Compiler specification and verification. Springer-Verlag LNCS 124, 1981.
[82] Andreas Poize, Peter Troger, and Martin von Lowis. The grid occam project. Technical report,Hasso-Plattner-Institute for Software Engineering, University Potsdam, 2004.
[83] J.C. Reynolds. Separation logic: a logic for shared mutable data structure. In Invited Papaer, Proceeding of 17th IEEE Conference on Logic in Computer Science, pages 55-74, 2002.
[84] A.W. Roscoe. The Theory and Pratice of Concurrency. Prentice Hall, 1998.
[85] John Rushby. A tutorial on specification and verification using pvs. Proceedings of the First International Symposium of Formal Methods Europe, 1993.
[86] Augusto Sampaio. An Algebraic Approach to Compiler Design, volume Vol 4. of AMAST Series in Computing. World Scientific Publishing Co., 1997.
[87] Nick Savoiu, Sandeep K. Shukla, and Rajesh K. Gupta. Efficient simulation of synthesisoriented system level designs. In Proceedings of the 15th international symposium on System Synthesis, 2001.
[88] Nick Savoiu, Sandeep K. Shukla, and Rajesh K. Gupta. Concurrency in system level design: Conflict between simulation and synthesis goals. In Proceedings of International Workshop on Logic Synthesis, 2002.
[89] SGS-THOMSON Microelectronics Limited. occam 2.1 REFERENCE MANUAL, 1995.
[90] E. Shade and K.T. Narayana. Real-time semantics for concurrency with shared variables. Technical Report CS-88-28, The Pennsylvania State University, 1988.
[91] E. Shade and K.T. Narayana. Concepts and models for real-time concurrency. 1991.
[92] Dongwan Shin and Daniel D. Gajski. Scheduling in rtl design methodology. Technical Report CECS-02-11, Center for Embedded Computer Systems, University of California, Irvine, 2002.
[93] Sterling and Leon. The Art of Prolog. The MIT Press, Cambridge, Mass, 2nd edition, 1994.
[94] SuperLog. http://www.superlog.org.
[95] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5: 285-309, 1955.
[96] Navin Vemuri, Priyank Kalla, and Russell Tessier. Bdd-based logic synthesis for lut-based fpgas. ACM Transactions on Design Autornatwn of Electronic Systems (TODAES), 7(4): 501-525, 2002.
[97] Jan Wielemaker. SWI-Prolog 5.0 Reference Manual.
[98] Qiang Xie and Daniel D. Gajski. Function binding in rtl design methodology. Technical Report ICS-01-36, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[99] Xilinx Company. Virtex Data Sheets, 2001.
[100] Xilinx Company. Xilinx Development System, Libraries Guide, 2002.
[101] C. Yang and M. Ciesielski. Bds: Bdd-based logic optimization system. IEEE Transactions on CAD, 21, July 2002.
[102] Haobo Yu and Daniel D. Gajski. Interconnection binding in rtl design methodology. Technical Report ICS-01-38, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[103] Pei Zhang and Daniel D. Gajski. Storage binding in rtl synthesis. Technical Report ICS-01-37, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[104] Vladimir D. Zivkovic and Paul Lieverse. An overview of methodologies and tools in the field of system-level design, pages 74-88, 2002.
[2] Accellera. System Verilog Language Reference Manual,
[3] Accellera. Property Specification Language Reference Manual Version 1.1, June 2004.
[4] Actel Company. Axcelator Family FPGAs Detailed Specification, 2004.
[5] Alfred V. Aho, Ravi Sethi, and jeffery D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, Pearson Education, Inc, 1986.
[6] P. Alexander, R. Kamath, and D. Barton. System specification in rosetta. Proceeding of The IEEE Engineering of Computer Based Systems Symposium, April 2000.
[7] Altera Corporation. Stratix Device Family Data Sheet, 2004.
[8] ANSI. ANSI/EIA Standard 548-1988, EDIF 200.
[9] David F. Bacon, Susan L. Graham, and Oliver J. Sharp. Compiler transformations for highperformance computing. ACM Computing Survey, 26(4): 345-420, 1994.
[10] Stephen Bailey. VHDL does not need the System moniker. Mentor Graphics Corp.
[11] F. Balarin, P. Giusto, and et al. Hardware-Software Co-Design of Embedded Systems: The POLLS Approach. 1997.
[12] P. Bellows and B. Hutchings. Jhdl - an hdl for reconfigurable systems. In IEEE Symposium on FPGAs for Custom Computing Machines, 1998.
[13] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretic Computer Science, 37(1): 77-121, 1985.
[14] Gerard Berry and Georges Gonthier. The esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2): 87-152, 1992.
[15] Jonathan Bowen. Occam resources:http://archive.comlab.ox.ac.uk/occam.html.
[16] Jonathan Bowen. Animating the semantics of verilog using prolog. Technical Report 176, UNU-IIST, 1999.
[17] Jonathan Bowen and He Jifeng. An approach to the specification and verification of a hardware compilation scheme. The Journal of Supercomputing, 19(1): 23-29, 2001.
[18] Jonathan P. Bowen, Martin Franzle, Ernst-Rü diger Olderog, and Anders P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland, pages 176-187, 22-24 June 1993.
[19] Stephen Brookes. Retracing the semantics of csp. In BCS-FACS: 25 Years of CSP, 2004.
[20] Stephen Brookes. A semantics for concurrent separation logic. In Proceeding of CONCUR'O4, 2004.
[21] F. M. Brown. Boolean Reasoning. Kluwer Academic Publishers, 1990.
[22] Stephen Brown and Jonathan Rose. Architecture of fpga and cpld: A tutorial. Technical report, Department of Electral and Computer Engineering, 1997.
[23] Francesco Bruschi and Fabrizio Ferrandi. Synthesis of complex control structures from behavioral systemc models. In In Proceedings of Design, Automation and Test in Europe Conference (DATE'03 Designers' Forum), 2003.
[24] R.E. Bryant. Graph - based algorithms for boolean function manipulation. IEEE Trans. on Comp, 35(8): 677-691, 1986.
[25] R. Burstall and P. Landin. Programs and their proofs: an algebraic approach. Machine Intelligence, 7: 17-43, 1969.
[26] Karl-Heinz Buth. Automated code generator verification based on algebraic laws. Technical Report Keil KHB 5/1, Christian-Albrechts-University Kiel, Germany, 1995.
[27] Lukai Cai, Shireesh Verma, and Daniel D. Gajski. Comparison of specc and systemc languages for system design. Technical Report TR-03-11, Center for Embedded Computer Systems, University of California, Irvine, 2003.
[28] Celoxica Company. Handel-C Language Reference Manual, 2003.
[29] K. Cheng, J.Cong, Y. Ding, A. Kahng, and P. Trajmar. Dog-map:graph-based fpga technology mapping for delay optimization. IEEE Design and Test of Computers), Sept 1992.
[30] J. Cong and Y. Ding. Beyond the combinatorial limit in depth minimization for LUT-based FPGA designs. In Proc. IEEE/ACM International Conference on CAD, 1993.
[31] John Cooley. Vhdl, the new latin. EE Design, April 2003.
[32] Clifford E. Cummings. Systemverilog - is this the merging of verilig & vhdl. In Proceesings of Synapsys User Group, 2003.
[33] CynApps Inc., Santa Clara USA. Cynlib: A C++ library for Hardware Description Reference Manual, 1999.
[34] J. da Silva. Correctness Proofs of Compilers and Debuggers: An approach based on Structural Operational Semantics. PhD thesis, PhD thesis, Department of Computer Science, University of Edinburgh, 1992. ECS-LFCS-92-241 or CST-95-92.
[35] D.Domer, D.D. Gajski, A.Gerstlauer, S.Zhao, and J. Zhu. SpecC: Specification Language and Methodology. Kluwer Academic Publishers, 2000.
[36] J. Despeyroux. Proof of translation in natural semantics. Symposium on Logic in Computer Science, pages 193-205, 1986.
[37] J. Bowen et al. A procos ii project final report: Esprit basic reearch project. Technical report, Oxford University Computing Laboratory, 1996.
[38] J. Eyre and J. Bier. Carmel enables customizable dsp. Microprocessor Report, 12(17), December 1998.
[39] P. L. Flake and Simon J. Davidmann. Superlog, a unified design language for system-on-chip. In Proceedings of the Asia and South Pacific Design Automation Conference, 2000.
[40] I. Panagopoulos G. Economakos, P. Oikonomakos. Behavioral synthesis with systemc.
[41] Paul Gastin and Michael W. Mislove. A truly concurrent semantics for a process algebra using resource pomsets. Theoretic Computer Science, 281(1-2): 369-421, 2002.
[42] Paul Gastin and Dan Teodosiu. Resource traces: a domain for processes sharing exclusive resources. Theoretic Comnputer Science, 278: 195-221, 2002.
[43] R. Gerber and I.Lee. A calculus for communicating shared resources. Concur'90 LNCS 458, Springer Verlag, 1990.
[44] R. Gerber and I.Lee. Specification and analysis of resource-bound real-time systems. Theory in Practice, LNCS 600. Springer Verlag, 1992.
[45] J.A. Goguen. Introducing obj. Technical Report SRI-CSL-92-03, Computer Science Lsboratory, SRI International, California, USA, 1992.
[46] A. Goswami and M. Joseph. A semantics for the specification of real-time processes. Technical Report 121, Department of Computer Science, University of Warwick, 1988.
[47] A. Goswami and M. Joseph. Semantics of real-time distributed programs. In Concurrency'88, 1988.
[48] Thorsten Groteker, Stan Liao, Grant Martin, and Stuart Swan. System Design with System C. Kluwer Academeic Publisher, 2001.
[49] Accellera C/C++ Working Group. Rtl semanics, draft specification. 2001.
[50] C.A. Gunter and J.C. Mitchell. Semantics of Programming Languages. MIT Press, 1992.
[51] Wolfgang Gunther and Rolf Drechsler. Action.combing logic synthesis and technology mapping for mux based fpgas. IEEE EUROMICRO Conference, 2000.
[52] Ali Habibi and Sofiene Tahar. A survey on system-on-a-chip design language. The 3rd IEEE International Workshop on System-on-Chip for Real-Time Application, 2003.
[53] Flemming Nielson Hanne Riis Nielson and. Semantics with Applications and Formal Introduction. John Wiely & Sons, 1992.
[54] Faisal Haque, Jonathan Michelson, and Khizar Khan. The Art of Verification with Vera. Verification Central, 2001.
[55] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
[56] C.A.R. Hoare, I. J. Hayes, He Jifeng, C.C. Morgan, A. W. Roscoe, J.W. Sanders, I.H.Sorensen, J.M. Spivey, and B.A.Sufrin. Laws of programming. Communications of the ACM, 8:672-686, 1987.
[57] C.A.R Hoare and Jifeng He. Unifying Theories of Programming. Series in Computer Science. Prentice-Hall Europe, 1st edition, 1998.
[58] C.A.R. Hoare, Jifeng He, and A. Sampio. Normal form approach to compiler design. Acta Informatica, 30:701-739, 1993.
[59] B. Hutchings and B. Nelson. Using general-purpose programming language for fpga design. Proceedings of Design Automation Conference, 2000.
[60] IEEE. P1076 Standard VHDL Language Reference Manual.
[61] IEEE. IEEE Std. 1364-2001 IEEE Standard for Verilog Hardware Description Language, 2001.
[62] He Jifeng, Ian Page, and Jonathan Bowen. Towards a provably correct hardware implementation of occam. Lecture Notes of Computer Science 683, pages 214-226, 1993.
[63] J.MaCarthy and J.Painter. Correctness of a compiler for arithmetic expressions. In Proceedings of Symposium on Aplied Mathematics, pages 33-41, 1967.
[64] Atsushi Kasuya, Ennis Hawk, and Tesh Tesfaye. Jeda tutorial. 2003.
[65] Bart Kienhuis, Ed F. Deprettere, Pieter van der Wolf, and Kees A. Vissers. A methodology to design programmable embedded systems - the y-chart approach. In Embedded Processor Design Challenges: Systems, Architectures, Modeling, and Simulation - SAMOS, pages 18-37, London, UK, 2002. Springer-Verlag.
[66] D. C. Ku and G. De Michili. High-level synthesis and optimization strangles in hercules/hebe. In Proceedings of the European Event in ASIC Design Conference, 1990.
[67] Paul Lieverse, Todor Stefanov, Pieter van der Wolf, and Ed Deprettere. System level design with spade: an m-jpeg case study. In ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, pages 31-38, Piscataway, NJ, USA, 2001. IEEE Press.
[68] Gavin Lowe. Scheduling-oriented models for real-time systems. The Computer Journal, 38(6), 1995.
[69] M. Meixner, J. Becker, Th. Hollstein, and M. Glesner. Object oriented specification approach for synthesis of hardware-/software systems. In Proc. GI/ITG/GMM Workshop Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 1999.
[70] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
[71] C. Morgan. Programming from Specifications. Series in Computer Science. Prentice-Hall International, 2nd edition, 1994.
[72] F. Morris. Advice on structuring compilers and proving them correct. SIGACT/SIGPLAN Symposium on Principles of Programming Languages, pages 144-152, 1973.
[73] Wolfgang Mueller. The simulation semantics of systemc. In Proceedings of Design, Automation and Test in Europe Conference(DATE), 2001.
[74] Wolfgang Mueller, Rainer Domer, and Andreas Gerstlauer. The formal execution semantics of specc. Technical Report ICS-TR-01-59, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[75] Markus Muller-Olm. Structuring code generator correctness proofs by stepwise abstracting the machine language's semantics. Technical Report Kiel MMO 12/3, Christian-Albrechts- University Kiel, Germany, 1995.
[76] Hanne Riis Nielson and Flemming Nielson. Semantics With Applications, A Formal Introduc tion. John Wiely and Sons, 1999.
[77] Ralf Niemann. Hardware/Software Co-Design for Data Flow Dominated Embedded Systems. Kluwer Academic Publisher, 1998.
[78] P. W. O'Hearn. Resources, concurrency, and local reasoning. In Proceeding of CONCUR'04, 2004.
[79] S. Owicki and D.Gries. Verifying properties of parallel programs: An axiomatic approach. Comm.ACM., 19(5):279-285, 1976.
[80] G. D. Plotkin. A structural approach to operational semantics. Daimi-fn-19, Aarhus University, 1981.
[81] W. Polak. Compiler specification and verification. Springer-Verlag LNCS 124, 1981.
[82] Andreas Poize, Peter Troger, and Martin von Lowis. The grid occam project. Technical report,Hasso-Plattner-Institute for Software Engineering, University Potsdam, 2004.
[83] J.C. Reynolds. Separation logic: a logic for shared mutable data structure. In Invited Papaer, Proceeding of 17th IEEE Conference on Logic in Computer Science, pages 55-74, 2002.
[84] A.W. Roscoe. The Theory and Pratice of Concurrency. Prentice Hall, 1998.
[85] John Rushby. A tutorial on specification and verification using pvs. Proceedings of the First International Symposium of Formal Methods Europe, 1993.
[86] Augusto Sampaio. An Algebraic Approach to Compiler Design, volume Vol 4. of AMAST Series in Computing. World Scientific Publishing Co., 1997.
[87] Nick Savoiu, Sandeep K. Shukla, and Rajesh K. Gupta. Efficient simulation of synthesisoriented system level designs. In Proceedings of the 15th international symposium on System Synthesis, 2001.
[88] Nick Savoiu, Sandeep K. Shukla, and Rajesh K. Gupta. Concurrency in system level design: Conflict between simulation and synthesis goals. In Proceedings of International Workshop on Logic Synthesis, 2002.
[89] SGS-THOMSON Microelectronics Limited. occam 2.1 REFERENCE MANUAL, 1995.
[90] E. Shade and K.T. Narayana. Real-time semantics for concurrency with shared variables. Technical Report CS-88-28, The Pennsylvania State University, 1988.
[91] E. Shade and K.T. Narayana. Concepts and models for real-time concurrency. 1991.
[92] Dongwan Shin and Daniel D. Gajski. Scheduling in rtl design methodology. Technical Report CECS-02-11, Center for Embedded Computer Systems, University of California, Irvine, 2002.
[93] Sterling and Leon. The Art of Prolog. The MIT Press, Cambridge, Mass, 2nd edition, 1994.
[94] SuperLog. http://www.superlog.org.
[95] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5: 285-309, 1955.
[96] Navin Vemuri, Priyank Kalla, and Russell Tessier. Bdd-based logic synthesis for lut-based fpgas. ACM Transactions on Design Autornatwn of Electronic Systems (TODAES), 7(4): 501-525, 2002.
[97] Jan Wielemaker. SWI-Prolog 5.0 Reference Manual.
[98] Qiang Xie and Daniel D. Gajski. Function binding in rtl design methodology. Technical Report ICS-01-36, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[99] Xilinx Company. Virtex Data Sheets, 2001.
[100] Xilinx Company. Xilinx Development System, Libraries Guide, 2002.
[101] C. Yang and M. Ciesielski. Bds: Bdd-based logic optimization system. IEEE Transactions on CAD, 21, July 2002.
[102] Haobo Yu and Daniel D. Gajski. Interconnection binding in rtl design methodology. Technical Report ICS-01-38, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[103] Pei Zhang and Daniel D. Gajski. Storage binding in rtl synthesis. Technical Report ICS-01-37, Center for Embedded Computer Systems, University of California, Irvine, 2001.
[104] Vladimir D. Zivkovic and Paul Lieverse. An overview of methodologies and tools in the field of system-level design, pages 74-88, 2002.