Средства функциональной верификации микропроцессоров

Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа схем, верификация остается самым узким местом процесса разработки (на нее тратится около 70% всех ресурсов проектирования). В работе делается краткий обзор средств верификации микропроцессоров, рассматриваются проблемы, возникающие в промышленной практике, анализируются возможные пути их решения. Значительная часть статьи посвящена исследованиям по верификации аппаратуры, проводимым в ИСП РАН: подводятся итоги выполненных работ, описываются текущие разработки, формулируются направления дальнейших исследований.

микропроцессоры, цифровая аппаратура, верификация, валидация, тестирование, генерация тестов, моделирование, языки описания архитектуры, распараллеливание

1. В.В. Кулямин. Методы верификации программного обеспечения, 2008. 111 с. (http://www.ispras.ru/~kuliamin/docs/VerMethods-2008-ru.pdf)

2. Статистика числа транзисторов в микропроцессорах — http://en.wikipedia.org/wiki/Transistor_count

3. А.С. Камкин. Верификация микропроцессоров: борьба с ошибками и управление качеством. Электроника: НТБ, №3, 2010. С. 98-104.

4. J. Bergeron. Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, 2000. 354 p.

5. G.E. Moore. Cramming More Components onto Integrated Circuits. Electronics Magazine, 86(1), 1965. P. 82-85. (http://www.cs.utexas.edu/~fussell/courses/cs352h/papers/moore.pdf)

6. B. Bentley. Validating the Intel® Pentium 4® Microprocessor. Design Automation Conference (DAC), 2001. P. 244-248.

7. B. Bentley. Validating a Modern Microprocessor. International Conference on Computer Aided Verification (CAV), 2005. P. 2-4. (http://www.cav2005.inf.ed.ac.uk/bentley_CAV_07_08_2005.ppt)

8. FDIV Replacement Program: Description of the Flaw — http://www.intel.com/support/processors/pentium/sb/CS-013007.htm

9. Revision Guide for AMD Family 10h Processors. Revision 3.84, August 2011. (http://developer.amd.com/wordpress/media/2012/10/41322.pdf)

10. S. Barak. Intel Denies Core i7 TLB Bug. The Inquirer, December 02 2008. (http://www.theinquirer.net/inquirer/news/1049427/intel-denies-core-i7-tlb-bug)

11. Intel® Core™ i7-900 Desktop Processor Extreme Edition Series and Intel® Core™ i7-900 Desktop Processor Series. Specification Update, May 2011. (http://download.intel.com/design/processor/specupdt/320836.pdf)

12. E.M. Clarke, J.M. Wing. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4), 1996. P. 626-643.

13. J. Harrison. Formal Methods at Intel — An Overview. Second NASA Formal Methods Symposium (NFM), 2010. (http://www.cl.cam.ac.uk/~jrh13/slides/nasa-14apr10/slides.pdf)

14. P. McLellan. History of Formal Verification at Intel. DAC Blog, December 05 2012. (http://blog.dac.com/post/2012/12/05/History-of-Formal-Verification-at-Intel.aspx)

15. R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore, S. Pandav, A. Slobodová, C. Taylor, V. Frolov, E. Reeber, A. Naik. Replacing Testing with Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation. International Conference on Computer Aided Verification (CAV), 2009. P. 414-429.

16. J. Bhadra, M. Abadir, S. Ray, L. Wang. A Survey of Hybrid Techniques for Functional Verification. IEEE Design & Test of Computers, 24(22), 2007. P. 112-122.

17. Z. Navabi. Languages for Design and Implementation of Hardware. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

18. S. Mikhani, Z. Navabi. System Level Design Languages. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

19. P. Mishra, N. Dutt (Eds.). Processor Description Languages. Systems on Silicon. Morgan Kaufmann, 2008. 432 p.

20. В. Кулямин. Перспективы интеграции методов верификации программного обеспечения. Труды ИСП РАН, 16, 2009. С. 73-88.

21. S. Agbaria, D. Carmi, O. Cohen, D. Korchemny, M. Lifshits, A. Nadel. SAT-Based Semiformal Verification of Hardware. Formal Methods in Computer-Aided Design (FMCAD), 2010. P. 25-32.

22. H. Jain, D. Kroening, N. Sharygina, E. Clarke. VCEGAR: Verilog Counterexample Guided Abstraction Refinement Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007. P. 583-586.

23. A. Kamkin, S. Smolov, I. Melnichenko. Static Analysis of HDL Descriptions: Extracting Models for Verification. East-West Design and Test Symposium (EWDTS), 2013. P. 184-187.

24. W.K. Lam. Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, 2005. 624 p.

25. N. Bombieri, F. Fummi, G. Pravadelli, J. Marques-Silva. Towards Equivalence Checking between TLM and RTL Models. IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2007. P. 113-122.

26. Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, G. Shurek. Constraint-Based Random Stimuli Generation for Hardware Verification. AI Magazine, 28(3), 2007. P. 13-30.

27. Технология верификации UVM — http://www.accellera.org/community/uvm

28. А.В. Баранцев, И.Б. Бурдонов, А.В. Демаков, С.В. Зеленов, А.С. Косачев, В.В. Кулямин, В.А. Омельченко, Н.В. Пакулин, А.К. Петренко, А.В. Хорошилов. Подход UniTesK к разработке тестов: достижения и перспективы. Труды ИСП РАН, 5, 2004. C. 151-156.

29. K. Sen, G. Rosu. Generating Optimal Monitors for Extended Regular Expressions. Electronic Notes in Theoretical Computer Science, 89(2), 2003. P. 162-181.

30. В.П. Иванников, А.С. Камкин, А.С. Косачев, В.В. Кулямин, А.К. Петренко. Использование контрактных спецификаций для представления требований и функционального тестирования моделей аппаратуры. Программирование, № 5, 2007. C. 47-61.

31. H. Barringer, D. Rydeheard, K. Havelund. Rule Systems for Run-Time Monitoring: From Eagle to RuleR. International Workshop on Runtime Verification, 2007. P. 111-125.

32. A. Bauer, M. Leucker, C. Schallhart. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, 20(4), 2011. P. 14:1-14:64.

33. A. Pnueli. Temporal Logic of Programs. Symposium on Foundation of Computer Science (SFCS), 1977. P. 46-57.

34. R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Vardi, Y. Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2002. P. 296-311.

35. OpenVera® Language Reference Manual: Assertions. Version 1.4.1, November 2004.

36. -2010 — IEEE Standard for Property Specification Language (PSL), 2010.

37. -2011 — IEEE Standard for the Functional Verification Language e, 2011.

38. -2012 — IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, 2013.

39. A. Pizialli. Functional Verification Coverage Measurement and Analysis. Kluwer Academic Publishers, 2004. 216 p.

40. M. Chupilko, A. Kamkin. A TLM-Based Approach to Functional Verification of Hardware Components at Different Abstraction Levels. Latin American Test Workshop (LATW), 2011. P. 1-6.

41. A. Adir, E. Almog, L. Fournier, E. Marcus, M. Rimon, M. Vinov, A. Ziv. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. IEEE Design & Test of Computers, 21(2), 2004. P. 84-93.

42. А.С. Камкин. Генерация тестовых программ для микропроцессоров. Труды ИСП РАН, 14(2), 2008. C. 23-63.

43. Тестовая программа PARANOIA — http://people.sc.fsu.edu/~%20jburkardt/c_src/paranoia/paranoia.html

44. А.С. Камкин, Т.И. Сергеева, С.А. Смолов, А.Д. Татарников, М.М. Чупилко. Расширяемая среда генерации тестовых программ для микропроцессоров. Программирование, № 1, 2014. (в печати)

45. Слайды по генератору тестовых программ RAVEN — http://www.slideshare.net/DVClub/introducing-obsidian-software-and-ravengcs-for-powerpc

46. I.V. Gribkov, A.V. Zakharov, P.P. Koltsov, N.V. Kotovich, A.A. Kravchenko, A.S. Koutsaev, A.S. Osipov, I.S Khisambeev. INTEG: A Stochastic Testing System for Microprocessor Verification. WSEAS International Conference on Circuits, Systems, Signal and Telecommunications (CSST), 2007. P. 55-59.

47. Страница инструмента MicroTESK — http://forge.ispras.ru/projects/microtesk

48. Страница инструмента Genesys-Pro — https://www.research.ibm.com/haifa/projects/verification/genesys_pro/index.shtml

49. P. Mishra, N. Dutt. Specification-Driven Directed Test Generation for Validation of Pipelined Processors. ACM Transactions on Design Automation of Electronic Systems, 13(3), 2008. P. 1-36.

50. T.N. Dang, A. Roychoudhury, T. Mitra, P. Mishra. Generating Test Programs to Cover Pipeline Interactions. Design Automation Conference (DAC), 2009. P. 142-147.

51. N. Mokhoff. Intel, Motorola Report Formal Verification Gains. EE Times, June 21 2001. (http://www.eetimes.com/document.asp?doc_id=1215957)

52. Страница инструмента CTESK — http://forge.ispras.ru/projects/ctesk

53. В.П. Иванников, А.С. Камкин, В.В. Кулямин, А.К. Петренко. Применение технологии UniTesK для функционального тестирования моделей аппаратного обеспечения. Препринт ИСП РАН, 2005. 16 с.

54. Д.Н. Воробьев, А.С. Камкин. Генерация тестовых программ для подсистемы управления памятью микропроцессора. Труды ИСП РАН, 17, 2009. С. 119-132.

55. С.И. Аряшев, А.С. Камкин, Б.Ю. Рогаткин. Тестирование RTL-моделей аппаратуры с помощью технологии UniTESK на примере блока преобразования адресов микропроцессора. Электроника, микро- и наноэлектроника, 2007. С. 183-187.

56. I. Bourdonov, A. Kossatchev, A. Petrenko, D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. Formal Methods. World Congress on Formal Methods in the Development of Computing Systems (FM), 1, 1999. P. 608-621.

57. И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. Программирование, № 5, 2003. C. 11-30.

58. И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. Программирование, № 1, 2004. С. 4-24.

59. B. Meyer. Design by Contract. Technical Report TR-EI-12/CO, Interactive Software Engineering Inc, 1986.

60. R.W. Floyd. Assigning Meaning to Programs. Symposium on Applied Mathematics, 1967. P. 19-32.

61. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 1969. P. 576-585.

62. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. 217 p.

63. V. Kuliamin, A. Petrenko, N. Pakoulin, A. Kossatchev, I. Bourdonov. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. Perspectives of System Informatics, 2003. P. 450-461.

64. A. Kamkin. Contract Specification of Pipelined Designs: Application to Testbench Automation. Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2007. P. 7-13.

65. A. Kamkin. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications. East-West Design & Test Symposium (EWDTS), 2008. P. 84-87.

66. А.С. Камкин. Метод формальной спецификации аппаратуры с конвейерной организацией и его приложение к задачам функционального тестирования. Труды ИСП РАН, 16, 2009. C. 107-128.

67. M. Chupilko, A. Kamkin. Developing Cycle-Accurate Contract Specifications for Synchronous Parallel-Pipeline Hardware: Application to Verification. Baltic Electronics Conference (BEC), 2010. P. 185-188.

68. M. Chupilko, A. Kamkin. Specification-Driven Testbench Development for Synchronous Parallel-Pipeline Designs. NORCHIP, 2009. P. 1-4.

69. M. Chupilko, A. Kamkin. Contract Specification of Hardware Designs at Different Abstraction Levels: Application to Functional Verification. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2010. P. 125-129.

70. А.В. Хорошилов. Спецификация и тестирование систем с асинхронным интерфейсом. Препринт ИСП РАН, 2006. 139 с.

71. А.С. Камкин, М.М. Чупилко. Тестирование модулей арифметики с плавающей точкой микропроцессоров на соответствие стандарту IEEE 754. Труды ИСП РАН, 14(2), 2008. С. 7-22.

72. М. Chupilko, A. Kamkin, D. Vorobyev. Methodology and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications. Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2008. P. 25-31.

73. Р.А. Баратов, А.С. Камкин, В.М. Майорова, А.Н. Мешков, А.А. Сортов, М.А. Якушева. Трудности модульной верификации аппаратуры на примере буфера команд микропроцессора «Эльбрус-2S». Вопросы радиоэлектроники, № 3, 2013. С. 84-96.

74. E. Dijkstra. Guarded Commands, Non-determinacy and Formal Derivation of Programs. Communications of the ACM, 18(8), 1975. P. 453-457.

75. D.L. Rosenband, Arvind. Hardware Synthesis from Guarded Atomic Actions with Performance Specifications. International Conference on Computer-Aided Design (ICCAD), 2005. P. 784-791.

76. BluespecTM SystemVerilog Reference Guide, 2012.

77. C. Clare. Designing Logic Systems Using State Machines. McGraw-Hill, 1973. 150 p.

78. S. Baranov. Logic and System Design of Digital Systems. TUT Press, 2008. 266 p.

79. В.П. Иванников, А.С. Камкин, М.М. Чупилко. Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс. Tools & Methods of Program Analysis (TMPA), 2013. С. 71-82.

80. M. Chupilko, A. Kamkin. Runtime Verification Based on Executable Models: On-the-Fly Matching of Timed Traces. Model-Based Testing Workshop (MBT), 2013. P. 67-81.

81. Страница инструмента C++TESK — http://forge.ispras.ru/cpptesk

82. G. von Bochmann, S. Haar, C. Jard, G.V. Jourdan. Testing Systems Specified as Partial Order Input/Output Automata. International Conference on Testing of Software and Communicating Systems (TestCom), 2008. P. 169-183.

83. И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. Использование конечных автоматов для тестирования программ. Программирование, 26(2), 2000. С. 61-73.

84. И.Б. Бурдонов, С.Г. Грошев, А.В. Демаков, А.С. Камкин, А.С. Косачев, А.А. Сортов. Параллельное тестирование больших автоматных моделей. Вестник ННГУ, № 3, 2011. C. 187-193.

85. A. Demakov, A. Kamkin, A. Sortov. High-Performance Testing: Parallelizing Functional Tests for Computer Systems Using Distributed Graph Exploration. Open Cirrus Summit, 2011.

86. И.Б. Бурдонов, А.С. Косачев. Обход неизвестного графа коллективом автоматов. Научный сервис в сети Интернет: все грани параллелизма, 2013. C. 228-232.

87. А.В. Демаков, С.А. Зеленова, С.В. Зеленов. Тестирование парсеров текстов на формальных языках. Программные системы и инструменты: Тематический сборник факультета ВМиК МГУ, № 2, 2001. С. 150-156.

88. С.В. Зеленов, С.А. Зеленова, А.С. Косачев, А.К. Петренко. Применение модельного подхода для автоматического тестирования оптимизирующих компиляторов, 2003.( http://citforum.ru/SE/testing/compilers)

89. L.-M. Wu, K. Wang, C.-Y. Chiu. A BNF-Based Automatic Test Program Generator for Compatible Microprocessor Verification. ACM Transactions on Design Automation of Electronic Systems, 9(1), 2004. P. 105-132.

90. А.С. Камкин. Некоторые вопросы автоматизации построения тестовых программ для модулей обработки переходов микропроцессоров. Труды ИСП РАН, 18, 2010. С. 129-149.

91. Д.Н. Воробьев, А.С. Камкин. Генерация тестовых программ для микропроцессоров на основе шаблонов конвейерных конфликтов. Труды ИСП РАН, 18, 2010. С. 91-113.

92. MIPS64™ Architecture For Programmers, Revision 2.0. MIPS Technologies Inc, June 9 2003.

93. RM7000 Family User Manual. Issue 1, May 2001.

94. А.С. Камкин. Комбинаторная генерация тестовых программ для микропроцессоров на основе моделей. Препринт ИСП РАН, 2008. 18 с.

95. A. Kamkin, E. Kornykhin, D. Vorobyev. Reconfigurable Model-Based Test Program Generator for Microprocessors. International Conference on Software Testing, Verification and Validation Workshops (ICSTW), 2011. P. 47-54.

96. A. Kamkin, A. Tatarnikov. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2012. P. 64-69.

97. M. Freericks. The nML Machine Description Formalism. Techical Report. TU Berlin, FB20, Bericht, 1991/15. 47 p.

98. Страница компании Target Compiler Technologies — http://www.retarget.com

99. S. Chandra, R. Moona. Retargetable Functional Simulator using High Level Processor Models. VLSI Design, 2000. P. 424-429.

100. Страница инструмента GLISS — http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=54

101. H. Cassé, J. Barre, R. Vaillant, P. Sainrat. Fast Instruction-Accurate Simulation with SimNML. Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO), 2011. P. 8-12.

102. A. Kamkin, T. Sergeeva, A. Tatarnikov, A. Utekhin. MicroTESK: An Extendable Framework for Test Program Generation. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2013. P. 51-57.

103. Язык программирования Ruby — http://www.ruby-lang.org

104. E. Kornykhin. SMT-Based Test Program Generation for Cache-Memory Testing. East-West Design & Test Symposium (EWDTS), 2009. P. 124-127.

105. E. Kornykhin. Generation of Test Data for Verification of Caching Mechanisms and Address Translation in Microprocessors. Programming and Computing Software, 36(1), 2010. P. 28-35.

106. J. Brandt, M. Gemünde, K. Schneider, S. Shukla, J.-P. Talpin. Integrating System Descriptions by Clocked Guarded Actions. Forum on Design Languages, 2011. P. 1-8.

107. G. Guglielmo, L. Guglielmo, F. Fummi, G. Pravadelli. Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs. Journal of Electronic Testing, 27(2), 2011. P. 37-162.

108. B. Karaçali, K.-C. Tai, M.A. Vouk. Deadlock Detection of EFSMs using Simultaneous Reachability Analysis. Dependable Systems and Networks (DSN), 2000. P. 315-324.

109. А.К. Ким, В.И. Перекатов, С.Г. Ермаков. Микропроцессоры и вычислительные комплексы семейства «Эльбрус». СПб.: Питер, 2013. 272 с.

110. Сайт ресурсов UML — http://www.uml.org

111. S. Chatterjee, M. Kishinevsky, U. Ogras. xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification. IEEE Design & Test of Computers, 2011. P. 80-88.

112. G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. 608 p.

113. А.С. Камкин, М.В. Петроченков. Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов. Вопросы радиоэлектроники, серия ЭВТ, 2014. (в печати)

114. K. Schneider, T. Kropf. A Unified Approach for Combining Different Formalisms for Hardware Verification. International Conference on Formal Methods in Computer Aided Design (FMCAD), 1996. P. 202-217.

115. B. Dutertre, L. Moura. The YICES SMT Solver, 2006. (http://yices.csl.sri.com/tool-paper.pdf).

116. L. Moura, N. Bjørner. Z3: An Efficient SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. P. 337-340.

117. K.L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993. 194 p.

118. Библиотека Java Constraint Solver API — http://forge.ispras.ru/projects/solver-api

119. D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial. GrammaTech, Inc., Version 1.1, 2011.

120. Страница инструмента ZamiaCAD — http://zamiacad.sourceforge.net