针对GSTE的电路模型抽取
|
摘要
集成电路产业已经成为国民经济的朝阳产业,每年在全球产生数千亿美元的生产价值。从世界上第一个块集成电路芯片诞生至今,集成电路芯片的面积越来越小,单位面积集成的电路元器件数越来越多,如今一块芯片上已集成了数亿个门。随成电路集成度的增高,人们发现制约集成电路发展的一个重要因素是芯片设计与芯片制造的严重脱节。阻碍芯片设计发展的一个重要因素便是如何验证芯片设计的正确性。传统的模拟验证已经难以满足芯片设计的要求。而形式化验证方法因其是基于严格的数学方法来确保芯片设计的正确性,因此已经在芯片设计领域受到越来越多的重视。实现形式化验证的理论并形成相关验证工具软件的一个关键点就是电路模型的抽取和仿真。
本论文首先研究和学习了形式化验证的相关理论知识,包括该理论的主要分支,发展情况。并对目前形式化验证领域的主流算法GSTE进行了深入学习和研究,并对比了该算法与传统算法的不同。
其次对当前学术界以及工业界的一些常用工具SMV,VIS,FORTE等进行研究和源码剖析。并对当前电路设计语言VERILOG进行学习研究后,在基于以上工具所提供的电路描述语言的基础上简化VERILOG。设计了一套针对GSTE算法的验证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并对电路模型进行抽取。最后设计了系统的框架以及技术路线。
然后,研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言描述的电路抽取为适合采用GSTE算法来进行验证的电路模型,使得GSTE算法能够应用在实际的电路设计领域。使用编译工具LEX,YACC实现了本软件的电路输入前端,在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后,交由后端GSTE验证算法进行电路模型的形式化验证。本论文在对数字电路仿真进行了相关研究后,基于抽取的电路模型,实现对该电路模型的仿真,能够得到相应的波形图,从来能方便的对GSTE算法进行演示。
最后对全文进行了系统全面的概括总结,并指出了本文所设计工具的不足以及下一步的改进方向,并展望了形式化验证算法在电路设计领域的良好应用前景。
IC industry has become a sunrise industry of the national economy annually. It produce several hundred billion dollars in the global value of production. A block from the world's first integrated circuit chip, since its inception, the area of integrated circuit chips getting smaller and smaller. Integrated circuits has per unit area of increasing number of components, and now a chip has been integrated with hundreds of millions of gates. With the increased integration into the circuit, it was discovered that constrained the development of an important factor in IC chip design and chip manufacturing is a serious disconnect. Hinder the development of chip design is an important factor in how to verify the correctness of chip design. Traditional analog chip design verification has been difficult to meet the requirements of the formal verification method is based on its rigorous mathematical methods to ensure the correctness of chip design, so the field of chip design has been more and more attention. To achieve the formation of formal verification of the theory and tools related to validation is a key point is the circuit model extraction and simulation.
In this paper, first of all research and study of the formal verification of the relevant theoretical knowledge, including the theory of the main branch of development. And is currently the mainstream of the field of formal verification algorithms GSTE conducted in-depth study and research, and compared the algorithm with the traditional algorithms different.
Second, pairs of digital circuits and digital circuit design method related to a summary study of digital circuit design front-end circuit description and digital circuits formal verification algorithm point. Analysis of how the circuit model expressed in the computer memory, data structure, and studied how to use language to describe a circuit extraction algorithm suitable for use GSTE to verify the circuit model, allowing GSTE algorithm can be applied to practical circuit design zone
Thirdly, in the current academic and industrial circles some common tools SMV, VIS, FORTE and other research and source analysis, and the current circuit design language VERILOG learning studies, in view of the above tools offered by the circuit description language summarized on the basis of grammatical simplification VERILOG produced a set of algorithms for verification tools GSTE circuit description language syntax and semantics, so that it could easily describe the circuit and the circuit model extraction. Using the compilation tools LEX, YACC implements the circuit of this software enter the front end, in the syntax tree generated from semantic reasoning, the circuit model of the data structure binary decision diagram by the back-end authentication algorithm GSTE Formal Verification of the circuit model. In order to visual observations of the circuit description language describes the circuit behavior, this paper in the digital circuit simulation carried out relevant studies, based on the extraction of the circuit model, realization of the circuit model of the simulation, the corresponding waveforms can be, never be able to convenient presentation of the GSTE algorithm.
Finally, the paper conducted a systematic and comprehensive summary of conclusion and pointed out the lack of design tools in this article, as well as the next step to improve the direction and looks forward to the formal verification algorithm in the field of circuit design a good application prospects.
本论文首先研究和学习了形式化验证的相关理论知识,包括该理论的主要分支,发展情况。并对目前形式化验证领域的主流算法GSTE进行了深入学习和研究,并对比了该算法与传统算法的不同。
其次对当前学术界以及工业界的一些常用工具SMV,VIS,FORTE等进行研究和源码剖析。并对当前电路设计语言VERILOG进行学习研究后,在基于以上工具所提供的电路描述语言的基础上简化VERILOG。设计了一套针对GSTE算法的验证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并对电路模型进行抽取。最后设计了系统的框架以及技术路线。
然后,研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言描述的电路抽取为适合采用GSTE算法来进行验证的电路模型,使得GSTE算法能够应用在实际的电路设计领域。使用编译工具LEX,YACC实现了本软件的电路输入前端,在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后,交由后端GSTE验证算法进行电路模型的形式化验证。本论文在对数字电路仿真进行了相关研究后,基于抽取的电路模型,实现对该电路模型的仿真,能够得到相应的波形图,从来能方便的对GSTE算法进行演示。
最后对全文进行了系统全面的概括总结,并指出了本文所设计工具的不足以及下一步的改进方向,并展望了形式化验证算法在电路设计领域的良好应用前景。
IC industry has become a sunrise industry of the national economy annually. It produce several hundred billion dollars in the global value of production. A block from the world's first integrated circuit chip, since its inception, the area of integrated circuit chips getting smaller and smaller. Integrated circuits has per unit area of increasing number of components, and now a chip has been integrated with hundreds of millions of gates. With the increased integration into the circuit, it was discovered that constrained the development of an important factor in IC chip design and chip manufacturing is a serious disconnect. Hinder the development of chip design is an important factor in how to verify the correctness of chip design. Traditional analog chip design verification has been difficult to meet the requirements of the formal verification method is based on its rigorous mathematical methods to ensure the correctness of chip design, so the field of chip design has been more and more attention. To achieve the formation of formal verification of the theory and tools related to validation is a key point is the circuit model extraction and simulation.
In this paper, first of all research and study of the formal verification of the relevant theoretical knowledge, including the theory of the main branch of development. And is currently the mainstream of the field of formal verification algorithms GSTE conducted in-depth study and research, and compared the algorithm with the traditional algorithms different.
Second, pairs of digital circuits and digital circuit design method related to a summary study of digital circuit design front-end circuit description and digital circuits formal verification algorithm point. Analysis of how the circuit model expressed in the computer memory, data structure, and studied how to use language to describe a circuit extraction algorithm suitable for use GSTE to verify the circuit model, allowing GSTE algorithm can be applied to practical circuit design zone
Thirdly, in the current academic and industrial circles some common tools SMV, VIS, FORTE and other research and source analysis, and the current circuit design language VERILOG learning studies, in view of the above tools offered by the circuit description language summarized on the basis of grammatical simplification VERILOG produced a set of algorithms for verification tools GSTE circuit description language syntax and semantics, so that it could easily describe the circuit and the circuit model extraction. Using the compilation tools LEX, YACC implements the circuit of this software enter the front end, in the syntax tree generated from semantic reasoning, the circuit model of the data structure binary decision diagram by the back-end authentication algorithm GSTE Formal Verification of the circuit model. In order to visual observations of the circuit description language describes the circuit behavior, this paper in the digital circuit simulation carried out relevant studies, based on the extraction of the circuit model, realization of the circuit model of the simulation, the corresponding waveforms can be, never be able to convenient presentation of the GSTE algorithm.
Finally, the paper conducted a systematic and comprehensive summary of conclusion and pointed out the lack of design tools in this article, as well as the next step to improve the direction and looks forward to the formal verification algorithm in the field of circuit design a good application prospects.
引文
[1] Michael Huth .Logic in Compute Science Modelling and Reasoning about Systems,second Edtion. Cambridge University Press,2004
[2] The Gste group .EXLIF Extended Logic Interchange Format Syntax desribe for forte.Intel Corporation 2003
[3] Sarfraz Khurshid, Corina S. P?as?areanu, and Willem Visser. Generalized Symbolic Execution for Model Checking and Testing. . IEEE Spectrum, 1996 53-54
[4] Scott Hazelhurst and Carl-Johan H. Seger. A Simple Theorem Prover Based on Symbolic Trajectory Evaluation and BDD’s . IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 14, NO. 4, APRIL 1995
[5] M. C. McFarland, Formal verification of sequential hardware: A tutorial, IEEE Trans. Computer-Aided Design, vol.12, no.5, 1993.
[6] E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach, in Proc. 10th ACM Symp. Principles Programming Languages, New York, 1983, ACM, pp. 117-126.
[7] 0. Coudert, J. C. Madre, and C. Berthet, Verifying temporal properties of sequential machines without building their state diagram, in CAV'90: Proc. 2nd Int. Workshop Computer-Aided Verijicarion, June 1990, Lecture Notes in Computer Science 531.
[8] M. Pandey, R. Bryant. Exploiting Symmetry when Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1999, 18(7):918–935
[9]兰姆.硬件设计验证:基于模拟与验证的方法.机械工业出版社.2007年
[10] Edmund M. Clarke Jr. Orna Grumberg Doron A. Peled.Model Checking. The MIT Press.1999
[11] Matthew Dwyer.模型检测软件.北大出版社.2005
[12]徐琳琳.模型检测器前端系统的设计与实现: [硕士学位论文].成都:电子科技大学, 2007
[13]安培尔.金斯博格.现代编译原理.人民邮电出版社.2006
[14] Alfred V. Aho ,Monica S.Lam ,Ravi Sethi,Jeffrey D. Ullman.编译原理.机械工业出版社2008年
[15] Carl-Johan H. Seger, Robert B. Jones. An Industrially Effective Environment for FormalHardware Verification. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 24, NO. 9, SEPTEMBER 2005
[16] S. Rajan, N. Shankar, and M. Srivas, An integration of model checking and automated proof checking,in Proc. 8th Int. Conf. Computer Aided Verification (CAV), Jul. 31–Aug. 3, 1996, R. Alur and T. Henzinger, Eds. New York: Springer-Verlag, 1996, vol. 1102, pp. 411–414.
[17] Technical Publications and Training, Intel Corporation, Forte/FL User Guide: Version 1.0. Santa Clara, CA: Design Technol., Intel Corp.2003, release for academic, non-commercial use.
[18] M. Pandey, R. Raimi, R. E. Bryant, and M. S. Abadir, Formal verification of content addressable memories using symbolic trajectory evaluation, in ACM/IEEE Design Automation Conf. (DAC). Anaheim, CA: ACM Press, Jun. 1997, pp. 167–172.
[19] RAUL CAMPOSANO.WOLFGANG ROSENSTIEL.Synthesizing Circuits From Behavioral Descriptions. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN, VOL.8, NO.2.FEBRUARY 1989
[20] Edward Smith. A logic for GSTE. In Baumgartner and Sheeran [BS07],pages 119–126.2004
[21] Jin Yang and Carl-Johan H. Seger. Generalized symbolic trajectory evaluation.Technical report, Intel, 2000.
[22] Jin Yang and Carl-Johan H. Seger. Introduction to generalized symbolic trajectory evaluation. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 11(3):345–353, June 2003.
[23] Guowu Yang, Jin Yang, William N. N. Hung, et al. Implication of assertion graphs in GSTE. ASPDAC, 2005, 1060-1063
[24] Guowu Yang, Jin Yang, Xiaoyu Song, et al. Maximal Models of Assertion Graph in GSTE. TAMC, 2006, 684-693
[25]吕关锋,苏开乐,林瀚,骆翔宇,陈清亮,岳伟亚.基于BDD的图表示及其算法.中山大学学报(自然科学版本)第45卷第一期.2006年.
[26] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. KAP.1993
[27] Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey,1994.
[28]王毓银.数字电路逻辑设计.高等教育出版社.2002
[29]夏宇闻.VERILOG数字系统设计教程.北京航空航天大学出版社.2004
[30] S. Reddy, W. Kunz, and D. Pradhan. Novel verification framework combining structural and OBDD methods in a synthesis environment. In Proc. Design Automation Conference, pages414–419, 1995.
[31] R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, Boston,1988.
[32] C. Kern and M. Greenstreet: Formal Verification in Hardware Design: A Survey; ACM Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193.
[33] R. Hojati, R. K. Brayton. Automatic Datapath Abstraction in Hardware Systems. Computer Aided Verification, LNCS 939, Springer Verlag, 1995, pp. 98-113.
[34] B. Bentley, High level validation of next-generation microprocessors, IEEE International Workshop on High Level Design Validation and Test, 2002.
[35] J. Yang and A. Goel,“GSTE through a case study”, International Conference on Computer-Aided Design ICCAD, 2002.
[36] J. Yang and C.-J. H. Seger,“Generalized Symbolic Trajectory Evaluation: Abstraction in action”, Fourth International Symposium on Formal Methods in Computer-Aided Design (FMCAD), 2002.
[37] N. Narasimhan and R. Kaivola, Verification of Pentium?4 Multiplier with Symbolic Simulation & Theorem Proving, 2001.
[38] John R. Levine,Tony Mason,Doug Brown. LEX和YACC(第二版).OREILLY.2004年
[39] E. A. Emerson, Temporal and modal logic,in Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Amsterdam, The Netherlands: Elsevier, vol.B, pp.995–1072.
[40] J. V. Guttag, J. J. Horning, S. J. Garland, K. D. Jones, A. Modet,and J. M. Wing, Larch: Languages and Tools for Formal Specification.New York: Springer-Verlag, 1993.
[41] M. Kwiatkowska, G. Norman, R. Segala, and J. Sprotson, Automatasic verification of real-time systems with discrete probability distributions,Theor. Comput. Sci., vol. 286, no. 1–2, 2002.
[42] R. De Nicola and F. Vaandrager, Three logics for branching bisimulation,J. Assoc. Comput. Mach., vol. 42, no. 2, pp. 458–487, 1995.
[43] X. Nicolin, J. Sifakis, and S.Yovine, Compiling real-time specifications into extended automata,IEEE Trans. Software Eng. (Special Issue on Real-Time Systems), vol. 18, pp. 794–804, Sept. 1992.
[44] S. A. Seshia and R. E. Bryant,“Unbounded, fully symbolic model checking of timed automata using Boolean methods,”in Lecture Notes in Computer Science, Computer-Aided Verification, 2003, vol.2725, pp. 154–166.
[45] H. Miller and S. Katz,“Saving space by fully exploiting invisible transitions,”Formal Methods Syst. Design, vol. 14, pp. 311–332,1999.
[46] S. Yamane,“Formal specification and verification method for hard real-time s7ystems,”IPSJ J., vol. 42, no. 6, 2001.
[47] D. W. Currie, A. J. Hu, S. Rajan, M. Fujita,Automatic Formal Verification of DSP Software, Proc. Design Automation Conference, pp.130--135, Jun. 2000.
[48] L. Semeria, A. Seawright, R. Mehra, D. Ng, A. Ekanayake, B. Pangrle,“C-Based RTL Methodology for Designing and Verifying a Multi-Threaded Processor'', Proc. Design Automation Conference, pp.123--128, 2002
[49]张秀秀.数字并发行为的STE验证方法: [硕士学位论文].兰州:兰州大学, 2007
[50] E. M. Clarke and D. Kroening,“Hardware Verification Using ANSI-C Programs as a Reference'', Proc. Asia South Pacific Design Automation Conference, pp.308--311, 2003.
[2] The Gste group .EXLIF Extended Logic Interchange Format Syntax desribe for forte.Intel Corporation 2003
[3] Sarfraz Khurshid, Corina S. P?as?areanu, and Willem Visser. Generalized Symbolic Execution for Model Checking and Testing. . IEEE Spectrum, 1996 53-54
[4] Scott Hazelhurst and Carl-Johan H. Seger. A Simple Theorem Prover Based on Symbolic Trajectory Evaluation and BDD’s . IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 14, NO. 4, APRIL 1995
[5] M. C. McFarland, Formal verification of sequential hardware: A tutorial, IEEE Trans. Computer-Aided Design, vol.12, no.5, 1993.
[6] E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach, in Proc. 10th ACM Symp. Principles Programming Languages, New York, 1983, ACM, pp. 117-126.
[7] 0. Coudert, J. C. Madre, and C. Berthet, Verifying temporal properties of sequential machines without building their state diagram, in CAV'90: Proc. 2nd Int. Workshop Computer-Aided Verijicarion, June 1990, Lecture Notes in Computer Science 531.
[8] M. Pandey, R. Bryant. Exploiting Symmetry when Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1999, 18(7):918–935
[9]兰姆.硬件设计验证:基于模拟与验证的方法.机械工业出版社.2007年
[10] Edmund M. Clarke Jr. Orna Grumberg Doron A. Peled.Model Checking. The MIT Press.1999
[11] Matthew Dwyer.模型检测软件.北大出版社.2005
[12]徐琳琳.模型检测器前端系统的设计与实现: [硕士学位论文].成都:电子科技大学, 2007
[13]安培尔.金斯博格.现代编译原理.人民邮电出版社.2006
[14] Alfred V. Aho ,Monica S.Lam ,Ravi Sethi,Jeffrey D. Ullman.编译原理.机械工业出版社2008年
[15] Carl-Johan H. Seger, Robert B. Jones. An Industrially Effective Environment for FormalHardware Verification. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 24, NO. 9, SEPTEMBER 2005
[16] S. Rajan, N. Shankar, and M. Srivas, An integration of model checking and automated proof checking,in Proc. 8th Int. Conf. Computer Aided Verification (CAV), Jul. 31–Aug. 3, 1996, R. Alur and T. Henzinger, Eds. New York: Springer-Verlag, 1996, vol. 1102, pp. 411–414.
[17] Technical Publications and Training, Intel Corporation, Forte/FL User Guide: Version 1.0. Santa Clara, CA: Design Technol., Intel Corp.2003, release for academic, non-commercial use.
[18] M. Pandey, R. Raimi, R. E. Bryant, and M. S. Abadir, Formal verification of content addressable memories using symbolic trajectory evaluation, in ACM/IEEE Design Automation Conf. (DAC). Anaheim, CA: ACM Press, Jun. 1997, pp. 167–172.
[19] RAUL CAMPOSANO.WOLFGANG ROSENSTIEL.Synthesizing Circuits From Behavioral Descriptions. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN, VOL.8, NO.2.FEBRUARY 1989
[20] Edward Smith. A logic for GSTE. In Baumgartner and Sheeran [BS07],pages 119–126.2004
[21] Jin Yang and Carl-Johan H. Seger. Generalized symbolic trajectory evaluation.Technical report, Intel, 2000.
[22] Jin Yang and Carl-Johan H. Seger. Introduction to generalized symbolic trajectory evaluation. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 11(3):345–353, June 2003.
[23] Guowu Yang, Jin Yang, William N. N. Hung, et al. Implication of assertion graphs in GSTE. ASPDAC, 2005, 1060-1063
[24] Guowu Yang, Jin Yang, Xiaoyu Song, et al. Maximal Models of Assertion Graph in GSTE. TAMC, 2006, 684-693
[25]吕关锋,苏开乐,林瀚,骆翔宇,陈清亮,岳伟亚.基于BDD的图表示及其算法.中山大学学报(自然科学版本)第45卷第一期.2006年.
[26] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. KAP.1993
[27] Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey,1994.
[28]王毓银.数字电路逻辑设计.高等教育出版社.2002
[29]夏宇闻.VERILOG数字系统设计教程.北京航空航天大学出版社.2004
[30] S. Reddy, W. Kunz, and D. Pradhan. Novel verification framework combining structural and OBDD methods in a synthesis environment. In Proc. Design Automation Conference, pages414–419, 1995.
[31] R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, Boston,1988.
[32] C. Kern and M. Greenstreet: Formal Verification in Hardware Design: A Survey; ACM Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193.
[33] R. Hojati, R. K. Brayton. Automatic Datapath Abstraction in Hardware Systems. Computer Aided Verification, LNCS 939, Springer Verlag, 1995, pp. 98-113.
[34] B. Bentley, High level validation of next-generation microprocessors, IEEE International Workshop on High Level Design Validation and Test, 2002.
[35] J. Yang and A. Goel,“GSTE through a case study”, International Conference on Computer-Aided Design ICCAD, 2002.
[36] J. Yang and C.-J. H. Seger,“Generalized Symbolic Trajectory Evaluation: Abstraction in action”, Fourth International Symposium on Formal Methods in Computer-Aided Design (FMCAD), 2002.
[37] N. Narasimhan and R. Kaivola, Verification of Pentium?4 Multiplier with Symbolic Simulation & Theorem Proving, 2001.
[38] John R. Levine,Tony Mason,Doug Brown. LEX和YACC(第二版).OREILLY.2004年
[39] E. A. Emerson, Temporal and modal logic,in Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Amsterdam, The Netherlands: Elsevier, vol.B, pp.995–1072.
[40] J. V. Guttag, J. J. Horning, S. J. Garland, K. D. Jones, A. Modet,and J. M. Wing, Larch: Languages and Tools for Formal Specification.New York: Springer-Verlag, 1993.
[41] M. Kwiatkowska, G. Norman, R. Segala, and J. Sprotson, Automatasic verification of real-time systems with discrete probability distributions,Theor. Comput. Sci., vol. 286, no. 1–2, 2002.
[42] R. De Nicola and F. Vaandrager, Three logics for branching bisimulation,J. Assoc. Comput. Mach., vol. 42, no. 2, pp. 458–487, 1995.
[43] X. Nicolin, J. Sifakis, and S.Yovine, Compiling real-time specifications into extended automata,IEEE Trans. Software Eng. (Special Issue on Real-Time Systems), vol. 18, pp. 794–804, Sept. 1992.
[44] S. A. Seshia and R. E. Bryant,“Unbounded, fully symbolic model checking of timed automata using Boolean methods,”in Lecture Notes in Computer Science, Computer-Aided Verification, 2003, vol.2725, pp. 154–166.
[45] H. Miller and S. Katz,“Saving space by fully exploiting invisible transitions,”Formal Methods Syst. Design, vol. 14, pp. 311–332,1999.
[46] S. Yamane,“Formal specification and verification method for hard real-time s7ystems,”IPSJ J., vol. 42, no. 6, 2001.
[47] D. W. Currie, A. J. Hu, S. Rajan, M. Fujita,Automatic Formal Verification of DSP Software, Proc. Design Automation Conference, pp.130--135, Jun. 2000.
[48] L. Semeria, A. Seawright, R. Mehra, D. Ng, A. Ekanayake, B. Pangrle,“C-Based RTL Methodology for Designing and Verifying a Multi-Threaded Processor'', Proc. Design Automation Conference, pp.123--128, 2002
[49]张秀秀.数字并发行为的STE验证方法: [硕士学位论文].兰州:兰州大学, 2007
[50] E. M. Clarke and D. Kroening,“Hardware Verification Using ANSI-C Programs as a Reference'', Proc. Asia South Pacific Design Automation Conference, pp.308--311, 2003.