Помощь в написании студенческих работ
Антистрессовый сервис

Динамическая верификация цифровой аппаратуры на основе формальных спецификаций

Диссертация: Динамическая верификация цифровой аппаратуры на основе формальных спецификаций
ДиссертацияПомощь в написанииУзнать стоимостьмоей работы

Традиционный метод динамической верификации состоит в следующем. Набор входных данных для проведения верификации {тестовая последовательность) описывается вручную или генерируется случайным образом, но в рамках ограничений, наложенных на значения отдельных элементов последовательности. Собственно проверка корректности поведения, задаваемого HDL-описанием, оценивается на основе утверждений… Читать ещё >

Динамическая верификация цифровой аппаратуры на основе формальных спецификаций (реферат, курсовая, диплом, контрольная)

Содержание

  • ГЛАВА 1. ФУНКЦИОНАЛЬНАЯ ВЕРИФИКАЦИЯ ЦИФРОВОЙ АППАРАТУРЫ
    • 1. 1. Формальная верификация
    • 1. 2. Динамическая верификация
      • 1. 2. 1. Общая схема тестирования
      • 1. 2. 2. Уровень сложности тестируемого компонента
      • 1. 2. 3. Генерация тестовых воздействий
      • 1. 2. 4. Проверка реакций тестируемого компонента
      • 1. 2. 5. Оценка полноты тестирования
      • 1. 2. 6. Технологии создания тестовых систем
      • 1. 2. 7. Анализ существующих технологий
    • 1. 3. Уточнение задач диссертационной работы
    • 1. 4. Краткое введение в предлагаемый метод
  • ГЛАВА 2. МЕТОД ВЕРИФИКАЦИИ АППАРАТУРЫ
    • 2. 1. Уровни абстракции эталонной модели
    • 2. 2. Архитектура тестовой системы
      • 2. 2. 1. Архитектура тестового оракула
      • 2. 2. 2. Генерация стимулов
      • 2. 2. 3. Способ оценки полноты покрытия
      • 2. 2. 4. Применение подхода на разных уровнях абстракции
      • 2. 2. 5. Формализация работы тестового оракула
      • 2. 2. 6. Соединение нескольких тестовых систем
    • 2. 3. Классификация ошибок в аппаратуре
    • 2. 4. Результаты главы
  • ГЛАВА 3. РЕАЛИЗАЦИЯ МЕТОДА ВЕРИФИКАЦИИ АППАРАТУРЫ
    • 3. 1. Средства описания тестовых оракулов
      • 3. 1. 1. Описание сообщений
      • 3. 1. 2. Описание моделей интерфейсов
      • 3. 1. 3. Первичные арбитры реакций
      • 3. 1. 4. Вторичные арбитры реакций
      • 3. 1. 5. Создание класса модельного окружения и тестового оракула
    • 3. 2. Адаптер
      • 3. 2. 1. Адаптеры моделей входных и выходных интерфейсов
      • 3. 2. 2. Создание класса адаптера
    • 3. 3. Сценарий тестирования
      • 3. 3. 1. Сценарные функции
      • 3. 3. 2. Функция получения текущего состояния
    • 3. 4. Реализация функционального покрытия
    • 3. 5. Реализация объединения нескольких модулей
    • 3. 6. Реализация автоматического построения конечных автоматов
    • 3. 7. Результаты главы
  • ГЛАВА 4. РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ ПОДХОДА
    • 4. 1. Коммутатор данных северного моста
    • 4. 2. Системный контроллер прерываний
    • 4. 3. Устройство аппаратного поиска по таблице страниц
    • 4. 4. Буфер команд
    • 4. 5. Опыты по автоматическому построению конечных автоматов
    • 4. 6. Результаты верификации модулей
    • 4. 7. Результаты главы

Актуальность темы

.

Современная цифровая аппаратура на основе интегральных схем (ИС) представляет собой сложные устройства, проектирование и производство которых требует больших затрат ресурсов. Непосредственное изготовление ИС происходит с использованием наборов фотошаблонов, которые создаются на основе схемы соединений (net list). Схема соединений получается автоматически путем синтеза из модели, созданной на специализированном языке описания аппаратуры. В настоящее время проектирование моделей устройств осуществляется с помощью языков, называемых языками описания аппаратуры (.Hardware Description Language, HDL). Такие модели, основанные на HDL-описаниях, часто называют имитационными, так как они допускают их выполнение в специализированной среде имитационного моделирования — симуляторе.

