Построение тестовых программ для проверки подсистем управления памяти микропроцессоров тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Корныхин, Евгений Валерьевич

• Корныхин, Евгений Валерьевич
• кандидат физико-математических наук
• 2010

Оглавление диссертации кандидат физико-математических наук Корныхин, Евгений Валерьевич

Введение

1 Исследование методов построения тестовых программ

1.1 Системное тестирование микропроцессоров.

1.2 Тестирование подсистем управления памяти.

1.3 Методы целенаправленного построения тестовых программ

1.3.1 Методы на основе массовой генерации тестовых программ

1.3.2 Методы непосредственного построения тестовых программ.

1.4 Анализ существующих методов целенаправленного построения тестовых программ.

1.5 Уточненная постановка задачи.

2 Описание предлагаемых методов и моделей

2.1 Подход к генерации тестовых программ.

2.2 Моделирование устройств подсистемы управления памяти и вариантов исполнения инструкций

2.3 Метод построения ограничений.

2.3.1 Алгоритмы.

2.3.2 Таблицы вытеснения.

2.3.3 Существенно вытесняющие стратегии вытеснения

2.4 Новое определение стратегии вытеснения

Pseudo-LRU

2.5 Метод полезных обращений для записи стратегии вытеснения в виде ограничений.

2.5.1 Метод полезных обращений для стратегии вытеснения LRU

2.5.2 Метод полезных обращений для стратегии вытеснения FIFO.

2.5.3 Метод полезных обращений для стратегии вытеснения Pseudo-LRU

2.5.4 Разрешение ограничений, описывающих стратегии вытеснения

2.6 Конструирование текста тестовой программы.

3 Применение предлагаемых методов, сравнение с аналогамиЮЗ

3.1 Генерация тестов для архитектуры MIPS.

3.2 Генерация тестов для архитектуры PowerPC.

3.3 Генерация тестов для архитектуры IA-32.

3.4 Экспериментальная реализация программного средства для генерации тестовых программ.

3.5 Эксперименты по оценке допустимой сложности тестовых шаблонов

3.6 Сравнение с Genesys-Pro.

3.7 Сравнение с работами Intel.

Введение диссертации (часть автореферата) на тему «Построение тестовых программ для проверки подсистем управления памяти микропроцессоров»

Актуальность

Современные микропроцессоры — сложные многокомпонентные системы. Размеры современных микропроцессоров оцениваются как 107 — 108 вентилей[41]. Естественно при разработке таких сложных систем в проекты микропроцессоров вносятся ошибки, порой довольно критичные[20]. Поэтому для обнаружения этих ошибок в цикл разработки микропроцессора в обязательном порядке входят этапы функциональной верификации.

Чем позднее будут обнаружены ошибки в микропроцессорах, тем дороже обойдётся исправление ошибок: сделать это в готовой микросхеме, тем более выпущенной на рынок, практически невозможно. Тем актуальнее становятся методы обнаружения ошибок на ранних этапах разработки микропроцессоров. Цикл разработки предполагает подготовку микропроцессоров в виде исполнимых программных моделей на языках Уеп^ или УНБЬ[19]. Это делает возможным проведение функциональной верификации на таких моделях (т.е. до производства самих микропроцессоров) и актуальным исследование методов такой верификации. Целью функциональной верификации программных моделей микропроцессоров является обнаружение ошибок реализации функциональности в программных моделях микропроцессоров.

Выделяют следующие виды функциональной верификации: экспертизу, имитационное тестирование и формальную верификацию[10]. Экспертиза предполагает анализ текстов моделей экспертами с целью оценки их корректности и обнаружения ошибок. Этот вид функциональной верификации эффективно применяется на ранних стадиях разработки. Однако, ввиду наличия человеческого фактора, после экспертизы ошибки в микропроцессоре всё же остаются. Методы формальной верификации позволяют дать исчерпывающий ответ на вопрос о корректности отдельных модулей и всего микропроцессора. Однако трудоемкость формальной верификации чрезвычайно велика. Например, при разработке Intel Pentium 4 были формально верифицированы модуль работы с плавающей точкой (FPU), модуль декодирования инструкции и логика внеочередного выполнения (out-of-order), было найдено порядка 20 новых ошибок, однако трудоемкость этого проекта составила порядка 60 человеко-лет[20].

