基于仿真的系统芯片功能验证技术研究
|
摘要
验证已成为系统芯片(SoC)设计所面临的重大挑战,形式验证所能验证的电路规模远远不能满足设计需要,基于仿真的验证方法一直占统治地位。课题主要研究基于仿真的SoC验证技术。
首先,提出并实现一种向量自动生成算法——“基于遗传算法和覆盖率驱动的Verilog RTL功能验证向量自动生成算法”。反馈覆盖率信息构建闭环系统,采用遗传算法根据覆盖率模型分析覆盖率信息自动生成验证向量。然后,提出并实现一种故障模型——“Verilog RTL域故障模型”。域故障模型准确全面地反映导致域错误的原因,域覆盖率衡量验证工作的充分性,域测试点选择策略快速生成域测试所需测试点。接着,实现基于C参考模型和SVA(System Verilog Assertion)的功能检查方法。最后,提出并实现一种SoC芯片级快速验证方法——“基于C建模的SoC芯片级验证方法”。针对ARM处理器构建AMBA周期精确模型,总线设备周期精确模型可由Verilog RTL生成,快速进行周期精确的芯片级验证。
以Garfield系列系统芯片1验证为平台。模块级验证过程中采用基于遗传算法和覆盖率驱动的验证向量自动生成算法生成验证向量,数据表明,相对手写和随机生成验证向量方法本方法能减少验证向量开发时间,并达到更高的覆盖率;采用域覆盖率衡量模块级验证工作的充分型,结果表明这种覆盖率相对于行覆盖率和路径覆盖率更能准确衡量验证工作的充分性和发现验证漏洞;模块级验证过程中采用C参考模型与SVA检查DUV(Design Under Verification)的响应是否和功能定义一致,结果表明该方法能减少调试时间,提高验证质量。模块验证达到所需要的域和功能覆盖率后,SoC验证重点转向芯片级(Chip-Level)验证,采用基于C建模的SoC芯片级验证方法验证整个芯片功能,数据结果表明该方法比传统的RTL仿真速度提高了20倍以上。
Verification has been one of the most important challenges to SoC design. Despite recent advances in formal verification, it can not meet the requirement of design. Simulation based verification method continues to be the workhorse. This dissertation addresses the issues of simulation based verification.
Firstly, proposed and implemented coverage driven and GA(Genetic Algorithm) based Verilog RTL verification vector auto generation algorithm. Coverage information is fed back and form a closed system, the GA analyses dynamically the coverage information and selects the vector with higher fitness to generate the next generation vector. Secondly, proposed and implemented Domain fault model, coverage metrics and testing points selecting strategies. Domain fault model correctly reflects the reason causing domain errors, Domain coverage metrics measure the quality of the verification approach, and test point selecting strategies generate required points for domain testing. Thirdly, implemented a C reference model and SVA(System Verilog Assertion) based function checking method. Lastly, proposed and implemented a C based SoC chip level verification method, in which a cycle accurate AMBA functional model is connected to ARM ISS and the devices on bus are translated from Verilog RTL.
Preceding methods are used in Garfield series SoC2 verification approach. When doing block level verification, GA based Verilog RTL verification vector auto generation algorithm is used to generate the verification vector, results show that the algorithm can generate vector more quickly and reach higher coverage than directed and random method. Domain method is adopted to measure block level verification quality, domain coverage metrics can find more verification holes, compared with line and path coverage metrics. C reference model and SVA based checking method are also used in the block verification approach, results show that this method can reduce greatly verification time and human resource, locate the design error quickly. When block level verification reaches the required domain and functional coverage, the C based SoC chip level verification method is used to verification whole chip, results show that whole chip can be verified at speed of 20 times of Verilog RTL simulation.
首先,提出并实现一种向量自动生成算法——“基于遗传算法和覆盖率驱动的Verilog RTL功能验证向量自动生成算法”。反馈覆盖率信息构建闭环系统,采用遗传算法根据覆盖率模型分析覆盖率信息自动生成验证向量。然后,提出并实现一种故障模型——“Verilog RTL域故障模型”。域故障模型准确全面地反映导致域错误的原因,域覆盖率衡量验证工作的充分性,域测试点选择策略快速生成域测试所需测试点。接着,实现基于C参考模型和SVA(System Verilog Assertion)的功能检查方法。最后,提出并实现一种SoC芯片级快速验证方法——“基于C建模的SoC芯片级验证方法”。针对ARM处理器构建AMBA周期精确模型,总线设备周期精确模型可由Verilog RTL生成,快速进行周期精确的芯片级验证。
以Garfield系列系统芯片1验证为平台。模块级验证过程中采用基于遗传算法和覆盖率驱动的验证向量自动生成算法生成验证向量,数据表明,相对手写和随机生成验证向量方法本方法能减少验证向量开发时间,并达到更高的覆盖率;采用域覆盖率衡量模块级验证工作的充分型,结果表明这种覆盖率相对于行覆盖率和路径覆盖率更能准确衡量验证工作的充分性和发现验证漏洞;模块级验证过程中采用C参考模型与SVA检查DUV(Design Under Verification)的响应是否和功能定义一致,结果表明该方法能减少调试时间,提高验证质量。模块验证达到所需要的域和功能覆盖率后,SoC验证重点转向芯片级(Chip-Level)验证,采用基于C建模的SoC芯片级验证方法验证整个芯片功能,数据结果表明该方法比传统的RTL仿真速度提高了20倍以上。
Verification has been one of the most important challenges to SoC design. Despite recent advances in formal verification, it can not meet the requirement of design. Simulation based verification method continues to be the workhorse. This dissertation addresses the issues of simulation based verification.
Firstly, proposed and implemented coverage driven and GA(Genetic Algorithm) based Verilog RTL verification vector auto generation algorithm. Coverage information is fed back and form a closed system, the GA analyses dynamically the coverage information and selects the vector with higher fitness to generate the next generation vector. Secondly, proposed and implemented Domain fault model, coverage metrics and testing points selecting strategies. Domain fault model correctly reflects the reason causing domain errors, Domain coverage metrics measure the quality of the verification approach, and test point selecting strategies generate required points for domain testing. Thirdly, implemented a C reference model and SVA(System Verilog Assertion) based function checking method. Lastly, proposed and implemented a C based SoC chip level verification method, in which a cycle accurate AMBA functional model is connected to ARM ISS and the devices on bus are translated from Verilog RTL.
Preceding methods are used in Garfield series SoC2 verification approach. When doing block level verification, GA based Verilog RTL verification vector auto generation algorithm is used to generate the verification vector, results show that the algorithm can generate vector more quickly and reach higher coverage than directed and random method. Domain method is adopted to measure block level verification quality, domain coverage metrics can find more verification holes, compared with line and path coverage metrics. C reference model and SVA based checking method are also used in the block verification approach, results show that this method can reduce greatly verification time and human resource, locate the design error quickly. When block level verification reaches the required domain and functional coverage, the C based SoC chip level verification method is used to verification whole chip, results show that whole chip can be verified at speed of 20 times of Verilog RTL simulation.
引文
[1] ITRS, ITRS Design DTWG[C]. INTERNATIONAL TECHNOLOGY ROADMAP FOR SEMICONDUCTORS'99 Conference. November,1999. 7.
[2] ITRS, INTERNATIONAL TECHNOLOGY ROADMAP FOR SEMICONDUCTORS 2005 Edition Design[EB/OL]. http://www.itrs.net/Common/2005ITRS/Home2005.htm. 2005. 21-30.
[3] Bergeron Janick, Writing Testbenchs: Functional Verification of HDL Models[M]. January 2000: Kluwer Academic Publishers. 1-19.
[4] Bailey Brian, The Need for a Scalable Verification Methodology to Overcome the Limitations of Current Verification Approaches[EB/OL]. http://www.mentor.com/techpapers/fulfillment/upload/mentorpaper_22780.pdf. August 1, 2004.
[5] Clarke E.M, Automatic verification of finite-state concurrent systems[C]. Logic in Computer Science, 1994, LICS '94. Jul 1994. 126-132.
[6] Jayanta Bhadra, Abstraction techniques for verification of digital designs[D]:[博士学位论文], in Engineering, Electronics and Electrical. 2001, The University of Texas at Austin.
[7] Burch J.R., symbolic model checking: 1020 states and beyond[C]. Logic in Computer Science, 1990, LICS '90. 1990. 428-439.
[8] Clarke E.M,E.A. Emerson and A.P. Sittla, Automatic verification of finite-state concurrent systems using temporal logic specification[J]. ACM Trans. on Program Language Systems, 1986. 8: p. 244-263.
[9] Pnueli A. Siegel M., A temporal logic of concurrent programs[J]. Theoretical Computer Science, 1981. 13: p. 45-60.
[10] Bryant R.E., Graph based algorithms for Boolean function manipulation[J]. IEEE Transactions on Computers, 1986. 35(8): p. 677-691.
[11] VISGroup, VIS User's Manual[EB/OL]. http://vlsi.colorado.edu/%7Evis/doc/VisUser/vis_user/vis_user.html.
[12] Martin Davis and Hilary Putnam, A computing procedure for quantification theory[J]. Journal of The Assocation for Computing Machinery, 1960. 7: p. 201-215.
[13] Matthew H. Moskewicz Conor F. Madigan, Ying Zhao et al, Chaff: Engineering an Efficient STA Solver[C]. Proceedings of the 38th Design Automation Conference. June 2001. 530-535.
[14] Prasad Mukul Ranjan, Propositional satisfiability algorithms in EDA applications[D]:[博士论文], in Engineering, Electronics and Electrical.;Computer Science. 2001, University of California, Berkeley.
[15] Marques-Silva J. and Guerra Silva, Solving satisfiability in combinational circuits[J]. Design & Test of Computers, IEEE. 20(4): p. 16-21.
[16] Wang Dong, SAT based abstraction refinement for hardware verification[D]:[博士学位论文], in Engineering, Electronics and Electrical. 2003, Carnegie Mellon University.
[17] Lyerand Parthasarathy G.M.K. and Cheng K.T., Safety property verification using sequential SAT and bounded model checking[J]. Design & Test of Computers, IEEE,2004. 21(2): p. 132-143.
[18] Marek Kai Richter,Marek Jersak and Rolf Ernst, A Formal Approach to MpSoC Performance Verification[J]. IEEE Computer, April 2003. 36(4): p. 60-67.
[19] Choi Hoon, Byeongwhee Yun, Yuntae Lee, et al, Model checking of S3C2400X industrial embedded SOC product[C]. Design Automation Conference,2001. 611-616.
[20] Clarke E.M. and J. Wing, Formal methods: state of the art and future directions[J]. ACM Comuting Surveys. 28(4): p. 626-643.
[21] Gordon M. J. C., A proof generating system for higher order logic[J]. Current Trends in Hardware Verification and Automated Theorem Proving, 1989: p. 74-128.
[22] Owre S.,J. M. Rushby and N. Shankar, PVS: A prototype verification system[C]. 11th International Conference on Automated Deduction (CADE). 1992. 748-752.
[23] Brock Bishop,Matt Kaufmann and Moore Strother, ACL2 Theorems about Commercial Microprocessors[C]. First international conference on formal methods in computer-aided design. 1996.
[24] Moore J Strother,Tom Lynch and Matt Kaufmann, A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm[J]. IEEE Transactions on Computers, 1998. 47(9): p. 913-926.
[25] Paul Miner and Leathrum James, Verification of IEEE Compliant Subtractive Division Algorithms[C]. First international conference on formal methods in computer-aided design. 1996. 111-122.
[26] Herbstritt M.,Kmieciak T. and Becker B., On the impact of structural circuit partitioning on SAT-based combinational circuit verification[C]. Microprocessor Test and Verification, 2004. Fifth International Workshop on. 2004. 50-55.
[27] Reda S. and Salem A., Combinational Equivalence Checking using Boolean Satisfiability and Binary Decision Diagrams[C]. Design, Automation and Test in Europe. 2001.
[28] Davis M., Logeman G., Loveland D., A machine program for the theorm proving[J]. Communication. ACM, July 1962. 5: p. 394-397.
[29] Kuehlmann A. Paruthi V., Krohm F., et al, Robust Boolean reasoning for equivalence checking and functional property verification[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, Dec. 2002. 21(12): p. 1377-1394.
[30] Jan M. Rabaey Anantha Chandrakasan, Borivoje Nikolic, Digital Integrated Circuits:A design Perspective[M]. second ed. 2004: Prentice Hall. 319-372.
[31] Hitchcock R. B., Timing verification and the timing analysis program[C]. IEEE/ACM Design Automation Conf. 1982. 594-604.
[32] Jouppi N. P., Timing analysis for nMOS VLSI[C]. IEEE/ACM Design Automation Conf. 1993. 411-418.
[33] Blaauw D.,V. Zolotov and S. Sundareswaran, Slope propagation in static timing analysis[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, 2002. 21(10): p. 1180-1195.
[34] Visweswariah C. and A.R. Conn, Formulation of static circuit optimization with reduced size,degeneracy and redundancy by timing graph manipulation[C]. Computer-Aided Design, 1999. Digest of Technical Papers. 1999 IEEE/ACM International Conference on. 1999. 244-251.
[35] Alur Rajeev, MOCHA User's Manual[EB/OL].http://embedded.eecs.berkeley.edu/research/mocha/doc/j-doc/.
[36] Rajeev Alur and Thomas A., Mocha: Modularity in model checking[C]. Tenth International Conference on Computer-aided Verification (CAV 1998). 521-525.
[37] Bryant R.E. and C.H.Seger, Formal hardware verification by symbolic ternary trajectory evaluation[C]. 28th Design Automation Conference. 1991. 397-402.
[38] Ritter G. Eveking H., Formal verification of design with complex control by symbolic simulation. Correct Hardware Design and Verification Metho'99. 1999. 234-249.
[39] Van Myra, Inwegen's checker summary[EB/OL]. http://www.cl.cam.ac.uk/~mjcg/HandelProject/summary.ps.
[40] Huang Chung-Yang, Register-transfer-level functional verification techniques[D]:[博士论文], in Engineering, Electronics and Electrical. 2000, University of California, Santa Barbara.
[41] Kantrowitz M., Noack, L.M., I'm done simulating; now what? Verification coverage analysis andcorrectness checking of the DECchip 21164 Alpha microprocessor[C]. Design Automation Conference Proceedings 1996, 33rd. 325-330.
[42] Kunle Olukotun Mark Heinrich, David Ofelt, Digital System Simulation: Methodologies and Examples[C]. Proceedings of 35th IEEE/ACM Design Automation Conference. 1998, San Francisco, CA.
[43] John Michael and Sebastian Smith, Application-Specific Integrated Circuits[M]. VLSI Design Series. June 1997: Addison-Wesley Publishing Company.
[44] Ulrich E.G., Event Manipulation for Discrete Simulations Requiring Large Numbers of Events[J]. Journal of the ACM, Sept 1978. 21(9): p. 777-785.
[45] Schilp William J., Techniques for high-speed digital circuit simulation[D]:[博士论文], in Computer Science.;Engineering, Electronics and Electrical. 2001, University of South Florida.
[46] Hansen C., Hardware Logic Simulation by Compilation[C]. 25th Design Automation Conference. 1988. 712-715.
[47] Wang Z. and P. M. Maurer, LECSIM: A Levelized Event Driven Compiled Logic Simulator[C]. 27th Design Automation Conference. 1990. 491-496.
[48] Lewis D. M., A Hierarchical Compiled Code Event driven Logic Simulator[J]. IEEE Transactions on Computer-Aided Design, June 1991. 10: p. 726-737.
[49] Maure Y. S. Lee and P. M., Two New Techniques for Compiled Multi-Delay Logic Simulation[C]. 29th Design Automation Conference. 1992. 420-423.
[50] Peter Maurer, The inversion algorithm for digital simulation[C]. International Conference on Computer-Aided Design, 1994. 1994. 61-258.
[51] Wang L.-T. Hoover N. E., Porter E. H. et al, SSIM: a software levelized compiled-code simulator[C]. Proceedings of the 24th ACM/IEEE conference on Design automation. June 1987. 2 - 8.
[52] Yaran B.H. Rahmati D., Zebardast A.S., Applying cycle-based simulation technique to VITAL as a VHDL gate level standard[C]. Electrical and Computer Engineering, 2001. Canadian Conference on. 1079-1084.
[53] Naroska E. Feipei Lai, Rung-Ji Shang et al, Hybrid parallel circuit simulation approaches[C]. 261 - 270.
[54] Prakash Rashinkar Peter Paterson, Leena Singh, System-on-chip verification[M]. 2001, Boston: Kluwer academic publisher. 10-13.
[55] 罗春, 田晓明, 王集森, et al, 系统芯片 FPGA 验证系统的软件调试环境设计[J].电子器件, 2003. 26(2).
[56] Graphics Mentor, VStationPRO[EB/OL]. http://www.mentor.com/products/fv/emulation/vstation_pro/. 2005.
[57] Graphics Mentor, VStationTBX[EB/OL]. http://www.mentor.com/products/fv/emulation/vstation_tbx/. 2005.
[58] Peterson G.D., Predicting the performance of SoC verification technologies[C]. VHDL International Users Forum Fall Workshop. 2000. 17-24.
[59] A. S. O. Clarke E.M. Gupta, Sat-based counterexample-guided abstraction refinement[J]. IEEE transaction on CAD of Integrated Circuits and Systems, July 2004. 23(7): p. 1113-1123.
[60] Peterson Gregory D., Performance Tradeoffs for Emulation, Hardware Acceleration, and Simulation[C]. 9th Annual International HDL Conference. March 2000.
[61] Yuan K. Shultz, C. Pixley et al, Modeling design constraints and biasing in simulation using BDDs[C]. ICCAD 1999. 584-589.
[62] Lee Richard and Benjamin Tsien, Presilicon verification of alpha 21364 micro-processor error handling system[C]. DAC 2001. 822-827.
[63] Synopsys, Vera User Guide[M/CD]. V6.1 ed. Synopsys Online Document U-2003.9. Vol. 1,2,4.
[64] Verisity, Specman Elite Manus[M/CD]. 2003: Verisity Design, Inc.
[65] 孟维佳, Garfield 芯片功能验证规划[D]:[硕士论文], in 电子工程系. 2005, 东南大学: 南京.
[66] 李暾, VLSI RTL 级模拟矢量自动生成技术研究[D]:[博士论文], in 计算机. 2003, 国防科技大学.
[67] Cheng Kwang-Ting and A.S. Krishnakumar, Automatic Generation of functional vectors using the extended finite state machine model[J]. ACM Trans. on Design Automation of Electronics Systems, Jan 1996: p. 57-79.
[68] Ganai M.K.,A. Aziz and A Kuehlmann, Enhancing simulation with BDDs and ATPG[C]. Design automation Conference 1999. 385-390.
[69] Pei-Hsin Ho Thomas Shiple, Smarts simulation using collaborative formal and simulation engines[J]. ICCAD 2000. 120-126.
[70] Zeng Zhihong, Functional test generation based on word-level satisfiability[D]:[博士论文], in Engineering, Electronics and Electrical. 2003, University of Massachusetts Amherst.
[71] Corno F. Sonza Reorda, M. Squillero, G. et al., Automatic test bench generation for validation of RT-level descriptions: an industrial experience[C]. Design, Automation and Test in Europe Conference and Exhibition. 2000. 385- 389.
[72] Stamenkovic Z. Dahmen, H.-Ch.et al, VHDL design validation by genetic manipulation techniques[C]. Microelectronics Proceedings. 2000. 735-738.
[73] Ferrandi F. Fin, A., An application of genetic algorithms and BDDs to functional testing. omputer Design, 2000. Proceedings. 48-56.
[74] Corno F. Reorda, M.S. Squillero, G. et al, Fully automatic test program generation for microprocessor cores[C]. Design, Automation and Test in Europe Conference and Exhibition, 2003. 1006- 1011.
[75] Shai Fine Avl Zlv, Coverage Directed Test Generation for Functional Verification Using Bayesian Networks. IEEE Design Automation Conference(DAC). June 2-6 2003.
[76] 罗春 杨军, 凌明, 基于遗传算法和覆盖率驱动的功能验证向量自动生成算法[J]. 应用科学学报. 23(4): p. 375-379.
[77] Lajolo M. Rebaudengo, M. etc al, System-level test bench generation in a co-design framework[C]. European Test Workshop, 2000, Proceedings. 25-30.
[78] Benjamin M. Geist, D. Hartman, A. Wolfsthal, Y. et al, A study in coverage-driven test generation[C]. Design Automation Conference, 1999. 970-975.
[79] K. Tasiran S. Keutzer, Coverage metrics for functional validation of hardware designs[J]. Design & Test of Computers, IEEE, July-Aug 2001. 18(4): p. 36-45.
[80] Corno F. Reorda, M.S. Squillero, G. et al, VEGA: a verification tool based on genetic algorithms[C]. VLSI in Computers and Processors. 1998.
[81] Qiushuang Zhang Harris, I.G., A data flow fault coverage metric for validation of behavioral HDL descriptions[C]. IEEE Computer Aided Design Conference. 2000. 217-220.
[82] Chien-Nan Jimmy Liu Chen-Yi Chang, Jing-Yang Jou, et al, A novel approach for functional coverage measurement in HDL[C]. IEEE ISCAS. 2000. 217-220.
[83] Luo Chun Yang Jun, Shi Longxing, Domain Strategy and Coverage Metric for Validation[C]. IEEE International Symposium on Quality Electronic Design (ISQED) 2005. 40-45.
[84] Luo Chun Yang Jun, Gao Gugang, et al, Domain Fault Model and Coverage Metric for SoC Verification[C]. IEEE International Symposium on Circuit and System(ISCAS) 2005. 5662-5665.
[85] 罗春、田晓明、王集森, 系统芯片 FPGA 验证系统的软件调试环境设计[J]. 电子器件, 2003. 26(2).
[86] Fallah F.,S. Devadas and K. Keutzer, OCCOM: Efficient computation of observability-based code coverage metirics for functional verification[C]. 35th ACM/IEEE DAC 1998. 152-157.
[87] Zhang Qiushuang and Harris I.G., A data flow fault coverage metric for validation of behavioral HDL descriptions[C]. IEEE Computer Aided Design Conference. 2000. 217-220.
[88] Pixley C, Guest Editor's Instroduction:Formal Verification of Commercial Integrated Circuits[J]. IEEE Design and Test of Computers, 2001. 18(4): p. 4-5.
[89] Semeria L. Seawright A., Mehra R., et al, RTL C-based methodology for designing and verifying a multi-threaded processor[C]. DAC 2002. 123-128.
[90] Matsumoto T. Saito H., Fujita M., Equivalence checking of C-based hardware descriptions by using symbolic simulation and program slice[C]. International Workshop on Logic and Synthesis 2003.
[91] Kroening D,Clarke E and Yorav K., Behavioral cosistency of C and Verilog programs using bounded model checking[C]. DAC 2003. 368-371.
[92] Pnueli A. Siegel M., Shtrichman O., The Code validation tool(CVT)-automatic verification of a compilation process[J]. Journal of Software Toolf for Technology Transfer, 1998. 2(2): p. 192-201.
[93] Accellera, Open Verification Library Assertion Monitor Reference Manual[EB/OL] V03.10.14. http://www.accellera.org/activities/ovl/TermsConditions. 2005.
[94] Accellera, SystemVerilog 3.1a Language Reference Manual[EM/OL]. http://www.systemverilog.org/. 2004.
[95] Accellera, SystemVerilog 3.1a Language Reference Manual.Chttp://www.systemverilog.org/. 2004.
[96] Pixley C Chittor A, Meyer F, et al, Functional verification 2003: technology, tools and methodology[C]. ASIC, 2003. Proceedings 5th International Conference on. 1-5.
[97] Chen Kuang-Chien, Assertion-based verification for SoC designs[C]. SIC, 2003. Proceedings 5th International Conference on. 12-15.
[98] Wang L-C Abadir M S, Krishnamurthy N et al, Automatic generation of assertions for formal verification of PowerPCTM microprocessor arrays using symbolic trajectory evaluation[C]. Design Automation Conference, 1998. Proceedings. 534-537.
[99] Ramkumar P Banerjee P, ProperCAD: A portable object-oriented parallel environment for VLSI CAD[J]. IEEE transaction on CAD, 1994. 13: p. 829-842.
[100] Wilsey P. A., QUESI II: Parallel simulation of VHDL[EB/OL], ed. Www.Ececs.Uc.Edu/~Paw/Quest.
[101] Banerjee P., Parallel algorithms for VLSI computer-aided design[M]. 1994: PTR Prentice Hall Press.
[102] Dragos Lungeanu, Discovery: Distributed simulation of digital and analog VLSI systems[D]:[博士论文], in Computer Science. 2000, The University of Iowa.
[103] Hering K., A parallel LCC simulation system[C]. Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings. xlv+1147.
[104] Mary L. Bailey, Jack V. Briner, Roger D., et al, Parallel logic simulation of VLSI systems[J]. ACM Computing Surveys, September 1994. 26(3): p. 255-294.
[105] Sundaram S., Patnaik, L.M., Distributed logic simulation: time-first evaluation vs. event driven algorithms[C]. VLSI Design, 1996. Proceedings,Ninth International Conference on. 307-310.
[106] Balarin Felice, Massimiliano Chiodo, Paolo Giusto, et al, Hardware-software co-design of embedded system[M]. 1997, Norwell: Kluwer Academic Publishers.
[107] Berkeley, Polis User Manual [EB/OL]. http://www-cad.eecs.berkeley.edu/Respep/Research/hsc/abstract.html.
[108] Sayinta A Canverdi G, Pauwels M, etc al., A mixed abstraction level co-simulation case study using SystemC for system on chip verification[c]. Design Automation and Test in Europe Conference and Exhibition 2003. 95-100.
[109] Kai RichterMarek Marek Jersak, Rolf Ernst, A Formal Approach to MpSoC Performance Verification[J]. IEEE Computer, 2003: p. 60-67.
[110] Wakabayashi K Okamoto T., C-based SoC design flow and EDA tools: an ASIC and system vendor perspective[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on. 19(12): p. 1507-1522.
[111] Joon-Seo Yim Yoon-Ho Hwang, Chang-Jae Park, A C-based RTL Design Verification Methodology for Complex Microprocessor[C]. 34th Design Automation Conference. 1997. 83-88.
[112] ARM, AMBA Specification[M/CD]. 2.0 ed. 1999: ARM.
[113] Jun Yuan Albin K. Aziz, A. et al, Simplifying Boolean constraint solving for random simulation-vector generation[C]. Computer Aided Design, 2002. ICCAD 2002. IEEE/ACM International Conference on. 123 - 127.
[114] Yuan J. Shultz, K. Pixley, C. et al, Modeling design constraints and biasing in simulation using BDDs[C]. ICCAD 1999. 584-589.
[115] Chung-Yang Huan Kwang-Ting Cheng, Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking[C].Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on. March 2001. 381 - 391.
[116] Fallah F. Ashar, P. Devadas, S., Simulation vector generation from HDL descriptions for observability-enhanced statement coverage[C]. Design Automation Conference, 1999. Proceedings,36th. xxxii+1003.
[117] Fallah F. Devadas, S. Keutzer, K., Functional vector generation for HDL models using linear programming and 3-satisfiability[C]. Design Automation Conference, 1998. Proceedings. xxxii+820.
[118] Jaffar J.,S. Michaylov and P. J. Syuckey, The CLP(R) Language and System[J]. IBM, Res. Rep. RC 16292 (#72336), 1990.
[119] Chandra A.K. Iyengar, V.S., Constraint solving for test case generation: a technique for high-level design verification[C]. Computer Design: VLSI in Computers and Processors, 1992. ICCD '92. Proceedings., IEEE 1992 International Conference on. 245 - 248.
[120] Aharon A.,A. Bar-David and B. Dorfman, Verification of the IBM RISC system/6000 by a dynamic biased pseudo-random test program generator[J]. IBM System Journal, July 1991. 30(4): p. 527-538.
[121] Freeman J.,R. Duerden and C. Taylor, The 68060 micoprocessor functional design and verification methodology[C]. In On-Chip-System Design Conference. 1995. 10.1-10.14.
[122] Weiser M., Program Slicing[J]. IEEE transaction on Software Engineering, 1984. 10(4): p. 352-357.
[123] Ichinose S.,M. Iwaihara and H.Yasuura, Program slicing on VHDL descriptions and its evaluation[J]. IEICE Transactions on Fund, Dec. 1998. E81-A(12): p. 2585-2597.
[124] Moundanos D., Abraham J.A., Hoskote Y.V., Abstraction techniques for valication coverage analysis and test generation[J]. IEEE transaction on Computers, 1998. 47(1): p. 2-14.
[125] Diaz Daniel and Philips Codognet, The GNU prolog system and its implementation[C]. 2000 ACM symposium on Applied computing. Vol. 2. 2000. 728-732.
[126] Joon-Seo Yim Chang-Jae Park, Woo-Seung Yang, et al, Verification methodology of compatible microprocessors. Design Automation Conference 1997. Proceedings of the ASP-DAC '97. Asia and South Pacific. 173 -180.
[127] Fine Shai and Avl Zlv, Coverage Directed Test Generation for Functional Verification Using Bayesian Networks[C]. IEEE Design Automation Conference(DAC). June 2-6 2003.
[128] Corno F., Sonza Reorda and G. Squillero, Automatic test bench generation for validation of RT-level descriptions: an industrial experience[C]. Design, Automation and Test in Europe Conference and Exhibition. 2000. 385- 389.
[129] Holland J H, Adaptation in natual and artificial systems[M]. 1975, Ann Arbor: The University of Michigan Press.
[130] Prinetto P., M. Rebaudengo, M. Sonza, et al, GATTO: an Intelligent Tool for Automatic Test Pattern Generation for Digital Circuits[EB/OL]. http://www.polito.it.
[131] 韦刚,陆以勤 贺前华,, 基因算法研究进展[J]. 电子学报, 1998 年十月.
[133] 杨军, 基于压缩和调度的系统芯片低成本测试研究[D]:[博士论文], in 电子工程系. 2004, 东南大学.
[134] Min Byeong Eon, Register-transfer-level design verification: Coverage and acceleration[D]:[博士论文], in Engineering, Electronics and Electrical.;Computer Science. 2001, Texas A&M University.
[135] Devadas S.,A. Ghosh and K. Keutzer, An observability-based code coverage metric[C]. IEEE/ACM Conf. on Computer-Aided Design(ICCAD-96). 1996. 418-425.
[136] R. Vemuri R. Kalyanaraman, Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming[J]. IEEE transaction on VLSI Systems, 1995. 3(2): p. 201-214.
[137] Corno F.,M.S. Reorda and G. Squillero, High-level observability for effective high-level ATPG[C]. 18th IEEE VLSI Test Symp. 2000. 411-416.
[138] White L. J. Cohen, E I, A domain strategy for computer program testing[J]. IEEE Transaction on Software Engineering, May 1980. SE-6(3): p. 247-257.
[139] 赵瑞莲, 软件测试方法研究[D]:[博士论文]. 2001, 中国科学院计算机技术研究所.
[140] Clarke J. L.A , A close look at domain testing[J]. IEEE Transaction on Software Engineering, July 1982. SE-8(4): p. 380-390.
[141] B.Jeng E. J., A simplified domain-testing strategy[J]. ACM Transactions on Software Engineering and Methodology, July 1994. 3(3): p. 254-270.
[142] Qiushuang Zhang Harris I.G., A domain coverage metric for the validation of behavioral VHDL descriptions[C]. Test Conference, 2000 Proceedings International. 302-308.
[143] Synopsys, HDL Compiler for VerilogReference Manual[DB/MT] V6.1. Synopsys Online Document U-2003.9 Volumes 1,2,4.
[144] IEEE, Standard Verilog Hardware Description Language[S]. IEEE Std. 1364-2001. 2001.
[145] 张文军,罗春 and 杨军, 基于 PLI 的 AC97 Codec 快速仿真模型设计[J]. 电子工程师, 2005 年 第 12 期.
[146] Qiushuang Zhang, Validation of behavioral hardware descriptions[D]:[博士论文]. 2003, University of Massachusetts Amherst.
[147] Synopsys. DesignWare DW_apb_uart Databook[DB/MT]. Version2.00e. 2003/10.
[148] Synopsys, VCS / VCS MX Coverage Metrics User Guide. Version 7.1.1[DB/MT]. 2003/10.
[149] Kroening D Clarke E, Checking consistency of C and Verilog using predicate abstraction and induction[C]. IEEE ICCAD-2004. 1004-1009.
[150] Jain P.P., Cost-effective co-verification using RTL-accurate C models[C]. Circuits and Systems 99. 1999. 460 - 463.
[151] Takach A.,B. Bowyer and T. Bollaert, C based hardware design for wireless applications[C]. Design, Automation and Test in Europe, 2005. 124 - 129.
[152] 罗琨,曹阳 and 尹建华, 数字专用集成电路设计中SystemC建模验证方法[J]. 武汉大学学报, 2002 年 6 月. 48(3): p. 306-310.
[153] Blaurock O., A systemC-based modular design and verification framework for C-model reuse in a HW/SW-codesign design flow[C]. Distributed Computing Systems Workshops, 2004. Proceedings. 24th International Conference on. 838-843.
[154] 庄明渊, 基于 ARM7TDMI 的 MPEG-4 视频解码的实现和优化[D]:[硕士论文].2005, 东南大学.
[155] Chen W H,Smith C H and Fralick S C, A fast computational algorithm for the discrete transform[J]. IEEE Trans on Communications, 1997. 19: p. 1004-1009.
[156] Turing A. M., Checking a Large Routine. Conference on High Speed Automatic Calculating Machines. June 1949. 67-69.
[157] Taylor Scott, Functional Verification of a Multiple-issue, Out-of-Order, Superscalar . 638-643. Alpha Processor The DEC Alpha 21264 Microprocessor[C]. esign Automation Conference. Jun 1998. 638-643.
[158] Abarbanel Y., FoCs - Automatic Generation of Simulation Checkers from Formal Speciation[C]. 12th International Conference on Computer-Aided Verification (CAV). Vol. olume 1855 of Lecture Notes in Computer Science. 2000.
[159] Accellera, Open Verification Library Reference Manual[EB/OL]. http://www.verificationlib.org. 2003.
[160] Accellera, Property Specification Language Reference Manual[EB/OL]. http://www.eda.org/vfv/docs/PSL-v1.1.pdf. 2004.
[161] Kausik Datta and P P Das, Assertion Based Verification Using HDVL[C]. Proceedings of the 17th International Conference on VLSI Design(VLSID ? 04). 2004.
[162] Andrews Jason R, Co-Verification of Hardware and Software for Arm SoC Design[M]. 2004, Burlington: Newnes. 134-137.
[163] Andrews Jason R, Co-Verification of Hardware and Software for Arm SoC Design[M]. 2004, Burlington: Newnes. 137-140.
[164] Ptolemy, The Ptolemy Project[EB/OL]. http://ptolemy.eecs.berkeley.edu/.
[165] MentorGraphics, SeamlessCVE5.0[EB/OL]. http://www.mentor.com/seamless.
[166] Synopsys, Co-CentricSystemStudio[EB/OL]. http://www.synopsys.com/products/cocentric_studio/.
[167] Hoffmann A. Kogel T., Meyr H., A framework for fast hardware-software co-simulation[C]. Design, Automation and Test in Europe Conference and Exhibition, 2001. 760 - 764.
[168] Hoffmann A. Kogel, T. Meyr, H., A framework for fast hardware-software co-simulation[C]. Design, Automation and Test in Europe Conference and Exhibition, 2001. 760 - 764.
[169] CoWare, CoWare N2C System Designer[EB/OL]. http://www.coware.com.
[170] TNI-Valiosys, Cosimate[EB/OLL]. http://www.tniworld.com/cosimate.asp.
[171] Fornaciari W. Sciuto, D. Salice, F., A two-level cosimulation environment[J]. IEEE Computer, 1997. 30(6): p. 109-11.
[172] Lahiri K. Raghunathan, A. Dey, S., System-level performance analysis for designing on-chip communication architectures[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, June 2001. 20(6): p. 768-783.
[173] Morawice A. Ubar, R. Raik, J., Cycle-based simulation algorithms for digital systems using high-level decision diagrams[C], ed. Design Automation and Test in Europe Conference and Exhibition 2000. 743.
[174] Ubar R. Morawiec, A. Raik, J., Cycle-based simulation with decision diagrams[C]. Design, Automation and Test in Europe Conference and Exhibition 1999. 454 - 458.
[175] Kei-Yong Khoo Willson A.N., Jr., Cycle-based timing simulations using event-streams[C]. Computer Design: VLSI in Computers and Processors, 1996. 460 -465.
[176] McKinney M.D., Integrating Perl, Tcl and C++ into simulation-based ASIC verification environments[C]. High-Level Design Validation and Test Workshop, 2001. Proceedings. Sixth IEEE International. 19 - 24.
[177] Sarmento A.,Cesario W. and Jerraya A.A., Automatic building of executable models from abstract SoC architectures made of heterogeneous subsystems[C]. Rapid System Prototyping, 2004. Proceedings. 15th IEEE International Workshop on. 88 - 95.
[178] A. Wadekar S., A RT level verification method for SoC designs[C]. IEEE SOC Conference 2003. 29-32.
[179] Jindal R Jain K., Verification of transaction-level SystemC models using RTL testbenches[C]. Formal Methods and Models for Co-Design, 2003. 199-203.
[180] P.P. Jain, Cost-effective co-verification using RTL-accurate C models[C]. Circuits and Systems 99. 1999. 460 - 463.
[181] Chen Shi Hua Shenghua Lien Y.E. Using the C language to reduce the design cycle of an MPEG-2 video IC: a case study. in 2nd International Conference on ASIC. 19996: IEEE.
[182] Takach A. Bowyer, B. Bollaert, T., C based hardware design for wireless applications[C]. Design, Automation and Test in Europe, 2005. 124 - 129.
[183] Formaggio L. Fummi, F. Pravadelli, G., A timing-accurate HW/SW cosimulation of an ISS with SystemC[C]. International Conference on Hardware/Software Codesign and System Synthesis, 2004. 152 - 157.
[184] Liem C. Nacabal, F. Valderrama, C. Paulin, P. Jerraya, A., System-on-a-chip cosimulation and compilation[J]. Design & Test of Computers, IEEE, April-June 1997. 14(2): p. 16-25.
[185] Greaves D.J., A Verilog to C compiler[C]. 11th International Workshop on Rapid System Prototyping, 2000. 122-127.
[186] ARM, ARM Developer Suite Debug Targut Guide[M/CD]. 1.1 ed. 2001: ARM Limited.
[187] 王镇, SoC 系统的高层建模[D]:[硕士论文], in 电子工程系. 2005, 东南大学.
[188] Wilson Snyder Paul Wasson, Duane Galbi, Verilator - Convert Verilog code to C++/SystemC[EB/OL]. http://www.veripool.com/verilator_doc.html.
[189] ARM, MM_synopsys_vcs_verilog.txt[M/CD]. 2002: ARM.
[190] 张拥军, 基于 Specman Elite 验证平台的 Garfield III 功能验证[D]:[硕士论文], in 电子工程系. 2004, 东南大学.
[191] Rafael C.Gonzalez Richard E.Woods, Digital Image Processing. 2th ed. 2002.7: Publishing House of Electronics Industry.
[192] 朱永峰, 多媒体加速器的研究及设计[D]:[硕士论文], in 电子工程系. 2004, 东南大学.
[2] ITRS, INTERNATIONAL TECHNOLOGY ROADMAP FOR SEMICONDUCTORS 2005 Edition Design[EB/OL]. http://www.itrs.net/Common/2005ITRS/Home2005.htm. 2005. 21-30.
[3] Bergeron Janick, Writing Testbenchs: Functional Verification of HDL Models[M]. January 2000: Kluwer Academic Publishers. 1-19.
[4] Bailey Brian, The Need for a Scalable Verification Methodology to Overcome the Limitations of Current Verification Approaches[EB/OL]. http://www.mentor.com/techpapers/fulfillment/upload/mentorpaper_22780.pdf. August 1, 2004.
[5] Clarke E.M, Automatic verification of finite-state concurrent systems[C]. Logic in Computer Science, 1994, LICS '94. Jul 1994. 126-132.
[6] Jayanta Bhadra, Abstraction techniques for verification of digital designs[D]:[博士学位论文], in Engineering, Electronics and Electrical. 2001, The University of Texas at Austin.
[7] Burch J.R., symbolic model checking: 1020 states and beyond[C]. Logic in Computer Science, 1990, LICS '90. 1990. 428-439.
[8] Clarke E.M,E.A. Emerson and A.P. Sittla, Automatic verification of finite-state concurrent systems using temporal logic specification[J]. ACM Trans. on Program Language Systems, 1986. 8: p. 244-263.
[9] Pnueli A. Siegel M., A temporal logic of concurrent programs[J]. Theoretical Computer Science, 1981. 13: p. 45-60.
[10] Bryant R.E., Graph based algorithms for Boolean function manipulation[J]. IEEE Transactions on Computers, 1986. 35(8): p. 677-691.
[11] VISGroup, VIS User's Manual[EB/OL]. http://vlsi.colorado.edu/%7Evis/doc/VisUser/vis_user/vis_user.html.
[12] Martin Davis and Hilary Putnam, A computing procedure for quantification theory[J]. Journal of The Assocation for Computing Machinery, 1960. 7: p. 201-215.
[13] Matthew H. Moskewicz Conor F. Madigan, Ying Zhao et al, Chaff: Engineering an Efficient STA Solver[C]. Proceedings of the 38th Design Automation Conference. June 2001. 530-535.
[14] Prasad Mukul Ranjan, Propositional satisfiability algorithms in EDA applications[D]:[博士论文], in Engineering, Electronics and Electrical.;Computer Science. 2001, University of California, Berkeley.
[15] Marques-Silva J. and Guerra Silva, Solving satisfiability in combinational circuits[J]. Design & Test of Computers, IEEE. 20(4): p. 16-21.
[16] Wang Dong, SAT based abstraction refinement for hardware verification[D]:[博士学位论文], in Engineering, Electronics and Electrical. 2003, Carnegie Mellon University.
[17] Lyerand Parthasarathy G.M.K. and Cheng K.T., Safety property verification using sequential SAT and bounded model checking[J]. Design & Test of Computers, IEEE,2004. 21(2): p. 132-143.
[18] Marek Kai Richter,Marek Jersak and Rolf Ernst, A Formal Approach to MpSoC Performance Verification[J]. IEEE Computer, April 2003. 36(4): p. 60-67.
[19] Choi Hoon, Byeongwhee Yun, Yuntae Lee, et al, Model checking of S3C2400X industrial embedded SOC product[C]. Design Automation Conference,2001. 611-616.
[20] Clarke E.M. and J. Wing, Formal methods: state of the art and future directions[J]. ACM Comuting Surveys. 28(4): p. 626-643.
[21] Gordon M. J. C., A proof generating system for higher order logic[J]. Current Trends in Hardware Verification and Automated Theorem Proving, 1989: p. 74-128.
[22] Owre S.,J. M. Rushby and N. Shankar, PVS: A prototype verification system[C]. 11th International Conference on Automated Deduction (CADE). 1992. 748-752.
[23] Brock Bishop,Matt Kaufmann and Moore Strother, ACL2 Theorems about Commercial Microprocessors[C]. First international conference on formal methods in computer-aided design. 1996.
[24] Moore J Strother,Tom Lynch and Matt Kaufmann, A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm[J]. IEEE Transactions on Computers, 1998. 47(9): p. 913-926.
[25] Paul Miner and Leathrum James, Verification of IEEE Compliant Subtractive Division Algorithms[C]. First international conference on formal methods in computer-aided design. 1996. 111-122.
[26] Herbstritt M.,Kmieciak T. and Becker B., On the impact of structural circuit partitioning on SAT-based combinational circuit verification[C]. Microprocessor Test and Verification, 2004. Fifth International Workshop on. 2004. 50-55.
[27] Reda S. and Salem A., Combinational Equivalence Checking using Boolean Satisfiability and Binary Decision Diagrams[C]. Design, Automation and Test in Europe. 2001.
[28] Davis M., Logeman G., Loveland D., A machine program for the theorm proving[J]. Communication. ACM, July 1962. 5: p. 394-397.
[29] Kuehlmann A. Paruthi V., Krohm F., et al, Robust Boolean reasoning for equivalence checking and functional property verification[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, Dec. 2002. 21(12): p. 1377-1394.
[30] Jan M. Rabaey Anantha Chandrakasan, Borivoje Nikolic, Digital Integrated Circuits:A design Perspective[M]. second ed. 2004: Prentice Hall. 319-372.
[31] Hitchcock R. B., Timing verification and the timing analysis program[C]. IEEE/ACM Design Automation Conf. 1982. 594-604.
[32] Jouppi N. P., Timing analysis for nMOS VLSI[C]. IEEE/ACM Design Automation Conf. 1993. 411-418.
[33] Blaauw D.,V. Zolotov and S. Sundareswaran, Slope propagation in static timing analysis[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, 2002. 21(10): p. 1180-1195.
[34] Visweswariah C. and A.R. Conn, Formulation of static circuit optimization with reduced size,degeneracy and redundancy by timing graph manipulation[C]. Computer-Aided Design, 1999. Digest of Technical Papers. 1999 IEEE/ACM International Conference on. 1999. 244-251.
[35] Alur Rajeev, MOCHA User's Manual[EB/OL].http://embedded.eecs.berkeley.edu/research/mocha/doc/j-doc/.
[36] Rajeev Alur and Thomas A., Mocha: Modularity in model checking[C]. Tenth International Conference on Computer-aided Verification (CAV 1998). 521-525.
[37] Bryant R.E. and C.H.Seger, Formal hardware verification by symbolic ternary trajectory evaluation[C]. 28th Design Automation Conference. 1991. 397-402.
[38] Ritter G. Eveking H., Formal verification of design with complex control by symbolic simulation. Correct Hardware Design and Verification Metho'99. 1999. 234-249.
[39] Van Myra, Inwegen's checker summary[EB/OL]. http://www.cl.cam.ac.uk/~mjcg/HandelProject/summary.ps.
[40] Huang Chung-Yang, Register-transfer-level functional verification techniques[D]:[博士论文], in Engineering, Electronics and Electrical. 2000, University of California, Santa Barbara.
[41] Kantrowitz M., Noack, L.M., I'm done simulating; now what? Verification coverage analysis andcorrectness checking of the DECchip 21164 Alpha microprocessor[C]. Design Automation Conference Proceedings 1996, 33rd. 325-330.
[42] Kunle Olukotun Mark Heinrich, David Ofelt, Digital System Simulation: Methodologies and Examples[C]. Proceedings of 35th IEEE/ACM Design Automation Conference. 1998, San Francisco, CA.
[43] John Michael and Sebastian Smith, Application-Specific Integrated Circuits[M]. VLSI Design Series. June 1997: Addison-Wesley Publishing Company.
[44] Ulrich E.G., Event Manipulation for Discrete Simulations Requiring Large Numbers of Events[J]. Journal of the ACM, Sept 1978. 21(9): p. 777-785.
[45] Schilp William J., Techniques for high-speed digital circuit simulation[D]:[博士论文], in Computer Science.;Engineering, Electronics and Electrical. 2001, University of South Florida.
[46] Hansen C., Hardware Logic Simulation by Compilation[C]. 25th Design Automation Conference. 1988. 712-715.
[47] Wang Z. and P. M. Maurer, LECSIM: A Levelized Event Driven Compiled Logic Simulator[C]. 27th Design Automation Conference. 1990. 491-496.
[48] Lewis D. M., A Hierarchical Compiled Code Event driven Logic Simulator[J]. IEEE Transactions on Computer-Aided Design, June 1991. 10: p. 726-737.
[49] Maure Y. S. Lee and P. M., Two New Techniques for Compiled Multi-Delay Logic Simulation[C]. 29th Design Automation Conference. 1992. 420-423.
[50] Peter Maurer, The inversion algorithm for digital simulation[C]. International Conference on Computer-Aided Design, 1994. 1994. 61-258.
[51] Wang L.-T. Hoover N. E., Porter E. H. et al, SSIM: a software levelized compiled-code simulator[C]. Proceedings of the 24th ACM/IEEE conference on Design automation. June 1987. 2 - 8.
[52] Yaran B.H. Rahmati D., Zebardast A.S., Applying cycle-based simulation technique to VITAL as a VHDL gate level standard[C]. Electrical and Computer Engineering, 2001. Canadian Conference on. 1079-1084.
[53] Naroska E. Feipei Lai, Rung-Ji Shang et al, Hybrid parallel circuit simulation approaches[C]. 261 - 270.
[54] Prakash Rashinkar Peter Paterson, Leena Singh, System-on-chip verification[M]. 2001, Boston: Kluwer academic publisher. 10-13.
[55] 罗春, 田晓明, 王集森, et al, 系统芯片 FPGA 验证系统的软件调试环境设计[J].电子器件, 2003. 26(2).
[56] Graphics Mentor, VStationPRO[EB/OL]. http://www.mentor.com/products/fv/emulation/vstation_pro/. 2005.
[57] Graphics Mentor, VStationTBX[EB/OL]. http://www.mentor.com/products/fv/emulation/vstation_tbx/. 2005.
[58] Peterson G.D., Predicting the performance of SoC verification technologies[C]. VHDL International Users Forum Fall Workshop. 2000. 17-24.
[59] A. S. O. Clarke E.M. Gupta, Sat-based counterexample-guided abstraction refinement[J]. IEEE transaction on CAD of Integrated Circuits and Systems, July 2004. 23(7): p. 1113-1123.
[60] Peterson Gregory D., Performance Tradeoffs for Emulation, Hardware Acceleration, and Simulation[C]. 9th Annual International HDL Conference. March 2000.
[61] Yuan K. Shultz, C. Pixley et al, Modeling design constraints and biasing in simulation using BDDs[C]. ICCAD 1999. 584-589.
[62] Lee Richard and Benjamin Tsien, Presilicon verification of alpha 21364 micro-processor error handling system[C]. DAC 2001. 822-827.
[63] Synopsys, Vera User Guide[M/CD]. V6.1 ed. Synopsys Online Document U-2003.9. Vol. 1,2,4.
[64] Verisity, Specman Elite Manus[M/CD]. 2003: Verisity Design, Inc.
[65] 孟维佳, Garfield 芯片功能验证规划[D]:[硕士论文], in 电子工程系. 2005, 东南大学: 南京.
[66] 李暾, VLSI RTL 级模拟矢量自动生成技术研究[D]:[博士论文], in 计算机. 2003, 国防科技大学.
[67] Cheng Kwang-Ting and A.S. Krishnakumar, Automatic Generation of functional vectors using the extended finite state machine model[J]. ACM Trans. on Design Automation of Electronics Systems, Jan 1996: p. 57-79.
[68] Ganai M.K.,A. Aziz and A Kuehlmann, Enhancing simulation with BDDs and ATPG[C]. Design automation Conference 1999. 385-390.
[69] Pei-Hsin Ho Thomas Shiple, Smarts simulation using collaborative formal and simulation engines[J]. ICCAD 2000. 120-126.
[70] Zeng Zhihong, Functional test generation based on word-level satisfiability[D]:[博士论文], in Engineering, Electronics and Electrical. 2003, University of Massachusetts Amherst.
[71] Corno F. Sonza Reorda, M. Squillero, G. et al., Automatic test bench generation for validation of RT-level descriptions: an industrial experience[C]. Design, Automation and Test in Europe Conference and Exhibition. 2000. 385- 389.
[72] Stamenkovic Z. Dahmen, H.-Ch.et al, VHDL design validation by genetic manipulation techniques[C]. Microelectronics Proceedings. 2000. 735-738.
[73] Ferrandi F. Fin, A., An application of genetic algorithms and BDDs to functional testing. omputer Design, 2000. Proceedings. 48-56.
[74] Corno F. Reorda, M.S. Squillero, G. et al, Fully automatic test program generation for microprocessor cores[C]. Design, Automation and Test in Europe Conference and Exhibition, 2003. 1006- 1011.
[75] Shai Fine Avl Zlv, Coverage Directed Test Generation for Functional Verification Using Bayesian Networks. IEEE Design Automation Conference(DAC). June 2-6 2003.
[76] 罗春 杨军, 凌明, 基于遗传算法和覆盖率驱动的功能验证向量自动生成算法[J]. 应用科学学报. 23(4): p. 375-379.
[77] Lajolo M. Rebaudengo, M. etc al, System-level test bench generation in a co-design framework[C]. European Test Workshop, 2000, Proceedings. 25-30.
[78] Benjamin M. Geist, D. Hartman, A. Wolfsthal, Y. et al, A study in coverage-driven test generation[C]. Design Automation Conference, 1999. 970-975.
[79] K. Tasiran S. Keutzer, Coverage metrics for functional validation of hardware designs[J]. Design & Test of Computers, IEEE, July-Aug 2001. 18(4): p. 36-45.
[80] Corno F. Reorda, M.S. Squillero, G. et al, VEGA: a verification tool based on genetic algorithms[C]. VLSI in Computers and Processors. 1998.
[81] Qiushuang Zhang Harris, I.G., A data flow fault coverage metric for validation of behavioral HDL descriptions[C]. IEEE Computer Aided Design Conference. 2000. 217-220.
[82] Chien-Nan Jimmy Liu Chen-Yi Chang, Jing-Yang Jou, et al, A novel approach for functional coverage measurement in HDL[C]. IEEE ISCAS. 2000. 217-220.
[83] Luo Chun Yang Jun, Shi Longxing, Domain Strategy and Coverage Metric for Validation[C]. IEEE International Symposium on Quality Electronic Design (ISQED) 2005. 40-45.
[84] Luo Chun Yang Jun, Gao Gugang, et al, Domain Fault Model and Coverage Metric for SoC Verification[C]. IEEE International Symposium on Circuit and System(ISCAS) 2005. 5662-5665.
[85] 罗春、田晓明、王集森, 系统芯片 FPGA 验证系统的软件调试环境设计[J]. 电子器件, 2003. 26(2).
[86] Fallah F.,S. Devadas and K. Keutzer, OCCOM: Efficient computation of observability-based code coverage metirics for functional verification[C]. 35th ACM/IEEE DAC 1998. 152-157.
[87] Zhang Qiushuang and Harris I.G., A data flow fault coverage metric for validation of behavioral HDL descriptions[C]. IEEE Computer Aided Design Conference. 2000. 217-220.
[88] Pixley C, Guest Editor's Instroduction:Formal Verification of Commercial Integrated Circuits[J]. IEEE Design and Test of Computers, 2001. 18(4): p. 4-5.
[89] Semeria L. Seawright A., Mehra R., et al, RTL C-based methodology for designing and verifying a multi-threaded processor[C]. DAC 2002. 123-128.
[90] Matsumoto T. Saito H., Fujita M., Equivalence checking of C-based hardware descriptions by using symbolic simulation and program slice[C]. International Workshop on Logic and Synthesis 2003.
[91] Kroening D,Clarke E and Yorav K., Behavioral cosistency of C and Verilog programs using bounded model checking[C]. DAC 2003. 368-371.
[92] Pnueli A. Siegel M., Shtrichman O., The Code validation tool(CVT)-automatic verification of a compilation process[J]. Journal of Software Toolf for Technology Transfer, 1998. 2(2): p. 192-201.
[93] Accellera, Open Verification Library Assertion Monitor Reference Manual[EB/OL] V03.10.14. http://www.accellera.org/activities/ovl/TermsConditions. 2005.
[94] Accellera, SystemVerilog 3.1a Language Reference Manual[EM/OL]. http://www.systemverilog.org/. 2004.
[95] Accellera, SystemVerilog 3.1a Language Reference Manual.Chttp://www.systemverilog.org/. 2004.
[96] Pixley C Chittor A, Meyer F, et al, Functional verification 2003: technology, tools and methodology[C]. ASIC, 2003. Proceedings 5th International Conference on. 1-5.
[97] Chen Kuang-Chien, Assertion-based verification for SoC designs[C]. SIC, 2003. Proceedings 5th International Conference on. 12-15.
[98] Wang L-C Abadir M S, Krishnamurthy N et al, Automatic generation of assertions for formal verification of PowerPCTM microprocessor arrays using symbolic trajectory evaluation[C]. Design Automation Conference, 1998. Proceedings. 534-537.
[99] Ramkumar P Banerjee P, ProperCAD: A portable object-oriented parallel environment for VLSI CAD[J]. IEEE transaction on CAD, 1994. 13: p. 829-842.
[100] Wilsey P. A., QUESI II: Parallel simulation of VHDL[EB/OL], ed. Www.Ececs.Uc.Edu/~Paw/Quest.
[101] Banerjee P., Parallel algorithms for VLSI computer-aided design[M]. 1994: PTR Prentice Hall Press.
[102] Dragos Lungeanu, Discovery: Distributed simulation of digital and analog VLSI systems[D]:[博士论文], in Computer Science. 2000, The University of Iowa.
[103] Hering K., A parallel LCC simulation system[C]. Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings. xlv+1147.
[104] Mary L. Bailey, Jack V. Briner, Roger D., et al, Parallel logic simulation of VLSI systems[J]. ACM Computing Surveys, September 1994. 26(3): p. 255-294.
[105] Sundaram S., Patnaik, L.M., Distributed logic simulation: time-first evaluation vs. event driven algorithms[C]. VLSI Design, 1996. Proceedings,Ninth International Conference on. 307-310.
[106] Balarin Felice, Massimiliano Chiodo, Paolo Giusto, et al, Hardware-software co-design of embedded system[M]. 1997, Norwell: Kluwer Academic Publishers.
[107] Berkeley, Polis User Manual [EB/OL]. http://www-cad.eecs.berkeley.edu/Respep/Research/hsc/abstract.html.
[108] Sayinta A Canverdi G, Pauwels M, etc al., A mixed abstraction level co-simulation case study using SystemC for system on chip verification[c]. Design Automation and Test in Europe Conference and Exhibition 2003. 95-100.
[109] Kai RichterMarek Marek Jersak, Rolf Ernst, A Formal Approach to MpSoC Performance Verification[J]. IEEE Computer, 2003: p. 60-67.
[110] Wakabayashi K Okamoto T., C-based SoC design flow and EDA tools: an ASIC and system vendor perspective[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on. 19(12): p. 1507-1522.
[111] Joon-Seo Yim Yoon-Ho Hwang, Chang-Jae Park, A C-based RTL Design Verification Methodology for Complex Microprocessor[C]. 34th Design Automation Conference. 1997. 83-88.
[112] ARM, AMBA Specification[M/CD]. 2.0 ed. 1999: ARM.
[113] Jun Yuan Albin K. Aziz, A. et al, Simplifying Boolean constraint solving for random simulation-vector generation[C]. Computer Aided Design, 2002. ICCAD 2002. IEEE/ACM International Conference on. 123 - 127.
[114] Yuan J. Shultz, K. Pixley, C. et al, Modeling design constraints and biasing in simulation using BDDs[C]. ICCAD 1999. 584-589.
[115] Chung-Yang Huan Kwang-Ting Cheng, Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking[C].Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on. March 2001. 381 - 391.
[116] Fallah F. Ashar, P. Devadas, S., Simulation vector generation from HDL descriptions for observability-enhanced statement coverage[C]. Design Automation Conference, 1999. Proceedings,36th. xxxii+1003.
[117] Fallah F. Devadas, S. Keutzer, K., Functional vector generation for HDL models using linear programming and 3-satisfiability[C]. Design Automation Conference, 1998. Proceedings. xxxii+820.
[118] Jaffar J.,S. Michaylov and P. J. Syuckey, The CLP(R) Language and System[J]. IBM, Res. Rep. RC 16292 (#72336), 1990.
[119] Chandra A.K. Iyengar, V.S., Constraint solving for test case generation: a technique for high-level design verification[C]. Computer Design: VLSI in Computers and Processors, 1992. ICCD '92. Proceedings., IEEE 1992 International Conference on. 245 - 248.
[120] Aharon A.,A. Bar-David and B. Dorfman, Verification of the IBM RISC system/6000 by a dynamic biased pseudo-random test program generator[J]. IBM System Journal, July 1991. 30(4): p. 527-538.
[121] Freeman J.,R. Duerden and C. Taylor, The 68060 micoprocessor functional design and verification methodology[C]. In On-Chip-System Design Conference. 1995. 10.1-10.14.
[122] Weiser M., Program Slicing[J]. IEEE transaction on Software Engineering, 1984. 10(4): p. 352-357.
[123] Ichinose S.,M. Iwaihara and H.Yasuura, Program slicing on VHDL descriptions and its evaluation[J]. IEICE Transactions on Fund, Dec. 1998. E81-A(12): p. 2585-2597.
[124] Moundanos D., Abraham J.A., Hoskote Y.V., Abstraction techniques for valication coverage analysis and test generation[J]. IEEE transaction on Computers, 1998. 47(1): p. 2-14.
[125] Diaz Daniel and Philips Codognet, The GNU prolog system and its implementation[C]. 2000 ACM symposium on Applied computing. Vol. 2. 2000. 728-732.
[126] Joon-Seo Yim Chang-Jae Park, Woo-Seung Yang, et al, Verification methodology of compatible microprocessors. Design Automation Conference 1997. Proceedings of the ASP-DAC '97. Asia and South Pacific. 173 -180.
[127] Fine Shai and Avl Zlv, Coverage Directed Test Generation for Functional Verification Using Bayesian Networks[C]. IEEE Design Automation Conference(DAC). June 2-6 2003.
[128] Corno F., Sonza Reorda and G. Squillero, Automatic test bench generation for validation of RT-level descriptions: an industrial experience[C]. Design, Automation and Test in Europe Conference and Exhibition. 2000. 385- 389.
[129] Holland J H, Adaptation in natual and artificial systems[M]. 1975, Ann Arbor: The University of Michigan Press.
[130] Prinetto P., M. Rebaudengo, M. Sonza, et al, GATTO: an Intelligent Tool for Automatic Test Pattern Generation for Digital Circuits[EB/OL]. http://www.polito.it.
[131] 韦刚,陆以勤 贺前华,, 基因算法研究进展[J]. 电子学报, 1998 年十月.
[133] 杨军, 基于压缩和调度的系统芯片低成本测试研究[D]:[博士论文], in 电子工程系. 2004, 东南大学.
[134] Min Byeong Eon, Register-transfer-level design verification: Coverage and acceleration[D]:[博士论文], in Engineering, Electronics and Electrical.;Computer Science. 2001, Texas A&M University.
[135] Devadas S.,A. Ghosh and K. Keutzer, An observability-based code coverage metric[C]. IEEE/ACM Conf. on Computer-Aided Design(ICCAD-96). 1996. 418-425.
[136] R. Vemuri R. Kalyanaraman, Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming[J]. IEEE transaction on VLSI Systems, 1995. 3(2): p. 201-214.
[137] Corno F.,M.S. Reorda and G. Squillero, High-level observability for effective high-level ATPG[C]. 18th IEEE VLSI Test Symp. 2000. 411-416.
[138] White L. J. Cohen, E I, A domain strategy for computer program testing[J]. IEEE Transaction on Software Engineering, May 1980. SE-6(3): p. 247-257.
[139] 赵瑞莲, 软件测试方法研究[D]:[博士论文]. 2001, 中国科学院计算机技术研究所.
[140] Clarke J. L.A , A close look at domain testing[J]. IEEE Transaction on Software Engineering, July 1982. SE-8(4): p. 380-390.
[141] B.Jeng E. J., A simplified domain-testing strategy[J]. ACM Transactions on Software Engineering and Methodology, July 1994. 3(3): p. 254-270.
[142] Qiushuang Zhang Harris I.G., A domain coverage metric for the validation of behavioral VHDL descriptions[C]. Test Conference, 2000 Proceedings International. 302-308.
[143] Synopsys, HDL Compiler for VerilogReference Manual[DB/MT] V6.1. Synopsys Online Document U-2003.9 Volumes 1,2,4.
[144] IEEE, Standard Verilog Hardware Description Language[S]. IEEE Std. 1364-2001. 2001.
[145] 张文军,罗春 and 杨军, 基于 PLI 的 AC97 Codec 快速仿真模型设计[J]. 电子工程师, 2005 年 第 12 期.
[146] Qiushuang Zhang, Validation of behavioral hardware descriptions[D]:[博士论文]. 2003, University of Massachusetts Amherst.
[147] Synopsys. DesignWare DW_apb_uart Databook[DB/MT]. Version2.00e. 2003/10.
[148] Synopsys, VCS / VCS MX Coverage Metrics User Guide. Version 7.1.1[DB/MT]. 2003/10.
[149] Kroening D Clarke E, Checking consistency of C and Verilog using predicate abstraction and induction[C]. IEEE ICCAD-2004. 1004-1009.
[150] Jain P.P., Cost-effective co-verification using RTL-accurate C models[C]. Circuits and Systems 99. 1999. 460 - 463.
[151] Takach A.,B. Bowyer and T. Bollaert, C based hardware design for wireless applications[C]. Design, Automation and Test in Europe, 2005. 124 - 129.
[152] 罗琨,曹阳 and 尹建华, 数字专用集成电路设计中SystemC建模验证方法[J]. 武汉大学学报, 2002 年 6 月. 48(3): p. 306-310.
[153] Blaurock O., A systemC-based modular design and verification framework for C-model reuse in a HW/SW-codesign design flow[C]. Distributed Computing Systems Workshops, 2004. Proceedings. 24th International Conference on. 838-843.
[154] 庄明渊, 基于 ARM7TDMI 的 MPEG-4 视频解码的实现和优化[D]:[硕士论文].2005, 东南大学.
[155] Chen W H,Smith C H and Fralick S C, A fast computational algorithm for the discrete transform[J]. IEEE Trans on Communications, 1997. 19: p. 1004-1009.
[156] Turing A. M., Checking a Large Routine. Conference on High Speed Automatic Calculating Machines. June 1949. 67-69.
[157] Taylor Scott, Functional Verification of a Multiple-issue, Out-of-Order, Superscalar . 638-643. Alpha Processor The DEC Alpha 21264 Microprocessor[C]. esign Automation Conference. Jun 1998. 638-643.
[158] Abarbanel Y., FoCs - Automatic Generation of Simulation Checkers from Formal Speciation[C]. 12th International Conference on Computer-Aided Verification (CAV). Vol. olume 1855 of Lecture Notes in Computer Science. 2000.
[159] Accellera, Open Verification Library Reference Manual[EB/OL]. http://www.verificationlib.org. 2003.
[160] Accellera, Property Specification Language Reference Manual[EB/OL]. http://www.eda.org/vfv/docs/PSL-v1.1.pdf. 2004.
[161] Kausik Datta and P P Das, Assertion Based Verification Using HDVL[C]. Proceedings of the 17th International Conference on VLSI Design(VLSID ? 04). 2004.
[162] Andrews Jason R, Co-Verification of Hardware and Software for Arm SoC Design[M]. 2004, Burlington: Newnes. 134-137.
[163] Andrews Jason R, Co-Verification of Hardware and Software for Arm SoC Design[M]. 2004, Burlington: Newnes. 137-140.
[164] Ptolemy, The Ptolemy Project[EB/OL]. http://ptolemy.eecs.berkeley.edu/.
[165] MentorGraphics, SeamlessCVE5.0[EB/OL]. http://www.mentor.com/seamless.
[166] Synopsys, Co-CentricSystemStudio[EB/OL]. http://www.synopsys.com/products/cocentric_studio/.
[167] Hoffmann A. Kogel T., Meyr H., A framework for fast hardware-software co-simulation[C]. Design, Automation and Test in Europe Conference and Exhibition, 2001. 760 - 764.
[168] Hoffmann A. Kogel, T. Meyr, H., A framework for fast hardware-software co-simulation[C]. Design, Automation and Test in Europe Conference and Exhibition, 2001. 760 - 764.
[169] CoWare, CoWare N2C System Designer[EB/OL]. http://www.coware.com.
[170] TNI-Valiosys, Cosimate[EB/OLL]. http://www.tniworld.com/cosimate.asp.
[171] Fornaciari W. Sciuto, D. Salice, F., A two-level cosimulation environment[J]. IEEE Computer, 1997. 30(6): p. 109-11.
[172] Lahiri K. Raghunathan, A. Dey, S., System-level performance analysis for designing on-chip communication architectures[J]. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, June 2001. 20(6): p. 768-783.
[173] Morawice A. Ubar, R. Raik, J., Cycle-based simulation algorithms for digital systems using high-level decision diagrams[C], ed. Design Automation and Test in Europe Conference and Exhibition 2000. 743.
[174] Ubar R. Morawiec, A. Raik, J., Cycle-based simulation with decision diagrams[C]. Design, Automation and Test in Europe Conference and Exhibition 1999. 454 - 458.
[175] Kei-Yong Khoo Willson A.N., Jr., Cycle-based timing simulations using event-streams[C]. Computer Design: VLSI in Computers and Processors, 1996. 460 -465.
[176] McKinney M.D., Integrating Perl, Tcl and C++ into simulation-based ASIC verification environments[C]. High-Level Design Validation and Test Workshop, 2001. Proceedings. Sixth IEEE International. 19 - 24.
[177] Sarmento A.,Cesario W. and Jerraya A.A., Automatic building of executable models from abstract SoC architectures made of heterogeneous subsystems[C]. Rapid System Prototyping, 2004. Proceedings. 15th IEEE International Workshop on. 88 - 95.
[178] A. Wadekar S., A RT level verification method for SoC designs[C]. IEEE SOC Conference 2003. 29-32.
[179] Jindal R Jain K., Verification of transaction-level SystemC models using RTL testbenches[C]. Formal Methods and Models for Co-Design, 2003. 199-203.
[180] P.P. Jain, Cost-effective co-verification using RTL-accurate C models[C]. Circuits and Systems 99. 1999. 460 - 463.
[181] Chen Shi Hua Shenghua Lien Y.E. Using the C language to reduce the design cycle of an MPEG-2 video IC: a case study. in 2nd International Conference on ASIC. 19996: IEEE.
[182] Takach A. Bowyer, B. Bollaert, T., C based hardware design for wireless applications[C]. Design, Automation and Test in Europe, 2005. 124 - 129.
[183] Formaggio L. Fummi, F. Pravadelli, G., A timing-accurate HW/SW cosimulation of an ISS with SystemC[C]. International Conference on Hardware/Software Codesign and System Synthesis, 2004. 152 - 157.
[184] Liem C. Nacabal, F. Valderrama, C. Paulin, P. Jerraya, A., System-on-a-chip cosimulation and compilation[J]. Design & Test of Computers, IEEE, April-June 1997. 14(2): p. 16-25.
[185] Greaves D.J., A Verilog to C compiler[C]. 11th International Workshop on Rapid System Prototyping, 2000. 122-127.
[186] ARM, ARM Developer Suite Debug Targut Guide[M/CD]. 1.1 ed. 2001: ARM Limited.
[187] 王镇, SoC 系统的高层建模[D]:[硕士论文], in 电子工程系. 2005, 东南大学.
[188] Wilson Snyder Paul Wasson, Duane Galbi, Verilator - Convert Verilog code to C++/SystemC[EB/OL]. http://www.veripool.com/verilator_doc.html.
[189] ARM, MM_synopsys_vcs_verilog.txt[M/CD]. 2002: ARM.
[190] 张拥军, 基于 Specman Elite 验证平台的 Garfield III 功能验证[D]:[硕士论文], in 电子工程系. 2004, 东南大学.
[191] Rafael C.Gonzalez Richard E.Woods, Digital Image Processing. 2th ed. 2002.7: Publishing House of Electronics Industry.
[192] 朱永峰, 多媒体加速器的研究及设计[D]:[硕士论文], in 电子工程系. 2004, 东南大学.