Цена ошибки в аппаратуре может оказаться очень высокой: известный случай замены микропроцессоров Intel Pentium с ошибкой деления обошелся компании приблизительно в 500 миллионов долларов (Wolfe A. For Intel, it’s, а case ofFPU ail over again. ЕЕ Times, 1997. № 5). Так как исправление ошибок в уже готовых микросхемах невозможно, поиск и нахождение функциональных ошибок проводится на этапе проектирования HDL-описания устройства. Подобного рода деятельность, состоящая в проверке соответствия поведения аппаратуры, задаваемого HDL-описанием, его спецификации, называется верификацией. Верификация обычно требует до 70% от общих трудозатрат на создание всего устройства. Это обусловлено следующими причинами: логической сложностью HDL-описаний и ее постоянным увеличением (высокая степень параллелизма, асинхронность и большие размеры), существенной итеративностью процесса разработки HDL-описаний, требующего постоянной модификации тестов и HDL-описаний, меньшим уровнем модульности, чем в области программного обеспечения, фрагментарностью и неактуальностью документации.

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

Традиционный метод динамической верификации состоит в следующем. Набор входных данных для проведения верификации {тестовая последовательность) описывается вручную или генерируется случайным образом, но в рамках ограничений, наложенных на значения отдельных элементов последовательности. Собственно проверка корректности поведения, задаваемого HDL-описанием, оценивается на основе утверждений (assertions), а для оценки полноты верификации используются метрики на основе покрытия кода HDL-описания и покрытия комбинаций событий, возникающих в процессе выполнения HDL-описания в симуляторе {Open Verification Methodology User Guide [Электронный ресурс], 2011. URL: http://verificationacademy. com/file/ovm-2.1.2. zip).

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

Решению задачи тщательного тестирования НБЬ-описаний посвящено много работ. Многие из проблем, перечисленных выше, решены, например, в методе верификации ГГОЬ-описаний, основанном на формальных спецификациях, описывающих ожидаемое поведение тестируемой аппаратуры, в форме программных контрактов, наложенных на все операции и микрооперации (Камкин, А. С. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций, диссертация на соискание ученой степени кандидата физико-математических наук. М., 2009). Такие спецификации описывают ожидаемое поведение с потактовой точностью. Верификация в этом случае получается очень тщательной, так как вердикт касательно корректности НБЬ-описания выносится на основе и проверки данных, и проверки номера такта, на котором выполняемое в симуляторе НБЬ-описание выдало реакцию. Детальная документация, равно как и необходимость в столь тщательных проверках, появляется, как правило, на заключительных итерациях создания ЬГОЬ-описаний, поэтому наилучшее применение метод нашел именно на них. Требования метода к документации, а также сложность разработки спецификаций сделали его применение ограниченным: разработка потактовых спецификаций, которые к тому же не используют разработанные ранее на предыдущих этапах эталонные модели, занимает много ресурсов и времени, которых может и не остаться на заключительных итерациях проектирования.

Таким образом, ввиду важности и актуальности верификации ГГОЬ-описаний аппаратуры и отсутствия готовых решений, полностью удовлетворяющих промышленному применению на разных этапах проектирования, была поставлена задача исследования проблем верификации НБЬ-описаний. На основе анализа проблем необходимо предложить метод динамической верификации, учитывающий особенности как самих НБЬописаний, так и их процесса разработки, а именно: объективную сложность, инкрементальный процесс разработки, неполноту требований, особенно на ранних этапах проектирования.

Цель и задачи работы.

Основной целью работы является разработка метода верификации цифровой аппаратуры на основе формальных спецификаций в форме программных моделей с учетом требований промышленных процессов проектирования НОЬ-описаний. Для достижения цели работы были поставлены следующие задачи:

1. Провести анализ существующих методов верификации цифровой аппаратуры;

2. Разработать метод верификации НОЬ-описаний аппаратуры на основе использования эталонных программных моделей, допускающий:

• применение при неполноте требований;

• инкрементальный процесс разработки и уточнения формальных спецификаций в процессе проектирования;

• композицию тестовых систем различных ГГОЬ-описаний;

3. Разработать инструменты, реализующие метод;

4. Оценить реализацию метода на практике.

Основные результаты работы.

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

1. Разработан метод верификации цифровой аппаратуры, на основе формальных спецификаций в виде программных моделей на языке С++, отвечающий требованиям промышленных процессов проектирования НОЬ-описаний;

2. Разработан метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции;

3. Разработан метод сопоставления реакций цифровой аппаратуры и реакций эталонной модели, позволяющий автоматизировать процедуру проверки цифровой аппаратуры;

4. Реализованы инструменты, поддерживающие разработанные методы.

Научная новизна работы.

Научной новизной обладают следующие результаты работы:

1. Метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции;

2. Метод сопоставления реакций цифровой аппаратуры и реакций эталонной модели, позволяющий автоматизировать процедуру проверки цифровой аппаратуры.

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

На основе предложенного метода верификации были разработаны средства, позволяющие создавать тестовые системы на основе эталонных моделей на С++ на разных уровнях абстракции. Разработанные средства являются библиотекой классов на языке С++. Они были применены в 9 проектах верификации модулей промышленных микропроцессоров в течение 2009;2012 гг. В процессе верификации в среднем обнаруживалось 3−5 серьезных ошибок в модулях, прошедших верификацию другими методами. Продемонстрированы преимущества метода для поддержки итеративного процесса разработки.

Доклады и публикации.

Основные положения работы докладывались на следующих конференциях и семинарах:

• Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on.

Software Engineering, г. Нижний Новгород, 2010 г. и г. Екатеринбург, 2011 г.);