Имитационное тестирование позволяет ценой меньших усилий обнаружить значительную часть ошибок, в том числе критичных ошибок. Имитационное тестирование проводят для отдельных модулей (тогда оно называется модульным тестированием) и для всего микропроцессора в целом (тогда оно называется системным тестированием)^9]. Модули тестируются подачей на их входы специальных сигналов (модульных тестов) со снятием выходных сигналов и последующим анализом выходных сигналов. Входом при системном тестировании являются программы на машинном языке (тестовые программы). Проведение модульного тестирования требует кроме подготовки самих входных данных еще и подготовку тестирующей установки (testbench), выделение тестируемого модуля из всего проекта микропроцессора и т.п. Системное тестирование избавлено от этой необходимости. Поскольку размер и сложность отдельного модуля всегда меньше размера и сложности микропроцессора в целом, потенциально качество модульного тестирования может быть выше, чем системного. Однако для достижения высокого качества тестирования как число модульных тестов, так и совокупная трудоемкость их изготовления, получаются очень большими. Это вынуждает часть проверок проводить на модульном уровне, а другую часть на системном. Невысокая стоимость подготовки и проведения системного тестирования определила его наибольшую востребованность среди других методов функциональной верификации. Практически все разработчики микропроцессоров проводят системное тестирование.

Ключевым вопросом, определяющим качество тестирования, является вопрос выбора тестовых программ. Поскольку современные микропроцессоры обладают множеством инструкций (порядка сотен), длины конвейеров имеют порядок десятка стадий, количество различных состояний и ситуаций, в которых надо протестировать микропроцессор, измеряется десятками тысяч. Поэтому для тщательного системного тестирования нужно подобное же и количество тестовых программ. Это определяет актуальность задачи автоматического построения тестовых программ для системного тестирования.

Сложность микропроцессоров растет (увеличивается количество функциональных требований, количество ситуаций, в которых поведение микропроцессора должно обладать заданной спецификой). Это требует тестовых программ для проверки функциональных требований, которые не проверяются имеющимися тестовыми программами, и делает актуальными дальнейшие исследования в области построения тестов.

К числу наиболее сложных механизмов современных процессоров (поэтому наиболее подверженных ошибкам), использующих конвейеры и многоуровневые буферы типа кэш-памяти, относится механизм доступа к памяти. Поэтому актуальной является задача построения тестовых программ для проверки подсистем управления (механизмами) памяти микропроцессоров.

Цель работы

Целью диссертационной работы является исследование и разработка методов и программных средств построения тестовых программ для проверки подсистем управления памяти микропроцессоров.

Для достижения этой цели были поставлены следующие задачи:

1) исследовать описанные в научной литературе методы построения тестовых программ на предмет их применимости для системного тестирования подсистем управления памяти микропроцессоров;

2) разработать методы построения тестовых программ для системного функционального тестирования подсистем управления памяти.

Научная новизна

Научной новизной обладают следующие результаты работы: предложен подход к построению тестовых программ для проверки подсистем управления памяти микропроцессоров, сочетающий формализацию документации и технику ограничений;

2) предложен метод моделирования устройств подсистемы управления памяти, использующий конечные автоматы специального вида;

3) предложена формальная модель инструкций, описывающая отдельные пути их выполнения в виде утверждений о свойствах параметров инструкций и модельном состоянии устройств;

4) в рамках предложенного подхода разработан метод формализации механизма вытеснения данных при помощи построения ограничений, эффективно разрешаемых современным инструментарием.

Практическая значимость

Разработанные модели и методы могут быть использованы коллективами, занимающимися разработкой микропроцессоров, для автоматизации построения тестовых программ. Разработанный прототип системы построения тестовых программ использовался для генерации тестов подсистем управления памяти ряда микропроцессоров архитектуры М1Р864. Результаты работы могут быть использованы в исследованиях, которые ведутся в Институте системного программирования РАН, Московском государственном институте электроники и математики, НИИ системных исследований РАН, Институте точной механики и вычислительной техники им. С.А. Лебедева РАН, Институте проблем информатики РАН и других научных и промышленных организациях.

