浮点乘加中混合算术加法可信性增强关键技术的研究
|
摘要
系统可信性是在正确性、可靠性、安全性、可维护性等众多概念的基础上发展起来的一个新概念。一般认为,系统具有高可信性是指系统的动态行为及其结果总是符合人们的预期,系统在受到诸如操作错误、环境变化、外部攻击等干扰时仍能成功地向用户提供连续的服务。
工业界和学术界逐步认识到可信性已经成为信息系统的内在固有属性。然而,可信性不是安全性、可靠性等诸多属性的简单叠加。传统衡量系统质量的各个属性是从不同的视角定义的,它们之间存在相互关联和影响,将它们综合起来作为可信性的解释并不合理。目前,学者们仍不断尝试从各个角度、多种层次去诠释系统可信性,并以此为指导发展系统可信性增强技术。
系统可信性研究范围非常广泛,涉及计算机系统的各个领域。小到简单的硬件模块,大到复杂的分布式网络系统都存在可信性问题。系统可信性研究既要对多个领域的共性问题进行理论探讨,也要针对具体应用领域的特点进行技术创新。本文在研究系统可信性一般性问题的基础上,着重对计算机算术领域混合算术加法中的可信性问题及其相应的可信性增强技术进行了研究和探索,希望对提高微处理器计算部件的设计水平有所帮助。
本文在社会学、心理学等领域提出的信任模型和计算机领域现有的系统可信性模型的基础上,描述了一个通用的信任模型,并以该通用信任模型为基础,提出了一个新的系统可信性模型。本文提出的系统可信性模型总结了可信性的特点和主要研究内容,阐述了提高系统可信性的主要方法和途径。
以提出的系统可信性模型为指导,本文着重研究了浮点乘加部件中混合算术加法的可信性问题,并以IBM POWER6微处理器中128位循环进位混合加法器为应用实例研究了算术加法可信性增强的关键技术,它们包括:硬件部件功能正确性分析和证明,硬件部件非功能属性(如功耗等)的评估与优化以及硬件系统高层次建模与模型转换等。
针对算术加法部件的功能正确性,本文提出了基于半群理论的算术加法形式化分析和证明方法。本文首先基于半群理论和归纳法形式化地描述和证明了行波进位、超前进位、并行前缀等较基本的算术加法算法的正确性。以此为基础,本文提出了一种通用选择进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。然后,融合上述加法算法,本文提出了一种通用循环进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。本文的工作确保了遵从该通用循环进位/并行前缀混合加法系统结构而设计的加法器在算法层次的正确性。IBM POWER6 128位循环进位加法器是该通用系统结构的具体实例,因此其正确性也很容易得到了验证。
针对算术加法部件功耗等非功能属性,本文提出了基于面向方面的硬件设计空间搜索方法,在设计早期就对硬件系统的功能和非功能属性进行分析和评估,提高了搜索满足多个约束条件的优化设计方案的效率。IBM POWER6循环进位加法器作为示例说明了该方法的有效性。
此外,本文提出了基于模型驱动开发和面向服务建模的硬件高层次建模与设计方法。该方法通过提高系统设计描述的抽象层次和模型自动转换来提高系统开发的效率并增强系统设计的可信性。IBM POWER6的循环进位加法器同样作为示例验证了该方法的有效性。最后,本文还讨论了基于UML的高层次面向方面的硬件系统建模方法。
System trustworthiness is novel concept based on properties such as correct-ness, reliability, safety, maintainability and so on. Traditionally, trustworthiness isdefined as the system’s behaviors and its results are always consistent with the user’sexpectations. When there are some interferences from operation errors, environmentchanges and outside attacks, the trustworthy system is required to supply servicessuccessfully and continuously.
Industry and Academic begin to acknowledge that trustworthiness is a intrinsicproperty of the system, which is not a simple union of attributes such as security,reliability and so on. It is well-known that traditional quality attributes are de-fined from various perspectives, which are not orthogonal. It does not make senseto understand trustworthiness as a holistic property of the system, encompassingall of the traditional quality attributes. Right now, researchers are trying to ex-plain the concept of trustworthiness from various perspectives and develop relatedtrustworthiness improving techniques.
Based on the trust models from the sociology, psychology and the existingsystem trustworthiness models from the computer science, this paper presents ageneral trust model and a novel system trustworthiness model. The characteristicsof trustworthiness and its main research contexts are concluded in the proposedsystem trustworthiness model, which also explains the trustworthiness improvementtechnologies.
By the proposed system trustworthiness model, this paper focuses on the keytechniques of trustworthiness improvement on hybird arithmetic addition of ?oating-point fused multiply-add unit, including analysis and proof of the hardware func-tionality correctness, estimation and optimization of the non-functional propertiessuch as power consumption, as well as high-level hardware modeling and modeltransformation. The end-around-carry adder in IBM POWER6 microprocessor istaken as the case study in this paper.
For the correctness of arithmetic addition algorithms, the semi-group basedformal analysis and proof methodology is proposed in this paper. Firstly, the cor- rectness of basic addition algorithms such as ripple carry adder, carry look-aheadadder and parallel prefix adders are proved. Then, a general architecture for the de-sign of hybrid prefix/carry-select adder is proposed. A detailed proof of this generalarchitecture is described. By the above addition algorithms, a general architecturefor the design of hybrid prefix/end-around-carry adder is developed. The details ofits correctness proof are also described. This ensures the algorithm level correctnessof the real design of end-around-carry adder followed the general architecture. Theend-around-carry adder in IBM POWER6 microprocessor is a special case of theproposed hybrid prefix/end-around-carry adder general architecture, which meansits correctness can be verified easily.
For the adder’s non-functional properties ( such as power consumption ), thispaper presents an AOP-based hardware design space exploration methodology, whichdoes the analysis and estimation for the hardware system’s functionality and non-functional properties at the early stage of the design circle. This methodology ishelpful to search the optimized design under a number of constraints. The IBM’send-around-carry adder is taken as a case study to show the e?ectiveness of theproposed methodology.
Furthermore, this paper also presents a MDA-based and service-oriented high-level hardware modeling and design method. By using the high-level modelingtechnology and model transformation, the e?ciency of system development and thesystem’s trustworthiness can be both improved. The IBM’s end-around-carry adderis also taken as a case study to show the e?ectiveness of the proposed methodology.At last, the paper discusses the UML-based method to model the notions of AOPfor hardware design at the high level of abstraction.
工业界和学术界逐步认识到可信性已经成为信息系统的内在固有属性。然而,可信性不是安全性、可靠性等诸多属性的简单叠加。传统衡量系统质量的各个属性是从不同的视角定义的,它们之间存在相互关联和影响,将它们综合起来作为可信性的解释并不合理。目前,学者们仍不断尝试从各个角度、多种层次去诠释系统可信性,并以此为指导发展系统可信性增强技术。
系统可信性研究范围非常广泛,涉及计算机系统的各个领域。小到简单的硬件模块,大到复杂的分布式网络系统都存在可信性问题。系统可信性研究既要对多个领域的共性问题进行理论探讨,也要针对具体应用领域的特点进行技术创新。本文在研究系统可信性一般性问题的基础上,着重对计算机算术领域混合算术加法中的可信性问题及其相应的可信性增强技术进行了研究和探索,希望对提高微处理器计算部件的设计水平有所帮助。
本文在社会学、心理学等领域提出的信任模型和计算机领域现有的系统可信性模型的基础上,描述了一个通用的信任模型,并以该通用信任模型为基础,提出了一个新的系统可信性模型。本文提出的系统可信性模型总结了可信性的特点和主要研究内容,阐述了提高系统可信性的主要方法和途径。
以提出的系统可信性模型为指导,本文着重研究了浮点乘加部件中混合算术加法的可信性问题,并以IBM POWER6微处理器中128位循环进位混合加法器为应用实例研究了算术加法可信性增强的关键技术,它们包括:硬件部件功能正确性分析和证明,硬件部件非功能属性(如功耗等)的评估与优化以及硬件系统高层次建模与模型转换等。
针对算术加法部件的功能正确性,本文提出了基于半群理论的算术加法形式化分析和证明方法。本文首先基于半群理论和归纳法形式化地描述和证明了行波进位、超前进位、并行前缀等较基本的算术加法算法的正确性。以此为基础,本文提出了一种通用选择进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。然后,融合上述加法算法,本文提出了一种通用循环进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。本文的工作确保了遵从该通用循环进位/并行前缀混合加法系统结构而设计的加法器在算法层次的正确性。IBM POWER6 128位循环进位加法器是该通用系统结构的具体实例,因此其正确性也很容易得到了验证。
针对算术加法部件功耗等非功能属性,本文提出了基于面向方面的硬件设计空间搜索方法,在设计早期就对硬件系统的功能和非功能属性进行分析和评估,提高了搜索满足多个约束条件的优化设计方案的效率。IBM POWER6循环进位加法器作为示例说明了该方法的有效性。
此外,本文提出了基于模型驱动开发和面向服务建模的硬件高层次建模与设计方法。该方法通过提高系统设计描述的抽象层次和模型自动转换来提高系统开发的效率并增强系统设计的可信性。IBM POWER6的循环进位加法器同样作为示例验证了该方法的有效性。最后,本文还讨论了基于UML的高层次面向方面的硬件系统建模方法。
System trustworthiness is novel concept based on properties such as correct-ness, reliability, safety, maintainability and so on. Traditionally, trustworthiness isdefined as the system’s behaviors and its results are always consistent with the user’sexpectations. When there are some interferences from operation errors, environmentchanges and outside attacks, the trustworthy system is required to supply servicessuccessfully and continuously.
Industry and Academic begin to acknowledge that trustworthiness is a intrinsicproperty of the system, which is not a simple union of attributes such as security,reliability and so on. It is well-known that traditional quality attributes are de-fined from various perspectives, which are not orthogonal. It does not make senseto understand trustworthiness as a holistic property of the system, encompassingall of the traditional quality attributes. Right now, researchers are trying to ex-plain the concept of trustworthiness from various perspectives and develop relatedtrustworthiness improving techniques.
Based on the trust models from the sociology, psychology and the existingsystem trustworthiness models from the computer science, this paper presents ageneral trust model and a novel system trustworthiness model. The characteristicsof trustworthiness and its main research contexts are concluded in the proposedsystem trustworthiness model, which also explains the trustworthiness improvementtechnologies.
By the proposed system trustworthiness model, this paper focuses on the keytechniques of trustworthiness improvement on hybird arithmetic addition of ?oating-point fused multiply-add unit, including analysis and proof of the hardware func-tionality correctness, estimation and optimization of the non-functional propertiessuch as power consumption, as well as high-level hardware modeling and modeltransformation. The end-around-carry adder in IBM POWER6 microprocessor istaken as the case study in this paper.
For the correctness of arithmetic addition algorithms, the semi-group basedformal analysis and proof methodology is proposed in this paper. Firstly, the cor- rectness of basic addition algorithms such as ripple carry adder, carry look-aheadadder and parallel prefix adders are proved. Then, a general architecture for the de-sign of hybrid prefix/carry-select adder is proposed. A detailed proof of this generalarchitecture is described. By the above addition algorithms, a general architecturefor the design of hybrid prefix/end-around-carry adder is developed. The details ofits correctness proof are also described. This ensures the algorithm level correctnessof the real design of end-around-carry adder followed the general architecture. Theend-around-carry adder in IBM POWER6 microprocessor is a special case of theproposed hybrid prefix/end-around-carry adder general architecture, which meansits correctness can be verified easily.
For the adder’s non-functional properties ( such as power consumption ), thispaper presents an AOP-based hardware design space exploration methodology, whichdoes the analysis and estimation for the hardware system’s functionality and non-functional properties at the early stage of the design circle. This methodology ishelpful to search the optimized design under a number of constraints. The IBM’send-around-carry adder is taken as a case study to show the e?ectiveness of theproposed methodology.
Furthermore, this paper also presents a MDA-based and service-oriented high-level hardware modeling and design method. By using the high-level modelingtechnology and model transformation, the e?ciency of system development and thesystem’s trustworthiness can be both improved. The IBM’s end-around-carry adderis also taken as a case study to show the e?ectiveness of the proposed methodology.At last, the paper discusses the UML-based method to model the notions of AOPfor hardware design at the high level of abstraction.
引文
[1]刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述.中国科学基金. 2008, 22(03):145–151
[2]孙海平.计算机算术中若干前缀计算问题的研究. Ph.D. thesis,合肥工业大学,2006
[3] M. J. Flynn, S. F. Oberman. Advanced Computer Arithmetic Design. Wiley-Interscience, 2001
[4] Y. Shimazu, T. Kengaku, T. Fujiyama, E. Teraoka, et al. A 50MHz 24b Floating-Point DSP. In Proc of the IEEE International Solid-State Circuit Conference.1989:44–45
[5] S. F. Oberman. Design issues in high performance ?oating point arithmetic units.PhD thesis, Stanford University. 1996
[6] ANSI/IEEE Std, 754-2008. Binary Floating-Point Arithmetic. Tech. rep., IEEE-SAStandards Board, 2008
[7] I. Koren. Computer Arithmetic Algorithms. A. K. Peters, Natick, MA, 2002
[8] General Processor Information. Berkeley CPU information center at. Tech. rep.,http://bwrc.eecs.berkeley.edu/CIC/summary/local/summary.pdf, 2001
[9] A. Nannarelli. Low Power Division and Square Root. PhD thesis, University ofCalifornia. 1999
[10] M. Paragelis, D. Plexousakis, and T. Kutsuras. Alleviating the Sparsity Problemof Collaborative Filtering Using Trust Inferences. Trust Management, ProceedingsLecture Notes in Computer Science. 2005, 3477:224–239
[11] G. Pitsilis, L. Marshall. Trust as a Key to Improving Recommendation Sys-tems. Trust Management, Proceedings Lecture Notes in Computer Science. 2005,3477:210–223
[12] P. Giorgini, F. Massacci, J. Mylopoulos, N. Zannone. Modeling Social and IndividualTrust in Requirements Engineering Methodologies. Trust Management, ProceedingsLecture Notes in Computer Science. 2005, 3477:161–176
[13] B. Wong, C. Bibeau, K. A. Bishop, G. G. Rosenthal. Response to Perceived Preda-tion Threat in Fiddler Crabs: Trust Thy Neighbor as Thyself? Behavioral Ecologyand Sociobiology. 2005, 58(4):345–350
[14] A. Josang, C. Keser, T. Dimtrakos. Can We Manage Trust? Trust Management,Proceedings Lecture Notes in Computer Science. 2005, 3477:93–107
[15] J. M. Seigneur, A. Gray, C. D. Jensen. Trust Transfer: Encouraging Self-recommendations without Sybil Attack. Trust Management, Proceedings LectureNotes in Computer Science. 2005, 3477:321–337
[16] N. Dimmock, J. Bacon, D. Ingram, K. Moody. Risk Models for Trust-based Ac-cess Control (TBAC). Trust Management, Proceedings Lecture Notes in ComputerScience. 2005, 3477:364–371
[17] S. Pearson, M. C. Mont, S. Crane. Persistent and Dynamic Trust: Analysis andthe Related Impact of Trusted Platforms. Trust Management, Proceedings LectureNotes in Computer Science. 2005, 3477:355–363
[18]孙道奇.基于信任和服务模型的普适计算安全问题研究. Ph.D. thesis,东华大学, 2008
[19] Jsang and R. Ismail. The beta reputation system. In Proceedings of 15th BledElectronic Commerce Conference. 2002
[20] Y. Wang, J. Vassileva. Trust and Reputation Model in Peer-to-Peer Networks. ThirdInternational Conference on Peer-to-Peer Computing (P2P103), IEEE. 2003
[21] V. Cahill, B. Shand, E. Gray, et al. Using Trust for Secure Collaboration in Uncer-tain Environments. Pervasive Computing. 2003, 2(3):52–61
[22] A. A. Rahman, S. Hailes. Supporting Trust in Virtual Communities. Hawaii Inter-national Conference on System Sciences. 2000
[23] J. Sabater, C. Sierra. Reputation and Social Network Analysis in Muti-Agent Sys-tems. First International Joint Conference on Autonomous Agents and Muti-AgentSystems. 2001
[24] S. Song, K. Hwang, R. EZhou. Trusted P2P Transactions with Fuzzy ReputationAggregation. IEEE Internet Computing. 2005, 18(28)
[25] S. Karnvar, M. Schlosser. The EigenTrust Algorithm for Reputation Managemtn inP2P Networks. WWW. 2003
[26] W. Don, H. M. Wang, Y. Jia, P. Zou. A Recommendation-based Peer-to-Peer TrustModel. Journal of Software. 2004, 15(4):571–583
[27] D. Yamamoto, T. Asahara, Itao, et al. Distributed Pagerank: A Distributed Repu-tation Model for Open P2P Networks. Proceedings of the 2004 International Sym-posium on Applications and the Internet Workshops. 2004
[28] B. Yu, M. P. Singh, K. Sycara. Developing Trust in Largescale Peer-to-Peer Systems.Proceedings of the 1st IEEE Symposium on Multi-Agent Security and Suwiability.2004
[29] A. Josang. Trust-Based Decision Making for Electronic. Proceedings of the 4thNordic Workshop on Secure Computer Systems. 1999
[30] G. H. Nibaldi. Specification of a Trusted Computing Base. Technical Report, M79-228 The MITRE Corporation, Bedford, MA, USA. 1979
[31] Department of Defense Computer Security Center. Department of Defense TrustedComputer System Evaluation Criteria. Tech. rep., DoD, USA, 1985
[32] TCPA. TPM protection profile v.1.9.7. Tech. rep., TCPA,http//www.trustedcomputing.org/home, 2006-04-21
[33] TCPA. Main specification v 1.1b. Tech. rep., TCPA,http//www.trustedcomputing.org/home, 2006-04-25
[34] TCG. Trusted computing group(TCG) main specification version 1.1a. Tech. rep.,http://www.trustedcomputinggroup/downloads/tcg spec 1 1b.zip, 2006-04-30
[35] TCG. TCG PC specific, implementation specification version 1.1. Tech. rep.,http://www.trustedcomputinggroup/downloads/TCG PCSpecificSpecification v1 1.pdf,2006-04-26
[36] S. Pearson. Trusted Computing Platforms, the Next Security Solutoin. Tech. rep.,Technical report, Trusted E-Services Laboratory, HP Laboratories Bristol HPL-2002-221, 2002
[37] The Open Trusted Computing (OpenTC) consortium. General activities ofOpenTC. Tech. rep., http://www.opentc.net/activities/, 2006
[38]张焕国,罗捷,金刚,朱智强,余发江,严飞.可信计算研究进展.武汉大学学报(理学版). 2001, 52(5):513–518
[39] A. Avizienis, J. C. Laprie, B. Randell, C. Landwehr. Basic concepts and taxonomyof dependable and secure computing. IEEE Transactions on Dependable and SecureComputing. 2004, 1(1):11–33
[40] I. Sommerville. Software Engineering. AddisonWesley, 7th edition, 2004
[41] D. Patterson, A. Brown, P. Broadwell, et al. Recovery-Oriented Computing (ROC):Motivation, Definition, Techniques, and Case Studies. Tech. rep., Technical ReportTechnical Report UCB//CSD-02-1175, UC Berkeley Computer Science, 2002
[42] D. Oppenheimer, A. Ganapathi, D. Patterson. Why Do Internet Services Fail,and What Can Be Done About it. Proceedings of Usenix Symposium on InternetTechnologies and Systems. 2003:1–16
[43] L. J. Ho?man, K. L. Jenkins, J. Blum. Trust beyond security: an expanded trustmodel. Communications of the ACM. 2006, 49(7):94–101
[44] S. Becker, M. Boskovic, A. Dhama, et al. Trustworthy Software Systems: A Dis-cussion of Basic Concepts and Terminology. ACM SIGSOFT Software EngineeringNotes. 2006, 31(6):1–18
[45] The Second National Software Summit. Software 2015: A National Software Strat-egy to ensure U. S. Security and Competitiveness. Tech. rep., U. S. Center forNational Software Studies, 2005
[46] P. M. Kogge and H. S. Stone. A Parallel Algorithm for The E?cient Solution of AGeneral Class of Recurrence Equations. IEEE Transactions on Computers. 1973,22(8):786–793
[47] R. P. Brent, H. T. Kung. A Regular Layout for Parallel Adders. IEEE Transactionson Computers. 1982, C(31):260–264
[48] R. Ladner, M. Fischer. Parallel Prefix Computation. JACM. 1980, 27(4):831–838
[49] I. Koren. Computer Arithmetic Algorithms. A. K. Peters, Natick, MA, 2002
[50] J. Sklansky. Conditional-sum addition logic. IRE Trans. 1960, EC-9:226–231
[51] P. K. Chan, M. D. F. Schlag, C. D. Thomborson, and V. G. Oklobdzija. Delayoptimization of carry-skip adders and block carry-look-ahead adders using multidi-mendional dynamic programming. IEEE Trans on Computers. 1992, 41:920–930
[52] V. Kantabutra. Designing optimum carry-skip adders. Proc 8th Symp on ComputerArithmeitic. 1991:146–153
[53] C. S. Wallace. A suggestion for a fast multiplier. IEEE Trans on Computers. 1964,EC-13:14–17
[54] H. Ling. High speed binary adder. IBM J Res and Devel. 1981, 25:156–166
[55] M. J. Flynn, S. F. Oberman. Advanced computer arithmetic design. Wiley, NewYork, 2001
[56] P. K. Chan, M. D. F. Schlag. Analysis and design of CMOS Manchester adders withvariable carry-skip. IEEE Trans on Computers. 1990, 39:983–992
[57] T. Lyncn, E. E. Swartzlander, Jr. A spanning tree carry look-ahead adder. IEEETrans on Computers. 1992, 41:931–939
[58] D. W. Dobberpuhl, et al. A 200-MHz 64-b dual-issue CMOS microprocessor. IEEEJ of Solid-State Circuits. 1992, 27:1555–1565
[59] R. K. Montoye, E. Hokenek, S. L. Runyon. Design of the IBM RISC System/6000?oating-point execution unit. IBM Journal of Research and Development. 1990,34(1):59–70
[60] IBM. Enterprise Systems Architecture/390 Principles of Operation. Tech. rep.,Order No. SA227201-5, available through IBM branch o?ces, 1998
[61] S. Waser, M. J. Flynn. Introduction to Arithmetic for Digital Systems Designers.Holt, Rinehart, & Winston, 1982
[62] ANSI/IEEE Std, 754-1985. IEEE standard for binary ?oating-point arithmetic.Tech. rep., Institute of Electrical and Electronic Engineers, Inc. New York, 1985
[63] F. P. O’Connell, S. W. White. POWER3: The Next Generation of PowerPC Pro-cessors. IBM Journal of Research and Development. 2000, 44:873–884
[64] R. Jessani, C. Olson. The Floating-Point Unit of the PowerPC 603e. IBM Journalof Research and Development. 1996, 40:559–566
[65] R. M. Jessani, M. Putrino. Comparision of Single- and Dual-Pass Multiply-AddFused Floating-Point Units. IEEE Trans on Computers. 1998, 47:927–937
[66] A. Kumar. The HP PA-8000 RISC CPU. IEEE Micro Magazine. 1997, 17(2):27–32
[67] D. Hunt. Advanced Performance Features of the 64-bit PA-8000. Proceedings ofCompcon. 1995:123–128
[68] K. C. Yeager. The MIPS R10000 superscalar microprocessor. IEEE Micro Magazine.1996, 16(2):28–40
[69] C. Hinds. An Enhanced Floating Point Coprocessor for Embedded Signal Process-ing and Graphics Applications. Conference Record of the Thirty-Third AsilomarConference on Signals, Systems, and Computers. 1999:147–151
[70] B. Greer, J. Harrision, G. Henry, W. Li, P. Tang. Scientific Computing on theItanium Processor. Proceedings of the ACM/IEEE SC2001 Conference. 2001:1–8
[71] H. Sharangpani, K. Arora. Itanium Processor Microarchitecture. IEEE Micro Ma-ganize. 2000, 20(5):24–43
[72] E. C. Quinnell. Floating-Point Fused Multiply-Add Architectures. Ph.D. thesis, theUniversity of Texas at Austin, 2007
[73] Chen C, Chen L-A, et al. Architecture design of a fast ?oating-point multiplicaiton-add fused unit using signed-digit addition. IEE Proceedings- Computers and DigitalTechniques. 2002, 149(4):113–120
[74] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.Proceedings of 2002 IEEE International Conference on Computer Design: VLSI inComputers and Processors. 2002:145–150
[75] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.Tech. rep., Technical report, Department of Electrical and Computer Engineering,University of Santiago de Compostela, 2002
[76] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.IEEE Trans on Computers. 2004, 53(8):988–1003
[77] M. R. Santoro, G. Bewick, et al. Rounding algorithms for IEEE multiplier. Pro-ceedings of Ninth IEEE Symposium on Computer Arithmetic. 1989:176–183
[78] S. F. Oberman, H. Al-Twaijry, M. J. Flynn. The SNAP Project: Design of Float-ing Point Arithmetic Units. Proceedings of 13th IEEE Symposium on ComputerArithmetic. 1997:156–165
[79] http://www-03.ibm.com/press/us/en/pressrelease/21580.wss
[80] B.Curran, B.McCredie, L.Siqal, et al. 4GHz+ Low-Latency Fixed-Point and BinaryFloating-Point Execution Units for the POWER 6 Processor. Digest of 2006 IEEEInternational Solid-State Circuits Conference. 2006:1728–1734
[81] X. Y. Yu, B. Fleischer, Y. H. Chan, et al. A 5GHz+ 128-bit Binary Floating-PointAdder for the POWER 6 Processor. Proceedings of the 32nd European Solid-StateCircuits Conference. 2006:166–169
[82] V. G. Dklobdzija, D. Villeger. Improving Multiplier Design By Using ImprovedColumn Compression Tree And Optimized Final Adders In CMOS Technology.IEEE Transactions on VLSI Systems. 1995, 3(2)
[83] V. G. Oklobdzija, D. Villeger. Multiplier Design Utilizing Improved Column Com-pression Tree And Optimized Final Adder In CMOS Technology. Proceedings ofthe 1993 International Symposium on VLSI Technology, Systems and Applications.1993:209–212
[84] V. G. Oklobdija, P. Stelling. Design Strategies for the Final Adder in a ParallelMultiplier. Twenty-Ninth Annual Asilomar Conference on signal, Systems, andComputers, Pacific Grove, California. 1995
[85] P. Stelling, V. G. Oklobdzija. Design Strategies for Optimal Hybrid Final Addersin a Parallel Multiplier. special issue on VLSI Arithmetic, Journal of VLSI SignalProcessing, Kluwer Academic Publishers. 1996, 14(3)
[86] B. R. Zeydel, V. G. Oklobdzija, S. Mathew, R. K. Krishnamurthy, S. Borkar. A 90nm1GHz 22mW 16×16 2’s Complement Multiplier for Wireless Baseband. Proceedingsof the 2003 Symposium on VLSI Circuits. 2003
[87] E. Clarke, O. Grumberg, D. Long. Verification tools for finite-state concurrentsystems. A Decade of Concurrency-Re?ections and Perspectives Lecture Notes inComputer Science. 1994, (803)
[88] E. M. Clarke, E. A. Emersion, A. P. Sistla. Automatic verfication of finite-stateconcurrent systems using temporal logic specificaitons. ACM Transactions on Pro-gramming Languages and Systems. 1986, 8(2):244–263
[89] D. A. Du?y. Principles of automated theorem proving. John Wiley & Sons, Inc.New York, NY, USA, 1991
[90] J.O’Donnell, G.Rnger. Derivation of a carry lookahead addition circuit. Journal ofFunctional Programming. 2004, 14(6):127–158
[91] D.Kapur, M.Subramaniam. Mechanical verification of adder circuits using rewriterulelaboratory. Formal Methods in System Design. 1998, 13(2):127–158
[92] M.Sheeran. Hardware design and functional programming: a perfect match. Journalof Universal Computer Science. 2005, 11(7):1135–1158
[93] L. Benini, G. de Micheli. System-level power optimization: techniques and tools .ACM Trans on Design Automation of Electronic Systems. 2000, 5(2):115–192
[94] R. Kumar, Zhiyu Liu, V. Kursun. Fundamental concepts of power and energymeasurement with the computer-aided-design tools. 50th Midwest Symposium onCircuits and Systems. 2007:863–866
[95] S. Ghissoni, J. B. dos Santos Martins, L. L. de Oliveira. A New Methodology inPower Estimation in CMOS Combinational Circuits at Logic Level. 48th MidwestSymposium on Circuits and Systems. 2005, 2:1251–1254
[96] L. Zhong, S. Ravi, A. Raghunathan, N. K. Jha. RTL-Aware Cycle-Accurate Func-tional Power Estimation. IEEE Trans on Computer-Aid Design of Integrated Cir-cuits and Systems. 2006, 25(10):2103–2117
[97] R. Chaudhry, D. Stasiak, S. Posluszny, S. Dhong. A Cycle Accurate Power Estima-tion Tool. Asia and South Pacific Conference on Design Automation. 2006:24–27
[98] G. Dimitrakopoulos, P. Kolovos, P. Kalogerakis, D. Nikolos. Design of High-SpeedLow-Power Parallel-Prefix VLSI Adders. Lecture Notes in Computer Science: Inte-grated Circuit and System Design. 2004:248–257
[99] A. Aslund. Power Estimation of High Speed Bit-Parallel Adders. Tech. rep., Linkop-ing University, LiTH-ISY-EX-3534-2004, 2004
[100] M. Aguirre, M. Linares. A altenative logic approach to implement high-speed low-power full adders cells. Proceedings of the 18th annual symposium on Integratedcircuits and system design. 2005:166–171
[101] S. Lakshmivarahan, S. K. Dhall. Parallel Computing Using The Prefix Problem.Oxford University Press, 1994
[102] A. Pinto, A. Bonivento, S.anni-vincentelli. System Level Design Paradigms:Platform-based Design and Communication Synthesis. ACM Trans on Design Au-tomaiton of Electronic Systems. 2006, 11(3):537–563
[103] N. Aslam, T.Arslan, A.Erdogan. Algorithmic Level Design Space Exploration ToolFor Creation of Highly Optimized Synthesizable Circuits. IEEE International Con-ference on Acoustic Speech and Signal Processing (ICASSP). 2007:81–84
[104] M. Gries. Methods for Evaluating and Covering the Design Space During EarlyDesign Development. Integration the VLSI Journal. 2004, 38(2):131–183
[105] M. M. Ziegler, M. R. Stan. A Unified Design Space for Regular Parallel PrefixAdders. Proceedings of the Conference on Design, Automation and Test in Europe.2004, 21386
[106] Jianhua Liu, Yi Zhu, Haikun Zhu, C. K. Cheng, J. Lillis. Optimum Prefix Addersin a Comprehensive Area, Timing and Power Design Space. Proceedings of the 2007Asia and South Pacific Design Automation Conference. 2007:609–615
[107] S. Ghosh, K. Roy. Exploring high-speed low-power hybrid arithmetic units at scaledsupply and adaptive clock-stretching. Proceedings of the 2008 Asia and South PacificDesign Automation Conference. 2008:635–640
[108] Yi Zhu, Jiahua Liu, Haikun Zhu, C. K. Cheng. Timing-power optimization formixed-radix ling adders by integer programming. Proceedings of the 2008 Asia andSouth Pacific Design Automation Conference. 2008:131–137
[109] W. Hasselbring, R. Reussner. Toward Trustworthy Software Systems. IEEE Com-puter. 2006, 39(4):91–92
[110] O. E. Williamson. Calculativeness, Trust and Economic Organization. Journal ofLaw and Economics. 1993, 36:453–486
[111] K. W. Miller, J. Voas. The Metaphysics of Software Trust. IT Professional. 2009,11(2):52–55
[112] S. P. Marsh. Formalising trust as a computational concept. Ph.D. thesis, Universityof Stirling, Scotland, 1994
[113] S. Wright. Trust and Trustworthiness. Philosophia. Published online, 2009
[114] R. Holton. Deciding to trust, coming to believe. Australasian Journal of Philosophy.1994, 72(1):63–76
[115] O. Han?ing. How we trust one another. Philosophy (London, England). 2008,83(2):161–177
[116] H. Hexmoor. A Methodology for Comparing Service Policies Using a Trust Model.International Journal of Computer Science and Applications. 2009, 6(4):1–15
[117] S. Braynov. Trust Learing Based on Past Experience. Proceedings of KnowledgeIntensive Multiagent Systems. 2005:197–200
[118] A. A. Rahman, S. Hailes. Supporting Trust in Virtual Communities. Proceedingsof the 33rd Hawaii International Conference on System Sciences. 2000, 6:6007
[119] A. Elfatatry. Dealing with change: components versus services. Communicationsof the ACM. 2007, 50(8):35–39
[120] A. Sheth, K. Verma, K. Gomadam. Semantics to energize the full services spectrum.Communications of the ACM. 2006, 49(7):55–61
[121] M. B. Blake. Decomposing Composition: Service-oriented Software Engineers. IEEESoftware. 2007, 24(6):68–77
[122] SIIA. Software as a Service: Strategic Backgrounder. Tech. rep., Software & Infor-mation Industry Association, Washington DC, 2001
[123] H. Chesbrough, J. Spohrer. A Research manifesto for service science. Communica-tions of the ACM. 2006, 49(7):35–40
[124] A UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded sys-tems, Beta 2. Object Management Group, OMG, June, 2008
[125] J. Boegh. A New Standard for Quality Requirements. IEEE Software. 2008,25(2):57–63
[126] D. Jackson. A Direct Path to Dependable Software. Communications of the ACM.2009, 52(4):78–88
[127] D. Mackenzie. Mechanizing Proof: Computing, Risk, and Trust. MIT Press. 2001
[128] P. Ladkin, Transcriber. Transcription of Report on the Accidentof Airbus A320-211 Aircraft in Warsaw on Sept. 14, 1993. MainCommission Aircraft Accident Investigation Warsaw; wwwrvsuni-bielefeldde/publications/Incidents/DOCS/ComAndRep/Warsaw/warsaw-reporthtml. 1993
[129] M. Schmidt, H. Lipson. Distilling Free-Form Natural Laws from Experimental Data.Science. 2009, 324(5923)
[130] J. J. Shedletsky. Commenton on the Sequential and Indeterminate Behavior of anEnd-Around-Carry Adder. IEEE Transactions on Computers. 1977:271–271
[131] X. Y. Zhang, Y. H. Chan, R. Montoye, et al. A 270ps 20mW 108-bit End-aroundCarry Adder for Multiply-Add Fused Floating Point Unit. Journal of Signal Pro-cessing Systems. 2009
[132] E. M. Schwarz. Binary Floating-Point Unit Design. Book chapter in High Perfor-mance Energy E?cient Microprocessor Design, Springer, US. 2006:189–208
[133] J. H. Liu, Y. Zhu, H. K. Zhu, et al. Optimum Prefix Adders in a ComprehensiveArea, Timing and Power Design Space. Proceedings of 12th conference on AsiaSouth Pacific design automation (ASP-DAC’07). 2007:609–615
[134] K. Vitoroulis, A. J. AI-Khalili. Performance of Parallel Prefix Adders implementedwith FPGA technology. IEEE Northeast Workshop on Circuits and Systems.2007:498–501
[135] S. Knowles. A Family of Adders. Proceedings of the 15th IEEE Symposium onComputer Arithmetic. April 14-16 2001:277–281. Adelaide, Australia
[136] J.M.Howie. Fundamentals of Semigroup Theory. Oxford University Press, USA,1996
[137] Gang Chen, Feng Liu. Proofs of correctness and properties of integer adder circuits.IEEE Trans on Computers. 2010, 59(1):134–136
[138] V. Kantabutra. A recursive carry-lookahead/carry-select hybrid adder. IEEETransComput. 1993, 42:1495–1499
[139] O. Kwon, Jr. E. E. Swartzlander, K. Nowka. A Fast Hybrid Carry-Lookahead/Carry-Select Adder Design. Proceedings of the 11th Great Lakers sym-posium on VLSI. 2001:149–152
[140] Yuke Wang, C. Pai, Xiaoyu Song. The Design of Hybrid Carry-Lookahead/Carry-Select Adders. IEEE Transactions on Circuits and Systems II:Analog and DigitalSignal Proessing . 2002, 49(1):16–24
[141] A. Tyagi. A reduced-area scheme for carry-select adders. IEEE Transaction onComputers. 1993, 42(10):1163–1170
[142] C. Arjhan and R. G. Deshmukh. A Novel Scheme for Irregular parallel-prefix adders.Proceedings of IEEE Southeastcon’97,’Engineering new New Century’. 1997
[143] Jungang Han, G. Stone. The implementation and verification of a conditional sumadder. Technical Reports, Department of Computer Science, University of Calgary,Calgary, Alberta, Canada. 1988
[144] K. M. Elleithy, M. A. Aref. A Rule-based Approach for High Speed Adders DesignVerification. 37th Midwest Symposium on Circuits and Systems. 1994:274–277
[145] H. Ling. High speed binary adder. IBM JRes and Devel. 1981, 25:156–166
[146] J. R. Burch, E. M. Clarke, D. E. Long, K. L. MacMillan and D. L. Dill. SymbolicModel Checking for Sequential Circuit Verification. IEEE Trans Computer-AidedDesign of Integrated Circuits and Systems. 1994, 13(4):401–424
[147] R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEETrans Computers. 1986, 35(8):677–691
[148] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checkingusing SAT procedures instead of BDDs. in Proc Int DAC. 1999:317–320
[149] M. Wedler, D. Sto?el, R. Brinkmann, W. Kunz. A Normalization Method for Arith-metic Data-Path Verification. IEEE Trans Computer-Aided Design of IntegratedCircuits and Systems. 2007, 26(11):1909–1922
[150] M. Kaufmann, J. Moore. ACL2: An Industrial Strength Version of NQTHM. Proc11th Ann Conf Computer Assurance (COMPASS’96). 1996:23
[151] J. Sawada, W. A. Hunt. Processor Verification with Precise Exceptions and Spec-ulative Execution. Proc 10th Int’l Computer Aided Verification Conf (CAV’98).1998:135–146
[152] D. Kapur, H. Zhang. An Overview of Rewrite Rule Laboratory (RRL). J Computerand Math with Applications. 1995, 29(2):91–114
[153] J. O’Leary, X. Zhao, R. Gerth, and C. -J. H. Seger. Formally verification IEEEcompliance of ?oating point hardware. Intel Technology Journal. 1999, 3(1)
[154] R. Kaivola, N. Narasimhan. Formal verification of the Pentium 4 ?oating-pointmultiplier. Proceedings of the Design, Automation and Test in Europe Conferenceand Exhibition, (DATE’02). 2002:20–27
[155] J. S. Moore, T. Lynch, M. Kaufmann. A mechanically checked proof of the cor-rectness of the kernel of the AMD5K86 ?oating-point division program. IEEETransactions on Computers. 1998, 47:913–926
[156] D. M. Russino?. A case study in formal verification of register-transfer logic withACL2: The ?oating point adder of the AMD Athlon processor. Proceedings of5th Internation Conference, Formal Methods in Computer-Aided Design, (FM-CAD’2000)). 2000:22–55
[157] Y. -A. Chen, R. E. Bryant. Verification of ?oating point adders. Proc InternationalConference on Computer Aided Verification, (CAV’98). 1998:488–499
[158] C. Berg, C. Jacobi. Formal verification of the VAMP ?oating point unit. ProcCorrect Hardware Design and Verification Methods, iith IFIP WG 105 AdvancedResearch Working Conference, (CHARME’01). 2001:325–339
[159] C. Jacobi. Formal Verification of a Fully IEEE Compliant Floating Point Unit.Ph.D. thesis, PhD thesis, University of the Saarland. Available on the Web ashttp://engr.smu.edu/ seidel/research/diss-jacobi.ps.gz., 2002
[160] J. Harrison. Floating-Point Verification Using Theorem Proving. Formal Methodsfor Hardware Verification, 6th International School on Formal Methods for the De-sign of Computer, Communication, and Software Systems, (SFM’06). 2006:211–242
[161] S. Boldo, G. Melquiond. Emulation of FMA and Correctly Rounded Sums: ProvedAlgorithms Using Rounding to Odd. IEEE Transactions on Computers. 2008,57(4):462–471
[162] S. Boldo, M. Daumas, R. C. Li. Formally Verified Argument Reduction with aFused-Multiply-Add. IEEE Transactions on Computers, accepted for publication.2009
[163] C. Jacobi, K. Weber, V. Paruthi, J. Baumgartner. Automatic Formal Verificationof Fused-Mulitpy-Add FPUs. Proceedings of the Design, Automation and Test inEurope Conference and Exhibition, (DATE’05). 2005, 2:1298–1303
[164] T. Grotker, S. Liao, G. Martin, S. Swan. System Design with SystemC. KiuwerAcademic Publishers, 2002
[165] AspectC++. http://www.aspect.org
[166] D. Deharbe, S. Medeiros. Aspect-oriented design in SystemC: implementation andapplications. In Proceedings of the 19th annual symposium on Integrated circuitsand systems design. 2006:119–124
[167] G. Jakachi. Aspect-oriented techniques for extraction of communication models. InProceedings of the 5th International Conference ASIC. 2003:262–265
[168] M. Engel, O.Spinczyk. Aspect in Hardware: what do they look like? In Proceedingsof 2008 ASOD workshop on Aspects, components, and patterns for infrastructuresoftware. 2008:1–6
[169] D. Robision. An Introduction to Aspect-oriented Programming in e.http://wwwverilabcom/-downloadshtml. 2006
[170] R. Chris. Elements of Functional Programming. Boston, MA: Addison-WesleyLongman Publishing Co, 1989
[171] H. Mili, A. Elkharraz, H. Mcheick. Understanding Separation of Concerns. InEarly Aspects: Aspect-Oriented Requirements Engineering and Architecture De-sign. 2004:75–84
[172] H. Ossher, P. Tarr. Multi-dimensional Spearation of Concerns and the HyperspaceApproach. In Proceedings of the Symposium on Software Architectures and Com-ponent Technology: the State of the Art in Software Development. 2000
[173] R. Laddad. AspectJ in Action: Practical Aspect-oriented Programming . ManningPublication Co. 2003
[174] K. Gregor, J. Lamping, A. Mendhekar, et al. Aspect-oriented Programming. In Pro-ceedings of the European Conference on Object-Oriented Programming. 1997:220–242
[175] A. Varma, E. Debes, I. Kozintsev, et al. Accurate and fast system-level power mod-eling: An XScale-based case study. ACM Transactions on Embedded ComputingSystems. 2008, 7(3)
[176] G. Beltrame, D. Sciuto, C. Silvano. Multi-Accuracy Power and PerformanceTransaction-Level Modeling. IEEE Transactions on Computer-Aided Design of In-tegrated Circuits and Systems. 2007, 26(10):1830–1842
[177] F. Klein, G. Araujo, R. Azevedo, and et al. An E?cient Framework for High-LevelPower Exploration. Proceedings of the 50th Midwest Symposium on Circuits andSystems, MWSCAS 2007. 2007:1046–1049
[178] F. Klein, R. Leao, G. Araujo, L. Santors, R. Azevedo. PowerSC: A SystemC-basedframework for power estimation. Technical Report IC-07-02, Institute of Computing,UNICAMP. February 2007
[179] N. Dhanwada, I. C. Lin, V. Narayanan. A Power Estimation Methodology forSystemC Transaction. Proceedings of the 3rd IEEE/ACM/IFIP international con-ference on Hardware/software codesign and system synthesis, CODES+ISSS’05.2005:142–147
[180] R. Damaˇseviˇcius, V. Sˇtuikys. Estimation of Power Consumption at BehavioralModeling Level Using SystemC. EURASIP Journal on Embedded Systems. 2007,2007(ID 68673)
[181] R. Damaˇseviˇcius. Estimation of design characteristics at RTL modeling level usingSystemC . Information Technology and Control. 2006, 35(2):117–123
[182] P. Landman. High-level power estimation. Proc Int Symp Low Power Electronicsand Design. 1996:29–35
[183] E. Macii, M. Pedram, F. Somenzi. High-Level Power Modeling, Estimation, andOptimization. IEEE Transactions on Computer-Aided Design of Integrated Circuitsand Systems. 1998, 17(11):1061–1079
[184] S. Gupta, F. N. Najm. Power macromodeling for high level power estimation. Pro-ceedings of the 34th annual conference on Design automation, DAC’97. 1997:365–370
[185] T. Simunic, L. Benini, G. D. Micheli. Cycle-accurate simulation of energy consump-tion in embedded systems. Proceedings of 36th Design Automation Conference,DAC’99. 1999:867–872
[186] S. Dontharaju, S. Tung, J. T. Cain, et al. A Design Automation and Power Es-timation Flow for RFID Systems. ACM Transactions on Design Automation ofElectronic Systems (TODAES). 2009, 14(1):1–31
[187] L. Ost, G. Guindani, L. S. Indrusiak, et al. A High Abstraction, High AccuracyPower Estimation Model for Networks-on-chip. Proceedings of the 22nd AnnualSymposium on Integrated Circuits and System Design (SBCCI’09). 2009:1–6
[188] E. Macii, M. Poncino. Power macro-models for high-level power estimation, CRCPress, 2005. Low-Power Electronics Design
[189] A. Raghunathan, S. Dey, N. K. Jha. Register-transfer level estimation techniques forswitching activity and power consumption. Digest of Technical Papers, IEEE/ACMInternational Conference on Computer-Aided Design, ICCAD’96. 1996:158–165
[190] S. Gupta, F. N. Najm. Energy and peak-current per-cycle estimation at RTL. IEEETransactioins on Very Large Scale Integeration (VLSI) Systems. 2003, 11(4):525–537
[191] M. Anton, I. Coonescu, E. Macii, M. Poncino. Fast characterization of RTL powermacromodels. The 8th IEEE International Conference on Electronics, Circuits andSystems, ICECS’01. 2001, 3:1591–1594
[192] P. E. Landman, J. M. Rabaey. Activity-sensitive architectural power analysis.IEEE Transactions on Computer-Aided Design of Integrated Circuits. June 2002,15(6):571–587
[193] H. Mehta, R. M. Owens, M. J. Irwin. Energy characterization based on clustering.Proceedings of 33rd Design Automation Conference, DAC’96. June 1996:702–707
[194] W. Ye, N. Vijaykrishnan, M. Kandemir, M. J. Irwin. The design and use of sim-plePower: a cycle-accurate energy estimation tool. Proceedings of 37th DesignAutomation Conference, DAC’00. 2000:340–345
[195] N. Bansal, K. Lahiri, A. Raqhunathan, S. T. Chakradhar. Power monitors: aframework for system-level power estimation using heterogeneous power models.Proceedings of 18th International Conference on VLSI Design. 2005:579–585
[196] N. H. W. Weste, K. Eshraghian. Principles of CMOS VLSI design, A systemsperspective. Addison Wesley, 1993
[197] K. Czamecki, S. Helsen. Feature-based Survery of Model Transformation Ap-proaches. IBM Systems Journal. 2006, 45(3)
[198] OMG. MOF 2.0 Query/Views/Transformation RFP. OMG Document ad. 2002
[199] OMG. MOF 2.0. Query/Views/Transformation Specification Version 10. 2008
[200] OMG. OMG Unified Modeling Language Infrastructure V2.12, 2007
[201] OMG. UML Profile for System on Chip (SOC) Specification. version 101. 2006
[202] Y. Wang, X. Zhou, B. Zhou, L. Liang and C. Peng. A MDA based SoC ModelingApproach using UML and SystemC. Proc of CIT. 2006
[203] C. Xi, L. Jianhua, Z. Zucheng and S. Yaohui. Modeling SystemC Design in UMLand Automatic Code Generation. Proc of ASP-DAC. 2005
[204] B. A. Correa, J. F. Eusse, D. Munera, et al. Hign Level System-on-Chip Designusing UML and SystemC. Proc of Electronic, Robotics and Automotive MechanicsConference (CERMA). 2007
[205] E. Riccobene, P. Scandurra, S. Rosti, A. Bocchio. A SoC Design MethodologyInvolving a UML 2.0 Profile for SystemC. Design Automation and Test Europe(DATE). 2005
[206] E. Riccobene, P. Scandurra, S. Rosti, A. Bocchio. A UML 2.0 Profile for SystemC:Toward High-level SoC Design. EMSOFT’05. 2005
[207] W. Mueller, S. Rosti, A. Bocchio, et al. UML for ESL Design-Basic Principles, Tools,and Applications. Proc of IEEE/ACM International Conference on Computer AidedDesign (ICCAD). 2006
[208] F. Coyle, M. Thomton. Form UML to HDL: A Model Driven Architecture Ap-proach to Hardware-Software Co-Design. Information Systems: New GenerationsConference (ISNG). 2005
[209] L. Li, F. Coyle, M. Thomton. UML to SystemVerilog Synthesis For Embedded Sys-tem Models with Support for Assertion Generation. Proc of Forum on Specificationand Design Languages (FDL). 2007
[210] SysML, http://www.sysml.org/
[211] F. Jouault, F. Alliaire. J. Bezivin, et al. ATL: A QVT-like Transformation Lan-guage. Proc of the 21st ACM Symposium on Object-oriented Programming SystemsLanguages and Applicaitons (SIGPLAN). 2006
[212] ModelMorf. http://www.tcs-trddc.com/ModelMorf/index.htm
[213] MedianQVT. http://projects.ikv.de/qvt/
[214] SmartQVT. http://smartqvt.elibel.tm.fr/
[215] Zhanqi Cui, Linzhang Wang, Xuandong Li. Modeling and Integrating Aspects withUML Activity Diagrams. SAC’09. 2009
[216] J. Whittle, P. Jayaraman. MATA: A Tool for Aspect-Oriented Modeling Based onGraph Transformation. MoDeLS 2007 Workshops. 2007:16–27
[217] D. Stein, S. Hanenberg, R. Unland. An UML-based Aspect-Oriented Design NotainFor AspectJ. AOSD’02. 2002
[218] J. U. Junior, V. V. de Camargo, C. V. Flach. UML-AOF: A Profile for ModelingAspect-Oriented Frameworks. AOM’09. 2009
[219] J. Evermann. A Meta-Level Specification and Profile for AspectJ in UML. AOM’07.2007
[220] J. Evermann. A Meta-Level Specification and Profile for AspectJ in UML. Journalof Object Technology. 2006, 6(7):27–49
[2]孙海平.计算机算术中若干前缀计算问题的研究. Ph.D. thesis,合肥工业大学,2006
[3] M. J. Flynn, S. F. Oberman. Advanced Computer Arithmetic Design. Wiley-Interscience, 2001
[4] Y. Shimazu, T. Kengaku, T. Fujiyama, E. Teraoka, et al. A 50MHz 24b Floating-Point DSP. In Proc of the IEEE International Solid-State Circuit Conference.1989:44–45
[5] S. F. Oberman. Design issues in high performance ?oating point arithmetic units.PhD thesis, Stanford University. 1996
[6] ANSI/IEEE Std, 754-2008. Binary Floating-Point Arithmetic. Tech. rep., IEEE-SAStandards Board, 2008
[7] I. Koren. Computer Arithmetic Algorithms. A. K. Peters, Natick, MA, 2002
[8] General Processor Information. Berkeley CPU information center at. Tech. rep.,http://bwrc.eecs.berkeley.edu/CIC/summary/local/summary.pdf, 2001
[9] A. Nannarelli. Low Power Division and Square Root. PhD thesis, University ofCalifornia. 1999
[10] M. Paragelis, D. Plexousakis, and T. Kutsuras. Alleviating the Sparsity Problemof Collaborative Filtering Using Trust Inferences. Trust Management, ProceedingsLecture Notes in Computer Science. 2005, 3477:224–239
[11] G. Pitsilis, L. Marshall. Trust as a Key to Improving Recommendation Sys-tems. Trust Management, Proceedings Lecture Notes in Computer Science. 2005,3477:210–223
[12] P. Giorgini, F. Massacci, J. Mylopoulos, N. Zannone. Modeling Social and IndividualTrust in Requirements Engineering Methodologies. Trust Management, ProceedingsLecture Notes in Computer Science. 2005, 3477:161–176
[13] B. Wong, C. Bibeau, K. A. Bishop, G. G. Rosenthal. Response to Perceived Preda-tion Threat in Fiddler Crabs: Trust Thy Neighbor as Thyself? Behavioral Ecologyand Sociobiology. 2005, 58(4):345–350
[14] A. Josang, C. Keser, T. Dimtrakos. Can We Manage Trust? Trust Management,Proceedings Lecture Notes in Computer Science. 2005, 3477:93–107
[15] J. M. Seigneur, A. Gray, C. D. Jensen. Trust Transfer: Encouraging Self-recommendations without Sybil Attack. Trust Management, Proceedings LectureNotes in Computer Science. 2005, 3477:321–337
[16] N. Dimmock, J. Bacon, D. Ingram, K. Moody. Risk Models for Trust-based Ac-cess Control (TBAC). Trust Management, Proceedings Lecture Notes in ComputerScience. 2005, 3477:364–371
[17] S. Pearson, M. C. Mont, S. Crane. Persistent and Dynamic Trust: Analysis andthe Related Impact of Trusted Platforms. Trust Management, Proceedings LectureNotes in Computer Science. 2005, 3477:355–363
[18]孙道奇.基于信任和服务模型的普适计算安全问题研究. Ph.D. thesis,东华大学, 2008
[19] Jsang and R. Ismail. The beta reputation system. In Proceedings of 15th BledElectronic Commerce Conference. 2002
[20] Y. Wang, J. Vassileva. Trust and Reputation Model in Peer-to-Peer Networks. ThirdInternational Conference on Peer-to-Peer Computing (P2P103), IEEE. 2003
[21] V. Cahill, B. Shand, E. Gray, et al. Using Trust for Secure Collaboration in Uncer-tain Environments. Pervasive Computing. 2003, 2(3):52–61
[22] A. A. Rahman, S. Hailes. Supporting Trust in Virtual Communities. Hawaii Inter-national Conference on System Sciences. 2000
[23] J. Sabater, C. Sierra. Reputation and Social Network Analysis in Muti-Agent Sys-tems. First International Joint Conference on Autonomous Agents and Muti-AgentSystems. 2001
[24] S. Song, K. Hwang, R. EZhou. Trusted P2P Transactions with Fuzzy ReputationAggregation. IEEE Internet Computing. 2005, 18(28)
[25] S. Karnvar, M. Schlosser. The EigenTrust Algorithm for Reputation Managemtn inP2P Networks. WWW. 2003
[26] W. Don, H. M. Wang, Y. Jia, P. Zou. A Recommendation-based Peer-to-Peer TrustModel. Journal of Software. 2004, 15(4):571–583
[27] D. Yamamoto, T. Asahara, Itao, et al. Distributed Pagerank: A Distributed Repu-tation Model for Open P2P Networks. Proceedings of the 2004 International Sym-posium on Applications and the Internet Workshops. 2004
[28] B. Yu, M. P. Singh, K. Sycara. Developing Trust in Largescale Peer-to-Peer Systems.Proceedings of the 1st IEEE Symposium on Multi-Agent Security and Suwiability.2004
[29] A. Josang. Trust-Based Decision Making for Electronic. Proceedings of the 4thNordic Workshop on Secure Computer Systems. 1999
[30] G. H. Nibaldi. Specification of a Trusted Computing Base. Technical Report, M79-228 The MITRE Corporation, Bedford, MA, USA. 1979
[31] Department of Defense Computer Security Center. Department of Defense TrustedComputer System Evaluation Criteria. Tech. rep., DoD, USA, 1985
[32] TCPA. TPM protection profile v.1.9.7. Tech. rep., TCPA,http//www.trustedcomputing.org/home, 2006-04-21
[33] TCPA. Main specification v 1.1b. Tech. rep., TCPA,http//www.trustedcomputing.org/home, 2006-04-25
[34] TCG. Trusted computing group(TCG) main specification version 1.1a. Tech. rep.,http://www.trustedcomputinggroup/downloads/tcg spec 1 1b.zip, 2006-04-30
[35] TCG. TCG PC specific, implementation specification version 1.1. Tech. rep.,http://www.trustedcomputinggroup/downloads/TCG PCSpecificSpecification v1 1.pdf,2006-04-26
[36] S. Pearson. Trusted Computing Platforms, the Next Security Solutoin. Tech. rep.,Technical report, Trusted E-Services Laboratory, HP Laboratories Bristol HPL-2002-221, 2002
[37] The Open Trusted Computing (OpenTC) consortium. General activities ofOpenTC. Tech. rep., http://www.opentc.net/activities/, 2006
[38]张焕国,罗捷,金刚,朱智强,余发江,严飞.可信计算研究进展.武汉大学学报(理学版). 2001, 52(5):513–518
[39] A. Avizienis, J. C. Laprie, B. Randell, C. Landwehr. Basic concepts and taxonomyof dependable and secure computing. IEEE Transactions on Dependable and SecureComputing. 2004, 1(1):11–33
[40] I. Sommerville. Software Engineering. AddisonWesley, 7th edition, 2004
[41] D. Patterson, A. Brown, P. Broadwell, et al. Recovery-Oriented Computing (ROC):Motivation, Definition, Techniques, and Case Studies. Tech. rep., Technical ReportTechnical Report UCB//CSD-02-1175, UC Berkeley Computer Science, 2002
[42] D. Oppenheimer, A. Ganapathi, D. Patterson. Why Do Internet Services Fail,and What Can Be Done About it. Proceedings of Usenix Symposium on InternetTechnologies and Systems. 2003:1–16
[43] L. J. Ho?man, K. L. Jenkins, J. Blum. Trust beyond security: an expanded trustmodel. Communications of the ACM. 2006, 49(7):94–101
[44] S. Becker, M. Boskovic, A. Dhama, et al. Trustworthy Software Systems: A Dis-cussion of Basic Concepts and Terminology. ACM SIGSOFT Software EngineeringNotes. 2006, 31(6):1–18
[45] The Second National Software Summit. Software 2015: A National Software Strat-egy to ensure U. S. Security and Competitiveness. Tech. rep., U. S. Center forNational Software Studies, 2005
[46] P. M. Kogge and H. S. Stone. A Parallel Algorithm for The E?cient Solution of AGeneral Class of Recurrence Equations. IEEE Transactions on Computers. 1973,22(8):786–793
[47] R. P. Brent, H. T. Kung. A Regular Layout for Parallel Adders. IEEE Transactionson Computers. 1982, C(31):260–264
[48] R. Ladner, M. Fischer. Parallel Prefix Computation. JACM. 1980, 27(4):831–838
[49] I. Koren. Computer Arithmetic Algorithms. A. K. Peters, Natick, MA, 2002
[50] J. Sklansky. Conditional-sum addition logic. IRE Trans. 1960, EC-9:226–231
[51] P. K. Chan, M. D. F. Schlag, C. D. Thomborson, and V. G. Oklobdzija. Delayoptimization of carry-skip adders and block carry-look-ahead adders using multidi-mendional dynamic programming. IEEE Trans on Computers. 1992, 41:920–930
[52] V. Kantabutra. Designing optimum carry-skip adders. Proc 8th Symp on ComputerArithmeitic. 1991:146–153
[53] C. S. Wallace. A suggestion for a fast multiplier. IEEE Trans on Computers. 1964,EC-13:14–17
[54] H. Ling. High speed binary adder. IBM J Res and Devel. 1981, 25:156–166
[55] M. J. Flynn, S. F. Oberman. Advanced computer arithmetic design. Wiley, NewYork, 2001
[56] P. K. Chan, M. D. F. Schlag. Analysis and design of CMOS Manchester adders withvariable carry-skip. IEEE Trans on Computers. 1990, 39:983–992
[57] T. Lyncn, E. E. Swartzlander, Jr. A spanning tree carry look-ahead adder. IEEETrans on Computers. 1992, 41:931–939
[58] D. W. Dobberpuhl, et al. A 200-MHz 64-b dual-issue CMOS microprocessor. IEEEJ of Solid-State Circuits. 1992, 27:1555–1565
[59] R. K. Montoye, E. Hokenek, S. L. Runyon. Design of the IBM RISC System/6000?oating-point execution unit. IBM Journal of Research and Development. 1990,34(1):59–70
[60] IBM. Enterprise Systems Architecture/390 Principles of Operation. Tech. rep.,Order No. SA227201-5, available through IBM branch o?ces, 1998
[61] S. Waser, M. J. Flynn. Introduction to Arithmetic for Digital Systems Designers.Holt, Rinehart, & Winston, 1982
[62] ANSI/IEEE Std, 754-1985. IEEE standard for binary ?oating-point arithmetic.Tech. rep., Institute of Electrical and Electronic Engineers, Inc. New York, 1985
[63] F. P. O’Connell, S. W. White. POWER3: The Next Generation of PowerPC Pro-cessors. IBM Journal of Research and Development. 2000, 44:873–884
[64] R. Jessani, C. Olson. The Floating-Point Unit of the PowerPC 603e. IBM Journalof Research and Development. 1996, 40:559–566
[65] R. M. Jessani, M. Putrino. Comparision of Single- and Dual-Pass Multiply-AddFused Floating-Point Units. IEEE Trans on Computers. 1998, 47:927–937
[66] A. Kumar. The HP PA-8000 RISC CPU. IEEE Micro Magazine. 1997, 17(2):27–32
[67] D. Hunt. Advanced Performance Features of the 64-bit PA-8000. Proceedings ofCompcon. 1995:123–128
[68] K. C. Yeager. The MIPS R10000 superscalar microprocessor. IEEE Micro Magazine.1996, 16(2):28–40
[69] C. Hinds. An Enhanced Floating Point Coprocessor for Embedded Signal Process-ing and Graphics Applications. Conference Record of the Thirty-Third AsilomarConference on Signals, Systems, and Computers. 1999:147–151
[70] B. Greer, J. Harrision, G. Henry, W. Li, P. Tang. Scientific Computing on theItanium Processor. Proceedings of the ACM/IEEE SC2001 Conference. 2001:1–8
[71] H. Sharangpani, K. Arora. Itanium Processor Microarchitecture. IEEE Micro Ma-ganize. 2000, 20(5):24–43
[72] E. C. Quinnell. Floating-Point Fused Multiply-Add Architectures. Ph.D. thesis, theUniversity of Texas at Austin, 2007
[73] Chen C, Chen L-A, et al. Architecture design of a fast ?oating-point multiplicaiton-add fused unit using signed-digit addition. IEE Proceedings- Computers and DigitalTechniques. 2002, 149(4):113–120
[74] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.Proceedings of 2002 IEEE International Conference on Computer Design: VLSI inComputers and Processors. 2002:145–150
[75] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.Tech. rep., Technical report, Department of Electrical and Computer Engineering,University of Santiago de Compostela, 2002
[76] T. Lang, J. D. Bruguera. Floating-point fused multiply-add with reduced latency.IEEE Trans on Computers. 2004, 53(8):988–1003
[77] M. R. Santoro, G. Bewick, et al. Rounding algorithms for IEEE multiplier. Pro-ceedings of Ninth IEEE Symposium on Computer Arithmetic. 1989:176–183
[78] S. F. Oberman, H. Al-Twaijry, M. J. Flynn. The SNAP Project: Design of Float-ing Point Arithmetic Units. Proceedings of 13th IEEE Symposium on ComputerArithmetic. 1997:156–165
[79] http://www-03.ibm.com/press/us/en/pressrelease/21580.wss
[80] B.Curran, B.McCredie, L.Siqal, et al. 4GHz+ Low-Latency Fixed-Point and BinaryFloating-Point Execution Units for the POWER 6 Processor. Digest of 2006 IEEEInternational Solid-State Circuits Conference. 2006:1728–1734
[81] X. Y. Yu, B. Fleischer, Y. H. Chan, et al. A 5GHz+ 128-bit Binary Floating-PointAdder for the POWER 6 Processor. Proceedings of the 32nd European Solid-StateCircuits Conference. 2006:166–169
[82] V. G. Dklobdzija, D. Villeger. Improving Multiplier Design By Using ImprovedColumn Compression Tree And Optimized Final Adders In CMOS Technology.IEEE Transactions on VLSI Systems. 1995, 3(2)
[83] V. G. Oklobdzija, D. Villeger. Multiplier Design Utilizing Improved Column Com-pression Tree And Optimized Final Adder In CMOS Technology. Proceedings ofthe 1993 International Symposium on VLSI Technology, Systems and Applications.1993:209–212
[84] V. G. Oklobdija, P. Stelling. Design Strategies for the Final Adder in a ParallelMultiplier. Twenty-Ninth Annual Asilomar Conference on signal, Systems, andComputers, Pacific Grove, California. 1995
[85] P. Stelling, V. G. Oklobdzija. Design Strategies for Optimal Hybrid Final Addersin a Parallel Multiplier. special issue on VLSI Arithmetic, Journal of VLSI SignalProcessing, Kluwer Academic Publishers. 1996, 14(3)
[86] B. R. Zeydel, V. G. Oklobdzija, S. Mathew, R. K. Krishnamurthy, S. Borkar. A 90nm1GHz 22mW 16×16 2’s Complement Multiplier for Wireless Baseband. Proceedingsof the 2003 Symposium on VLSI Circuits. 2003
[87] E. Clarke, O. Grumberg, D. Long. Verification tools for finite-state concurrentsystems. A Decade of Concurrency-Re?ections and Perspectives Lecture Notes inComputer Science. 1994, (803)
[88] E. M. Clarke, E. A. Emersion, A. P. Sistla. Automatic verfication of finite-stateconcurrent systems using temporal logic specificaitons. ACM Transactions on Pro-gramming Languages and Systems. 1986, 8(2):244–263
[89] D. A. Du?y. Principles of automated theorem proving. John Wiley & Sons, Inc.New York, NY, USA, 1991
[90] J.O’Donnell, G.Rnger. Derivation of a carry lookahead addition circuit. Journal ofFunctional Programming. 2004, 14(6):127–158
[91] D.Kapur, M.Subramaniam. Mechanical verification of adder circuits using rewriterulelaboratory. Formal Methods in System Design. 1998, 13(2):127–158
[92] M.Sheeran. Hardware design and functional programming: a perfect match. Journalof Universal Computer Science. 2005, 11(7):1135–1158
[93] L. Benini, G. de Micheli. System-level power optimization: techniques and tools .ACM Trans on Design Automation of Electronic Systems. 2000, 5(2):115–192
[94] R. Kumar, Zhiyu Liu, V. Kursun. Fundamental concepts of power and energymeasurement with the computer-aided-design tools. 50th Midwest Symposium onCircuits and Systems. 2007:863–866
[95] S. Ghissoni, J. B. dos Santos Martins, L. L. de Oliveira. A New Methodology inPower Estimation in CMOS Combinational Circuits at Logic Level. 48th MidwestSymposium on Circuits and Systems. 2005, 2:1251–1254
[96] L. Zhong, S. Ravi, A. Raghunathan, N. K. Jha. RTL-Aware Cycle-Accurate Func-tional Power Estimation. IEEE Trans on Computer-Aid Design of Integrated Cir-cuits and Systems. 2006, 25(10):2103–2117
[97] R. Chaudhry, D. Stasiak, S. Posluszny, S. Dhong. A Cycle Accurate Power Estima-tion Tool. Asia and South Pacific Conference on Design Automation. 2006:24–27
[98] G. Dimitrakopoulos, P. Kolovos, P. Kalogerakis, D. Nikolos. Design of High-SpeedLow-Power Parallel-Prefix VLSI Adders. Lecture Notes in Computer Science: Inte-grated Circuit and System Design. 2004:248–257
[99] A. Aslund. Power Estimation of High Speed Bit-Parallel Adders. Tech. rep., Linkop-ing University, LiTH-ISY-EX-3534-2004, 2004
[100] M. Aguirre, M. Linares. A altenative logic approach to implement high-speed low-power full adders cells. Proceedings of the 18th annual symposium on Integratedcircuits and system design. 2005:166–171
[101] S. Lakshmivarahan, S. K. Dhall. Parallel Computing Using The Prefix Problem.Oxford University Press, 1994
[102] A. Pinto, A. Bonivento, S.anni-vincentelli. System Level Design Paradigms:Platform-based Design and Communication Synthesis. ACM Trans on Design Au-tomaiton of Electronic Systems. 2006, 11(3):537–563
[103] N. Aslam, T.Arslan, A.Erdogan. Algorithmic Level Design Space Exploration ToolFor Creation of Highly Optimized Synthesizable Circuits. IEEE International Con-ference on Acoustic Speech and Signal Processing (ICASSP). 2007:81–84
[104] M. Gries. Methods for Evaluating and Covering the Design Space During EarlyDesign Development. Integration the VLSI Journal. 2004, 38(2):131–183
[105] M. M. Ziegler, M. R. Stan. A Unified Design Space for Regular Parallel PrefixAdders. Proceedings of the Conference on Design, Automation and Test in Europe.2004, 21386
[106] Jianhua Liu, Yi Zhu, Haikun Zhu, C. K. Cheng, J. Lillis. Optimum Prefix Addersin a Comprehensive Area, Timing and Power Design Space. Proceedings of the 2007Asia and South Pacific Design Automation Conference. 2007:609–615
[107] S. Ghosh, K. Roy. Exploring high-speed low-power hybrid arithmetic units at scaledsupply and adaptive clock-stretching. Proceedings of the 2008 Asia and South PacificDesign Automation Conference. 2008:635–640
[108] Yi Zhu, Jiahua Liu, Haikun Zhu, C. K. Cheng. Timing-power optimization formixed-radix ling adders by integer programming. Proceedings of the 2008 Asia andSouth Pacific Design Automation Conference. 2008:131–137
[109] W. Hasselbring, R. Reussner. Toward Trustworthy Software Systems. IEEE Com-puter. 2006, 39(4):91–92
[110] O. E. Williamson. Calculativeness, Trust and Economic Organization. Journal ofLaw and Economics. 1993, 36:453–486
[111] K. W. Miller, J. Voas. The Metaphysics of Software Trust. IT Professional. 2009,11(2):52–55
[112] S. P. Marsh. Formalising trust as a computational concept. Ph.D. thesis, Universityof Stirling, Scotland, 1994
[113] S. Wright. Trust and Trustworthiness. Philosophia. Published online, 2009
[114] R. Holton. Deciding to trust, coming to believe. Australasian Journal of Philosophy.1994, 72(1):63–76
[115] O. Han?ing. How we trust one another. Philosophy (London, England). 2008,83(2):161–177
[116] H. Hexmoor. A Methodology for Comparing Service Policies Using a Trust Model.International Journal of Computer Science and Applications. 2009, 6(4):1–15
[117] S. Braynov. Trust Learing Based on Past Experience. Proceedings of KnowledgeIntensive Multiagent Systems. 2005:197–200
[118] A. A. Rahman, S. Hailes. Supporting Trust in Virtual Communities. Proceedingsof the 33rd Hawaii International Conference on System Sciences. 2000, 6:6007
[119] A. Elfatatry. Dealing with change: components versus services. Communicationsof the ACM. 2007, 50(8):35–39
[120] A. Sheth, K. Verma, K. Gomadam. Semantics to energize the full services spectrum.Communications of the ACM. 2006, 49(7):55–61
[121] M. B. Blake. Decomposing Composition: Service-oriented Software Engineers. IEEESoftware. 2007, 24(6):68–77
[122] SIIA. Software as a Service: Strategic Backgrounder. Tech. rep., Software & Infor-mation Industry Association, Washington DC, 2001
[123] H. Chesbrough, J. Spohrer. A Research manifesto for service science. Communica-tions of the ACM. 2006, 49(7):35–40
[124] A UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded sys-tems, Beta 2. Object Management Group, OMG, June, 2008
[125] J. Boegh. A New Standard for Quality Requirements. IEEE Software. 2008,25(2):57–63
[126] D. Jackson. A Direct Path to Dependable Software. Communications of the ACM.2009, 52(4):78–88
[127] D. Mackenzie. Mechanizing Proof: Computing, Risk, and Trust. MIT Press. 2001
[128] P. Ladkin, Transcriber. Transcription of Report on the Accidentof Airbus A320-211 Aircraft in Warsaw on Sept. 14, 1993. MainCommission Aircraft Accident Investigation Warsaw; wwwrvsuni-bielefeldde/publications/Incidents/DOCS/ComAndRep/Warsaw/warsaw-reporthtml. 1993
[129] M. Schmidt, H. Lipson. Distilling Free-Form Natural Laws from Experimental Data.Science. 2009, 324(5923)
[130] J. J. Shedletsky. Commenton on the Sequential and Indeterminate Behavior of anEnd-Around-Carry Adder. IEEE Transactions on Computers. 1977:271–271
[131] X. Y. Zhang, Y. H. Chan, R. Montoye, et al. A 270ps 20mW 108-bit End-aroundCarry Adder for Multiply-Add Fused Floating Point Unit. Journal of Signal Pro-cessing Systems. 2009
[132] E. M. Schwarz. Binary Floating-Point Unit Design. Book chapter in High Perfor-mance Energy E?cient Microprocessor Design, Springer, US. 2006:189–208
[133] J. H. Liu, Y. Zhu, H. K. Zhu, et al. Optimum Prefix Adders in a ComprehensiveArea, Timing and Power Design Space. Proceedings of 12th conference on AsiaSouth Pacific design automation (ASP-DAC’07). 2007:609–615
[134] K. Vitoroulis, A. J. AI-Khalili. Performance of Parallel Prefix Adders implementedwith FPGA technology. IEEE Northeast Workshop on Circuits and Systems.2007:498–501
[135] S. Knowles. A Family of Adders. Proceedings of the 15th IEEE Symposium onComputer Arithmetic. April 14-16 2001:277–281. Adelaide, Australia
[136] J.M.Howie. Fundamentals of Semigroup Theory. Oxford University Press, USA,1996
[137] Gang Chen, Feng Liu. Proofs of correctness and properties of integer adder circuits.IEEE Trans on Computers. 2010, 59(1):134–136
[138] V. Kantabutra. A recursive carry-lookahead/carry-select hybrid adder. IEEETransComput. 1993, 42:1495–1499
[139] O. Kwon, Jr. E. E. Swartzlander, K. Nowka. A Fast Hybrid Carry-Lookahead/Carry-Select Adder Design. Proceedings of the 11th Great Lakers sym-posium on VLSI. 2001:149–152
[140] Yuke Wang, C. Pai, Xiaoyu Song. The Design of Hybrid Carry-Lookahead/Carry-Select Adders. IEEE Transactions on Circuits and Systems II:Analog and DigitalSignal Proessing . 2002, 49(1):16–24
[141] A. Tyagi. A reduced-area scheme for carry-select adders. IEEE Transaction onComputers. 1993, 42(10):1163–1170
[142] C. Arjhan and R. G. Deshmukh. A Novel Scheme for Irregular parallel-prefix adders.Proceedings of IEEE Southeastcon’97,’Engineering new New Century’. 1997
[143] Jungang Han, G. Stone. The implementation and verification of a conditional sumadder. Technical Reports, Department of Computer Science, University of Calgary,Calgary, Alberta, Canada. 1988
[144] K. M. Elleithy, M. A. Aref. A Rule-based Approach for High Speed Adders DesignVerification. 37th Midwest Symposium on Circuits and Systems. 1994:274–277
[145] H. Ling. High speed binary adder. IBM JRes and Devel. 1981, 25:156–166
[146] J. R. Burch, E. M. Clarke, D. E. Long, K. L. MacMillan and D. L. Dill. SymbolicModel Checking for Sequential Circuit Verification. IEEE Trans Computer-AidedDesign of Integrated Circuits and Systems. 1994, 13(4):401–424
[147] R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEETrans Computers. 1986, 35(8):677–691
[148] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checkingusing SAT procedures instead of BDDs. in Proc Int DAC. 1999:317–320
[149] M. Wedler, D. Sto?el, R. Brinkmann, W. Kunz. A Normalization Method for Arith-metic Data-Path Verification. IEEE Trans Computer-Aided Design of IntegratedCircuits and Systems. 2007, 26(11):1909–1922
[150] M. Kaufmann, J. Moore. ACL2: An Industrial Strength Version of NQTHM. Proc11th Ann Conf Computer Assurance (COMPASS’96). 1996:23
[151] J. Sawada, W. A. Hunt. Processor Verification with Precise Exceptions and Spec-ulative Execution. Proc 10th Int’l Computer Aided Verification Conf (CAV’98).1998:135–146
[152] D. Kapur, H. Zhang. An Overview of Rewrite Rule Laboratory (RRL). J Computerand Math with Applications. 1995, 29(2):91–114
[153] J. O’Leary, X. Zhao, R. Gerth, and C. -J. H. Seger. Formally verification IEEEcompliance of ?oating point hardware. Intel Technology Journal. 1999, 3(1)
[154] R. Kaivola, N. Narasimhan. Formal verification of the Pentium 4 ?oating-pointmultiplier. Proceedings of the Design, Automation and Test in Europe Conferenceand Exhibition, (DATE’02). 2002:20–27
[155] J. S. Moore, T. Lynch, M. Kaufmann. A mechanically checked proof of the cor-rectness of the kernel of the AMD5K86 ?oating-point division program. IEEETransactions on Computers. 1998, 47:913–926
[156] D. M. Russino?. A case study in formal verification of register-transfer logic withACL2: The ?oating point adder of the AMD Athlon processor. Proceedings of5th Internation Conference, Formal Methods in Computer-Aided Design, (FM-CAD’2000)). 2000:22–55
[157] Y. -A. Chen, R. E. Bryant. Verification of ?oating point adders. Proc InternationalConference on Computer Aided Verification, (CAV’98). 1998:488–499
[158] C. Berg, C. Jacobi. Formal verification of the VAMP ?oating point unit. ProcCorrect Hardware Design and Verification Methods, iith IFIP WG 105 AdvancedResearch Working Conference, (CHARME’01). 2001:325–339
[159] C. Jacobi. Formal Verification of a Fully IEEE Compliant Floating Point Unit.Ph.D. thesis, PhD thesis, University of the Saarland. Available on the Web ashttp://engr.smu.edu/ seidel/research/diss-jacobi.ps.gz., 2002
[160] J. Harrison. Floating-Point Verification Using Theorem Proving. Formal Methodsfor Hardware Verification, 6th International School on Formal Methods for the De-sign of Computer, Communication, and Software Systems, (SFM’06). 2006:211–242
[161] S. Boldo, G. Melquiond. Emulation of FMA and Correctly Rounded Sums: ProvedAlgorithms Using Rounding to Odd. IEEE Transactions on Computers. 2008,57(4):462–471
[162] S. Boldo, M. Daumas, R. C. Li. Formally Verified Argument Reduction with aFused-Multiply-Add. IEEE Transactions on Computers, accepted for publication.2009
[163] C. Jacobi, K. Weber, V. Paruthi, J. Baumgartner. Automatic Formal Verificationof Fused-Mulitpy-Add FPUs. Proceedings of the Design, Automation and Test inEurope Conference and Exhibition, (DATE’05). 2005, 2:1298–1303
[164] T. Grotker, S. Liao, G. Martin, S. Swan. System Design with SystemC. KiuwerAcademic Publishers, 2002
[165] AspectC++. http://www.aspect.org
[166] D. Deharbe, S. Medeiros. Aspect-oriented design in SystemC: implementation andapplications. In Proceedings of the 19th annual symposium on Integrated circuitsand systems design. 2006:119–124
[167] G. Jakachi. Aspect-oriented techniques for extraction of communication models. InProceedings of the 5th International Conference ASIC. 2003:262–265
[168] M. Engel, O.Spinczyk. Aspect in Hardware: what do they look like? In Proceedingsof 2008 ASOD workshop on Aspects, components, and patterns for infrastructuresoftware. 2008:1–6
[169] D. Robision. An Introduction to Aspect-oriented Programming in e.http://wwwverilabcom/-downloadshtml. 2006
[170] R. Chris. Elements of Functional Programming. Boston, MA: Addison-WesleyLongman Publishing Co, 1989
[171] H. Mili, A. Elkharraz, H. Mcheick. Understanding Separation of Concerns. InEarly Aspects: Aspect-Oriented Requirements Engineering and Architecture De-sign. 2004:75–84
[172] H. Ossher, P. Tarr. Multi-dimensional Spearation of Concerns and the HyperspaceApproach. In Proceedings of the Symposium on Software Architectures and Com-ponent Technology: the State of the Art in Software Development. 2000
[173] R. Laddad. AspectJ in Action: Practical Aspect-oriented Programming . ManningPublication Co. 2003
[174] K. Gregor, J. Lamping, A. Mendhekar, et al. Aspect-oriented Programming. In Pro-ceedings of the European Conference on Object-Oriented Programming. 1997:220–242
[175] A. Varma, E. Debes, I. Kozintsev, et al. Accurate and fast system-level power mod-eling: An XScale-based case study. ACM Transactions on Embedded ComputingSystems. 2008, 7(3)
[176] G. Beltrame, D. Sciuto, C. Silvano. Multi-Accuracy Power and PerformanceTransaction-Level Modeling. IEEE Transactions on Computer-Aided Design of In-tegrated Circuits and Systems. 2007, 26(10):1830–1842
[177] F. Klein, G. Araujo, R. Azevedo, and et al. An E?cient Framework for High-LevelPower Exploration. Proceedings of the 50th Midwest Symposium on Circuits andSystems, MWSCAS 2007. 2007:1046–1049
[178] F. Klein, R. Leao, G. Araujo, L. Santors, R. Azevedo. PowerSC: A SystemC-basedframework for power estimation. Technical Report IC-07-02, Institute of Computing,UNICAMP. February 2007
[179] N. Dhanwada, I. C. Lin, V. Narayanan. A Power Estimation Methodology forSystemC Transaction. Proceedings of the 3rd IEEE/ACM/IFIP international con-ference on Hardware/software codesign and system synthesis, CODES+ISSS’05.2005:142–147
[180] R. Damaˇseviˇcius, V. Sˇtuikys. Estimation of Power Consumption at BehavioralModeling Level Using SystemC. EURASIP Journal on Embedded Systems. 2007,2007(ID 68673)
[181] R. Damaˇseviˇcius. Estimation of design characteristics at RTL modeling level usingSystemC . Information Technology and Control. 2006, 35(2):117–123
[182] P. Landman. High-level power estimation. Proc Int Symp Low Power Electronicsand Design. 1996:29–35
[183] E. Macii, M. Pedram, F. Somenzi. High-Level Power Modeling, Estimation, andOptimization. IEEE Transactions on Computer-Aided Design of Integrated Circuitsand Systems. 1998, 17(11):1061–1079
[184] S. Gupta, F. N. Najm. Power macromodeling for high level power estimation. Pro-ceedings of the 34th annual conference on Design automation, DAC’97. 1997:365–370
[185] T. Simunic, L. Benini, G. D. Micheli. Cycle-accurate simulation of energy consump-tion in embedded systems. Proceedings of 36th Design Automation Conference,DAC’99. 1999:867–872
[186] S. Dontharaju, S. Tung, J. T. Cain, et al. A Design Automation and Power Es-timation Flow for RFID Systems. ACM Transactions on Design Automation ofElectronic Systems (TODAES). 2009, 14(1):1–31
[187] L. Ost, G. Guindani, L. S. Indrusiak, et al. A High Abstraction, High AccuracyPower Estimation Model for Networks-on-chip. Proceedings of the 22nd AnnualSymposium on Integrated Circuits and System Design (SBCCI’09). 2009:1–6
[188] E. Macii, M. Poncino. Power macro-models for high-level power estimation, CRCPress, 2005. Low-Power Electronics Design
[189] A. Raghunathan, S. Dey, N. K. Jha. Register-transfer level estimation techniques forswitching activity and power consumption. Digest of Technical Papers, IEEE/ACMInternational Conference on Computer-Aided Design, ICCAD’96. 1996:158–165
[190] S. Gupta, F. N. Najm. Energy and peak-current per-cycle estimation at RTL. IEEETransactioins on Very Large Scale Integeration (VLSI) Systems. 2003, 11(4):525–537
[191] M. Anton, I. Coonescu, E. Macii, M. Poncino. Fast characterization of RTL powermacromodels. The 8th IEEE International Conference on Electronics, Circuits andSystems, ICECS’01. 2001, 3:1591–1594
[192] P. E. Landman, J. M. Rabaey. Activity-sensitive architectural power analysis.IEEE Transactions on Computer-Aided Design of Integrated Circuits. June 2002,15(6):571–587
[193] H. Mehta, R. M. Owens, M. J. Irwin. Energy characterization based on clustering.Proceedings of 33rd Design Automation Conference, DAC’96. June 1996:702–707
[194] W. Ye, N. Vijaykrishnan, M. Kandemir, M. J. Irwin. The design and use of sim-plePower: a cycle-accurate energy estimation tool. Proceedings of 37th DesignAutomation Conference, DAC’00. 2000:340–345
[195] N. Bansal, K. Lahiri, A. Raqhunathan, S. T. Chakradhar. Power monitors: aframework for system-level power estimation using heterogeneous power models.Proceedings of 18th International Conference on VLSI Design. 2005:579–585
[196] N. H. W. Weste, K. Eshraghian. Principles of CMOS VLSI design, A systemsperspective. Addison Wesley, 1993
[197] K. Czamecki, S. Helsen. Feature-based Survery of Model Transformation Ap-proaches. IBM Systems Journal. 2006, 45(3)
[198] OMG. MOF 2.0 Query/Views/Transformation RFP. OMG Document ad. 2002
[199] OMG. MOF 2.0. Query/Views/Transformation Specification Version 10. 2008
[200] OMG. OMG Unified Modeling Language Infrastructure V2.12, 2007
[201] OMG. UML Profile for System on Chip (SOC) Specification. version 101. 2006
[202] Y. Wang, X. Zhou, B. Zhou, L. Liang and C. Peng. A MDA based SoC ModelingApproach using UML and SystemC. Proc of CIT. 2006
[203] C. Xi, L. Jianhua, Z. Zucheng and S. Yaohui. Modeling SystemC Design in UMLand Automatic Code Generation. Proc of ASP-DAC. 2005
[204] B. A. Correa, J. F. Eusse, D. Munera, et al. Hign Level System-on-Chip Designusing UML and SystemC. Proc of Electronic, Robotics and Automotive MechanicsConference (CERMA). 2007
[205] E. Riccobene, P. Scandurra, S. Rosti, A. Bocchio. A SoC Design MethodologyInvolving a UML 2.0 Profile for SystemC. Design Automation and Test Europe(DATE). 2005
[206] E. Riccobene, P. Scandurra, S. Rosti, A. Bocchio. A UML 2.0 Profile for SystemC:Toward High-level SoC Design. EMSOFT’05. 2005
[207] W. Mueller, S. Rosti, A. Bocchio, et al. UML for ESL Design-Basic Principles, Tools,and Applications. Proc of IEEE/ACM International Conference on Computer AidedDesign (ICCAD). 2006
[208] F. Coyle, M. Thomton. Form UML to HDL: A Model Driven Architecture Ap-proach to Hardware-Software Co-Design. Information Systems: New GenerationsConference (ISNG). 2005
[209] L. Li, F. Coyle, M. Thomton. UML to SystemVerilog Synthesis For Embedded Sys-tem Models with Support for Assertion Generation. Proc of Forum on Specificationand Design Languages (FDL). 2007
[210] SysML, http://www.sysml.org/
[211] F. Jouault, F. Alliaire. J. Bezivin, et al. ATL: A QVT-like Transformation Lan-guage. Proc of the 21st ACM Symposium on Object-oriented Programming SystemsLanguages and Applicaitons (SIGPLAN). 2006
[212] ModelMorf. http://www.tcs-trddc.com/ModelMorf/index.htm
[213] MedianQVT. http://projects.ikv.de/qvt/
[214] SmartQVT. http://smartqvt.elibel.tm.fr/
[215] Zhanqi Cui, Linzhang Wang, Xuandong Li. Modeling and Integrating Aspects withUML Activity Diagrams. SAC’09. 2009
[216] J. Whittle, P. Jayaraman. MATA: A Tool for Aspect-Oriented Modeling Based onGraph Transformation. MoDeLS 2007 Workshops. 2007:16–27
[217] D. Stein, S. Hanenberg, R. Unland. An UML-based Aspect-Oriented Design NotainFor AspectJ. AOSD’02. 2002
[218] J. U. Junior, V. V. de Camargo, C. V. Flach. UML-AOF: A Profile for ModelingAspect-Oriented Frameworks. AOM’09. 2009
[219] J. Evermann. A Meta-Level Specification and Profile for AspectJ in UML. AOM’07.2007
[220] J. Evermann. A Meta-Level Specification and Profile for AspectJ in UML. Journalof Object Technology. 2006, 6(7):27–49