• Международный симпозиум «Восток-Запад: проектирование и тестирование» (EWDTS: East-West Design & Test Symposium, г. Санкт-Петербург, 2010 г. и г. Севастополь, 2011 г.);

• Международная конференция «Балтийская электронная конференция» (Baltic Electronics Conference, г. Таллин, 2010 г.);

• Семинар Института системного программирования РАН (г. Москва, 2011;2012 гг.).

По теме диссертации автором опубликованы работы [1]- [11] (из них 3 в изданиях из перечня ВАК), полно отражающие основные результаты работы.

Структура и объем диссертации

.

Работа состоит из введения, 4 глав, заключения и списка литературы (72 наименования). Основной текст диссертации (без приложений и списка литературы) занимает 120 страниц.

Заключение

.

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

1. Разработан метод верификации цифровой аппаратуры, на основе формальных спецификаций в виде программных моделей на языке С++, отвечающий требованиям промышленных процессов проектирования HDL-описаний;

2. Разработан метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции;

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

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

Благодарности. Автор выражает благодарность A.C. Камкину за неоценимый вклад в проведенную работу, без энтузиазма и оптимизма которого она бы не состоялась. Отдельную благодарность автор выражает коллегам по Институту, а также коллегам из НИИ Системных исследований РАН и ЗАО «МЦСТ», которые предоставили возможности и ресурсы для применения подхода на практике.

Показать весь текст