Публикации

По материалам диссертации опубликовано одиннадцать работ [3, 5, б, 8, 9, 11-13, 47-49], в том числе одна [11] в издании, входящем в перечень ведущих рецензируемых научных журналов и изданий ВАК.

Структура работы

Первая глава посвящена обзору существующих методов построения тестовых программ и подсистем управления памяти, их анализу и уточнению задач исследования. Вторая глава посвящена решению сформулированных в конце первой главы задач. В этой главе описываются предлагаемые модели и методы для построения тестовых программ. Третья глава посвящена оценке применимости предлагаемых во второй главе моделей для существующих практически важных архитектур микропроцессоров, описанию реализации программного средства для генерации тестовых программ и проводившихся на этой реализации экспериментов с целью оценки качества предлагаемых во второй главе методов.

Об обозначениях

Наиболее значимые утверждения помечены как «Теоремы», доказательства большинства из них помещены в приложении А. Менее значимые утверждения помечены как «Утверждения». Обоснования «Утверждений» обычно представлены непосредственно перед формулировкой «Утверждений». Вспомогательные утверждения помечены как «Леммы».

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Корныхин, Евгений Валерьевич

Основные результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:

1) Предложен подход к построению тестовых программ для проверки подсистем управления памяти микропроцессоров, позволяющий понизить сложность построения некоторого класса тестовых программ. Этот класс состоит из тестовых программ, в которых имеется цепочка длиной от 6 до 12 инструкций обращения к памяти. Понижение сложности обосновано при помощи ряда экспериментов на прототипе программного средства построения тестовых программ. Теоретически обоснована корректность алгоритмов в рамках предложенного подхода к построению тестовых программ. В рамках: предложенного подхода разработаны модели устройств подсистемы управления памяти и модели вариантов исполнения инструкций.

2) В рамках предложенного подхода разработан метод формализации механизма вытеснения данных, позволяющий в отличие от других методов моделрфования выразить ряд свойств вытесняемых данных в виде ограничений, причем эти ограничения эффективно разрешаются современным инструментарием. Теоретически обоснована корректность метода формализации для ряда стратегий вытеснения. Показано применение метода формализации к нескольким важным на практике стратегиям вытеснения.

Заключение

Список литературы диссертационного исследования кандидат физико-математических наук Корныхин, Евгений Валерьевич, 2010 год

1. http://wwwлntel.com/design/intaxch/papeгs/cache6.htm.

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

3. Корныхин, Е. В. Генерация тестовых данных для тестирования арифметических операций центральных процессоров / Е. В. Корныхин // Труды Института Системного Программирования. — 2008. — Т. 15. — С. 107-117.

4. Камкин, А. С. Комбинаторная генерация тестовых программ для микропроцессоров на основе моделей / А. С. Камкин // Препринт Института Системного Программирования РАН. — 2008. — Т. 21.

5. Корныхин, Е. В. Система генерации тестовых программ с использованием ограничений ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2009. — С. 39.

6. Корныхин, Е. В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции «Микроэлектроника и информатика». — 2009. — С. 87.

7. Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования микропроцессоров с учетом кэширования и трансляции адресов / Е. В. Корныхин // Труды Института Системного Программирования. — 2009. — Т. 17. — С. 145-160.

8. Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования fifo-кэш-памяти микропроцессоров / Е. В. Корныхин // Вычислительные методы и программирование. — 2009. — Т. 10.- С. 107-116.

9. Камкин, А. С. Функциональная верификация микропроцессоров: борьба с ошибками и управление качеством / А. С. Камкин // Электроника: Наука, Технология, Бизнес. — 2010. — по. 3.

10. Корныхин, Е. В. Генерация тестовых данных для тестирования механизмов кэширования и трансляции адресов микропроцессоров / Е. В. Корныхин // Программирование. — 2010. — Т. 36, № 1. — С. 40-49.

11. Корныхин, Е. В. Метод зеркальной генерации ограничений для построения тестовых программ по тестовым шаблонам / Е. В. Корныхин // Труды Института Системного Программирования. — 2010. — Т. 18. — С. 67-80.

12. Корныхин, Е. В. Определение стратегии вытеснения pseudolru на ветвях бинарного дерева /. Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2010. — С. 20-21.

13. Томпсон, Б. Управление памятью / Б. Томпсон // Computerworld Россия.— 2001.— № 22.

14. Касперски, К. Техника оптимизации программ. Эффективное использование памяти / К. Касперски. — СПб.: БХВ-Петербург, 2003. — Р. 560.

15. Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения / В. П. Иванников, А. С. Камкин,

16. В. В. Кулямин, А. К. Петренко. N0. 8.— М.: Препринт Института системного программирования РАН, 2005. — Р. 26.

17. Apt, K. R. Constraint Logic Programming using Eclipse / K. R. Apt, M. Wallace. — New York, NY, USA: Cambridge University Press, 2007.

18. Ashenden, P. J. The Designer's Guide to VHDL / P. J. Ashenden. — Elsevier, 2008.

19. Bentley, B. Validating the intel pentium 4 processor / B. Bentley, R. Gray // Intel Technology Journal. — 2001.

20. Borger, E. Abstract State Machines: A Method for High-Level System Design and Analysis / E. Borger, R. Stark. — Springer-Verlag, 2003.

21. Clarke, E. M. Model Checking / E. M. Clarke, O. Grumberg, D. A. Peled.— Cambridge, MA: MIT Press, 1999.

22. Evaluation of cardinality constraints on smt-based debugging / A. Sülflow, R. Wille, G. Fey, R. Drechsler // Multiple-Valued Logic, IEEE International Symposium on. — 2009. Vol. 0. - Pp. 298-303.

23. Expression: A . language for architecture exploration through compiler/simulator retargetability. / A. Halambi, P. Grun, V. Ganesh et al. // Proceedings of the European Conference on Design, Automation and Test. 1999. - Pp. 485-490.

24. Fallah, F. A new functional test program generation methodology / F. Fallah, K. Takayama // Proceedings 2001 IEEE International Conference on Computer Design: VLSI in Computers and Processors.— 2001.— Pp. 76-81.

25. Formal verification of backward compatibility of microcode / T. Arons,

26. E. Elster, L. Fix et al. // Lecture Notes in Computer Science. — 2005. — Vol. 3576/2005.-Pp. 185-198.

27. Frey, B. PowerPC Architecture Book / B. Frey. — IBM, 2005.

28. Fully automatic test program generation for microprocessor cores /

29. F. Corno, G. Cumani, S. M. Reorda, G. Squillero // DATE '03: Proceedings of the conference on Design, Automation and Test in Europe. — Washington, DC, USA: IEEE Computer Society, 2003.- P. 11006.

30. Functional verification of the equator maplOOO microprocessor / J. Shen, J. Abraham, D. Baker et al. // DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference. — New York, NY, USA: ACM, 1999. — Pp. 169-174.

31. Functional verification of the hp pa 8000 processor / S. T. Mangelsdorf, R. E Gratias, R. M. Blumberg, R. Bhatia // Hewlett-Packard Journal — 1997. — август. — Pp. 1-13.

32. Genesys-pro: Innovations in test program generation for functional processor verification / A. Adir, E. Almog, L. Fournier et al. // IEEE Design and Test of Computers. — 2004. — Mar/Apr. Vol. 21, no. 2. — Pp. 84-93.

33. Genetic Programming — An Introduction / W. Banzhaf, P. Nordin, R. Keller, F. Francone. — Morgan Kaufmann, 1998.

34. Grund, D. Estimating the performance of cache replacement policies /

35. D. Grund, J. Reineke // 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), June 57, 2008, Anaheim, С A, USA. 2008. - Pp. 101-112.

36. Hennenhoefer, E. The Evolution of Processor Test Generation Technology /

37. E. Hennenhoefer, M. Typaldos. — Obsidian Software Inc.

38. Hennessy, J. L. Computer architecture: a quantitative approach / J. L. Hennessy, D. A. Patterson, A. C. Arpaci-Dusseau. — 4 edition.— Morgan Kaufmann, 2007.

39. Ho, C.-M. R. Validation tools for complex digital designs: Tech. rep. / CM. R. Ho: 1996.

40. IA-32 Intel Architecture Software Developer's Manual. — Intel, 2006.