Список литературы

  1. А.С., Чупилко М. М. Механизмы поддержки функционального тестирования моделей аппаратуры на разных уровнях абстракции. II Труды ИСП РАН, т. 20, М., 2011, ISSN 2079−8156. с. 143−160.
  2. А., Чупилко М. Обзор современных технологий имитационной верификации аппаратуры. II Программирование, № 3, 2011. с. 42−49.
  3. М.М. Разработка тестовых систем для многомодульных моделей аппаратуры. II Программирование, № 1, 2012, с. 47−58.
  4. Chupilko М. C++TESK-SystemVerilog united approach to simulation-based verification of hardware designs. II Proceedings of EWDTS 2011: The 9th East-West Design & Test Symposium, 2011. pp. 136−139.
  5. Chupilko M. Developing test systems for multi-modules hardware designs. II Proceedings of SYRCoSE 2011: The 5th Spring Young Researchers Colloquium on Software Engineering, 2011. pp. 111−116.
  6. Kamkin A., Chupilko M. A TLM-based approach to functional verification of hardware components at different abstraction levels. II Proceedings of LATW 2011: The 12th Latin-American Test Workshop, 2011. pp. 1−6.
  7. Chupilko M., Kamkin A. Developing cycle-accurate contract specifications for synchronous parallel-pipeline hardware: application to verification. II Proceedings of ВЕС 2010: The 12th Biennial Baltic Electronics Conference, 2010. pp.185−188.
  8. Chupilko M. Models of Synchronous Hardware Designs Based on FSM at Different Abstraction Levels: Application to Functional Verification. II Proceedings of EWDTS 2010: The 8th East-West Design & Test Symposium, 2010. pp. 487−490.
  9. М.М. Автоматизация системного тестирования моделей аппаратуры на основе формальных спегщфикагщй. // Труды ИСП РАН, т. 18, М., 2010. с. 115−128.
  10. Chupilko М., Kamkin A. Specification-Driven Testbench Development for Synchronous Parallel-Pipeline Designs. // Proceedings of NorChip 2009: 27th Norchip Conference, 2009. pp. 1−4.
  11. Академик Лаврентьев M.A. Опыты жизни. 50 лет в науке Электронный ресурс]. URL: http://www.ipmce.ru/about/history/leading/lebedev/ remembrance/lavrentiev (дата последнего обращения: 21.03.2012 г.).
  12. П.Н. Синтез логических схем с использованием языка VHDL — М.: СОЛОН-Р, 2002, с. 8−54.
  13. IEEE Standard VHDL Language Reference Manual. IEEE Std 1076−2002.
  14. IEEE Standard Verilog hardware description language. IEEE Std 13 642 001.
  15. IEEE Standard for SystemVerilog: Unified Hardware Design, Specification and Verification Language. IEEE Std 1800−2005.
  16. IEEE Standard System С Language Reference Manual. IEEE Std 16 662 005.
  17. Wiemann A. Standardized Functional Verification, 2008 Springer Science+Business Media, LLC, Chapter 1, p.4.
  18. Intel Corp. Statistical Analysis of Floating Point Flaw: Intel White Paper Электронный ресурс], 1994. URL: http://support.intel.com/support/processors/ pentium/fdiv/wp (дата последнего обращения: 21.03.2012 г.).
  19. Moore G.E. Cramming more components onto integrated circuits. Electronics, 1965. pp. 114−117.
  20. Lam W. Hardware design verification: simulation and formal method-based approaches. Prentice Hall, 2005.
  21. Harrison J. Formal Verification In Industry (I) Электронный ресурс], 1999. URL: http://www.cl.cam.ac.uk/~jrhl3/slides/types-04sep99/slidesl .pdf (дата последнего обращения: 21.03.2012 г.).
  22. Iman S. Step-by-step Functional Verification with SystemVerilog and OVM. Hansen Brown Publishing, 2009.
  23. Ho C.-M.R. Validation tools for complex digital designs. PhD thesis, Stanford University, 1996.
  24. Foster H.D., Krolnik A.C., Lacey D.J. Assertion-based design. Kluwer Academic Publishers, 2004.
  25. Open Verification Methodology User Guide Электронный ресурс], 2011. URL: http://verificationacademy.eom/file/ovm-2.l.2.zip (дата последнего обращения 21.03.2012 г.).
  26. Larson K.D. Translation of an Existing VMM-based SystemVerilog Testbech to URM Электронный ресурс], 2007. URL: http://www.cdnusers.org/ community /incisive/vtpcdnlivesv2007mvplarsonpaperpdf.pdf (дата последнего обращения: 21.03.2012 г.).
  27. Rose A., Fitzpatrick Т., Rich D., Foster H. Advanced Verification Methodology Cookbook. Mentor Graphics Corporation, 2008.32. http://uvmworld.org сайт, посвященный методологии Universal Verification Methodology.
  28. Jonson N. UVMIs Not A Methodology Электронный ресурс], 2011. URL: http://www.agilesoc.com/uvm-is-not-a-methodology (дата последнего обращения: 21.03.2012 г.).
  29. Cai L., Gajski D. Transaction level modeling: an overview. II Proceedings of CODES+ISSS 2003: The International Conference on Hardware-Software Codesign and System Synthesis, 2003. pp. 19−24.
  30. Geist D., Farkas M., Landver A., Lichtenstein Y., Ur S., and Wolfsthal Y. Coverage directed test generation using symbolic techniques. II Proceedings of Formal Methods in Computer Aided Design, 1996.
  31. Ur S. and Yadin Y. Micro architecture coverage directed generation of test programs. II Proceedings of Design and Automation Conference, 1999.
  32. Mishra P. and Dutt N. Functional coverage driven test generation for validation ofpipelined processors. Proceedings of Design, Automation and Test in Europe Conference and Exhibition, 2005.
  33. Dang T.N., Roychoudhury A., Mitra Т., and Mishra P. Generating test programs to cover pipeline interactions. II Proceedings of Design and Automation Conference, 2009.
  34. Mishra P., Dutt N. Functional coverage driven test generation for validation of pipelined processors. II Proceedings of Design, Automation and Test in Europe Conference, 2005.
  35. Koo H.M., Mishra P. Test generation using SAT-based bounded model checking for validation of pipelined processors. II Proceedings of ACM Great Lakes Symposium on VLSI, 2006.
  36. Koo H.M., Mishra P. Functional test generation using property decomposition for validation of pipelined processors. II Proceedings of Design, Automation and Test in Europe Conference, 2006.
  37. Ho R.C., Yang C.H., Horowitz M.A., Dill D.L. Architecture validation for processors. II Proceedings of ISCA 1995: International Symposium on Computer Architecture, 1995. pp. 404−413.
  38. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. БХВ-Петербург, 2010.
  39. Clarke Е., Grumberg О. and Peled D., Model Checking, MIT Press, 1999.
  40. Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576−580,583 October 1969.
  41. Floyd R.W. Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics, 1967. v. 19, pp. 19−31.
  42. Bergeron J. Writing Testbenches Using SystemVerilog, Springer Science+Business Media, 2006.
  43. B.B., Петренко A.K., Косачев A.C., Бурдонов И. Б. Подход UniTesK к разработке тестов. Программирование, 29(6): 25−43, 2003.
  44. Bentley В, Gray R. Validating the Intel® Pentium® 4 Microprocessor Электронный ресурс], 2001. URL: http://download.intel.com/technology/itj/ ql2001/pdf/art3.pdf (дата последнего обращения 21.03.2012 г.).
  45. Ludden J.M. et al. Functional Verification of the POWER4 Microprocessor and POWER4 Multiprocessor Systems II IBM Journal of Research and Development, 2002, v. 46, № 1. pp. 53−76.
  46. А.С. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций. Диссертация на соискание ученой степени кандидата физико-математических наук. Москва, 2009.
  47. И.Б., Косачев А. С., Кулямин В. В. Использование конечных автоматов для тестирования программ. Программирование, 2000, № 2, стр. 12−28.
  48. И.Б. и др. Неизбыточные алгоритмы обхода ориентированных графов, Детерминированный случай. Программирование, 2003, № 5, стр. 11−30.
  49. И.Б. и др. Неизбыточные алгоритмы обхода ориентированных графов, • Недетерминированный случай. Программирование, 2004, № 1, стр. 4−24.
  50. А.В. Спецификация и тестирование систем с асинхронным интерфейсом. Препринт № 12. М.: Институт системного программирования РАН, 2006, стр. 140.
  51. Ur S., Yadin Y. Coverage Driven Processor Test Generation: Proof of Concept Электронный ресурс], 1997. URL: http://www.research.ibm.com/haifa/ dept/svt/papers/simulation/dac.ps (дата последнего обращения 21.03.2012 г.).
  52. Piziali A. Functional Verification Coverage Measurement And Analysis. Kluwer Academic Publishers, 2004.
  53. В.П., Камкин A.C., Кулямин B.B., Петренко А. К. Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения. // Препринт ИСП РАН, 2005.
  54. Jenihhin М., Raik J., Chepurov A., Ubar R. Simulation-based Verification with APRICOT Framework using High-Level Decision Diagrams. II Proceedings of EWDTS 2009: IEEE East-West Design & Test Symposium, 2009, pp.13−16.
  55. Spear С. SystemVerilog for Verification A Guide to Learning the Testbench Language Features. Springer Science+Business Media, LLC, 2008.62. http://www.unitesk.eom/content/category/7/14/33 страница, посвященная инструменту CTESK.
  56. Ubar R. Test Synthesis with Alternative Graphs. IEEE Design & Test of Computers, Spring 1996, pp. 48−57.
  57. Ubar R. Test Generation for Digital Systems on the Vector Alternative Graph Model II Proceedings of the 13th Symposium on Fault Tolerant Computing, Milano, Italy, 1983, pp. 374−377.
  58. Я.С., Камкин А. С., Чупилко М. М. Сравнительный анализ современных технологий разработки тестов для моделей аппаратного обеспечения II Труды ИСП РАН, 2009.
  59. Итеративная разработка Электронный ресурс]. URL: http://ш.wikipedia.org/wiki/Итepaтивнaяpaзpaбoткa (дата последнего обращения: 21.03.2012 г.).
Заполнить форму текущей работой

Сессия? Спокойно!