41. Industrial experience with test generation languages for processor verification / A. Adir, E. Almog, L. Fournier et al. // IEEE Design and Test of Computers. — 2004. — Mar./Apr. — Vol. 21, no. 2. — Pp. 84-93.

42. Kohno, K. A new verification methodology for complex pipeline behavior / K. Kohno, N. Matsumoto // Proceedings of the 38st Design Automation Conference (DAC'01). — 2001.

43. Koo, H.-M. Functional test generation using design and property decomposition techniques / H.-M. Koo, P. Mishra // ACM Transactions on Embedded Computer Systems. — 2009. — Vol. 8, no. 4.

44. Kornikhin, E. Test data generation for arithmetic subsystem of cpus mips64 / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. — 2008. — Vol. 2. — Pp. 43-46.

45. Kornikhin, E. Smt-based test program generation for cache-memory testing / E. Kornikhin // Proceedings of East-West D T S.— 2009.— Pp. 124-127.

46. Kornikhin, E. Test data generation for lru cache-memory testing / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. — 2009. — Pp. 88-92.

47. Maatg: A functional test program generator for microprocessor verification / T. Li, D. Zhu, Y. Guo et al. // Proceedings of the 2005 8th Euromicro conference on Digital System Design (DSD'05). — 2005.

48. McMillan, K. L. Symbolic Model Checking / K. L. McMillan. — Kluwer Acadcmic Publishers, 1993.

49. MIPS Technologies. — MIPS64™ Architecture For Programmers. Volume II: The MIPS64™ Instruction Set, 2001.

50. MIPS Technologies. — MIPS64™ Architecture For Programmers. Volume III: The MIPS64™ Privileged Resource Architecture, 2001.

51. Mishra, P. Automatic functional test program generation for pipelined processors using model checking / P. Mishra, N. Dutt // High-Level Design, Validation, and Test Workshop, IEEE International. — 2002. — Vol. 0. — Pp. 99-103.

52. Mishra, P. Graph-based functional test program generation for pipelined processors / P. Mishra, N. Dutt //In Proceedings of Design Automation and Test in Europe (DATE. 2004. - Pp. 182-187.

53. Mishra, P. Functional coverage driven test generation for validation of pipelined processors / P. Mishra, N. Dutt. — 2005. — Pp. 678-683.

54. On the test of microprocessor ip cores / F. Corno, M. S. Reorda, S. Squillero, M. Violante // DATE '01: Proceedings of the conference on Design, automation and test in Europe. — Piscataway, NJ, USA: IEEE Press, 2001.-Pp. 209-213.

55. Pentium Pro Family Developer's Manual Volume 3: Operating System Writer's Guide. — Intel, 1996.

56. Petters, S. Intel architecture software developer's manual volume 3: System programming: Tech. rep. / S. Petters: 2001.

57. Powerpc g5 user's manual: Tech. rep.: IBM, 2008.

58. The RAISE specification language / C. George, P. Haff, K. Havelund et al. — Prentice Hall Europe, 1992.

59. Shiva, S. G. Computer design and architecture / S. G. Shiva. — 3d edition. — Atlantic/Little, Brown, 2000.

60. Ur, S. Micro architecture coverage directed generation of test programs / S. Ur, Y. Yadin // DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference.— New York, NY, USA: ACM, 1999.— Pp. 175-180.

61. Using a constraint satisfaction formulation and solution techniques for random test program generation / E. Bin, R. Emek, G. Shurek, A. Ziv // IBM Systems Journal. — 2002. Vol. 41, no. 3. - Pp. 386-402.

62. Wang, L.-T. Electronic Design Automation: Synthesis, Verification, and Test / L.-T. Wang, Y.-W. Chang, K.-T. Cheng. — Morgan Kaufmann, 2009.

63. Wood, B. A. Verifying a multiprocessor cache controller using random test generation / D. A. Wood, G. A. Gibson, R. H. Katz // IEEE Design and Test of Computers. 1990. - Vol. 7. - Pp. 13-25.

64. Yeager, K. C. The mips rlOOOO superscalar microprocessor / K. C. Yeager // IEEE Micro. — 1996. Vol. 16, no. 2. - Pp. 28-40.