Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2017-29(4)-16

Полный текст:

Аннотация

Тестирование аппаратуры - это процесс, нацеленный на обнаружение неисправностей, внесенных в интегральные схемы в процессе производства. Для оценки качества таких тестов используют две основные метрики: способность обнаруживать ошибки (покрытие ошибок) и время тестирования (длина теста). Известно множество методов генерации тестов, однако масштабируемого решения, применимого к сложной цифровой аппаратуре, нет до сих пор. В данной статье анализируется возможность использования функциональных тестов, построенных по высокоуровневым моделям (прежде всего, моделям уровня регистровых передач), для низкоуровневого производственного тестирования. Рассматривается конкретный метод генерации тестов, использующий технику проверки моделей (model checking). Входной информацией выступает HDL-описание. Метод состоит из двух ключевых шагов: построение модели системы и построение модели покрытия. Указанные модели автоматически извлекаются из HDL-описания. Модель системы представлена в виде высокоуровневых решающих диаграмм. Модель покрытия - это множество LTL-формул, определяющих условия достижимости переходов расширенного конечного автомата, описывающего систему. Построенные модели транслируются во входной формат инструмента проверки моделей (model checker), который для каждой формулы модели покрытия генерирует контрпример - вычисление, нарушающее эту формулу, то есть приводящее к срабатыванию соответствующего перехода автомата. Изначально рассматриваемый метод предназначался для покрытия всех путей исполнения HDL-описания и обнаружения недостижимого кода. Экспериментальное сравнение метода с существующими аналогами показало, что он строит более короткие тесты, однако эти тесты достигают меньшего уровня покрытия константных неисправностей, чем тесты, построенные с помощью специальных средств. В статье предлагается модификация метода для преодоления указанного недостатка.

Об авторах

М. М. Чупилко
Институт системного программирования РАН
Россия


А. С. Камкин
Институт системного программирования РАН; Московский государственный университет им. М.В. Ломоносова; Московский физико-технический институт
Россия


М. С. Лебедев
Институт системного программирования РАН
Россия


С. А. Смолов
Институт системного программирования РАН
Россия


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

1. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Springer, 2003, 478 p. DOI: 10.1007/978-1-4615-0302-6.

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

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

4. Botros N.M. HDL Programming Fundamentals: VHDL and Verilog. Charles River Media, 2005, 506 p.

5. Berkeley Logic Interchange Format (BLIF). Berkeley, U.C., Oct Tools Distribution 2, 1992, pp. 197-247.

6. Melnichenko I., Kamkin A., Smolov S. An Extended Finite State Machine-Based Approach to Code Coverage-Directed Test Generation for Hardware Designs. Proceedings of ISP RAS, 2015, 27(3), pp. 161-182. DOI: 10.15514/ispras-2015-27(3)-12.

7. Smolov S., Lopez J., Kushik N., Yevtushenko N., Chupilko M., Kamkin A. Testing Logic Circuits at Different Abstraction Levels: An Experimental Evaluation. Proceedings of IEEE East-West Design Test Symposium (EWDTS), 2016, pp. 189-192. DOI: 10.1109/ewdts.2016.7807687.

8. Ferrandi F., Fummi F., Gerli L., Sciuto D. Symbolic Functional Vector Generation for VHDL Specifications. Proceedings of Design, Automation and Test in Europe Conference and Exhibition, 1999, pp. 442-446. DOI: 10.1145/307418.307541.

9. Minato S. Generation of BDDs from Hardware Algorithm Descriptions. Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 1996, pp. 644-649. DOI: 10.1109/iccad.1996.571340.

10. Guglielmo G.D., Fummi F., Jenihhin M., Pravadelli G., Raik J., Ubar R. On the Combined Use of HLDDs and EFSMs for Functional ATPG. Proceedings of IEEE East-West Design and Test Symposium (EWDTS), 2007, pp. 503-508.

11. Brayton R., Mishchenko A. ABC: An Academic Industrial-Strength Verification Tool. Proceedings of the Computer Aided Verification Conference (CAV), 2010, pp. 24-40. DOI: 10.1007/978-3-642-14295-6_5.

12. Kamkin A., Lebedev M., Smolov S. An EFSM-Driven and Model Checking-Based Approach to Functional Test Generation for Hardware Designs. Proceedings of IEEE East-West Design and Test Symposium (EWDTS), 2016, pp. 60-63. DOI: 10.1109/ewdts.2016.7807736.

13. Смолов С., Камкин А. Метод построения расширенных конечных автоматов по HDL-описанию на основе статического анализа кода. Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 1(212), 2015, cтр. 60-73. DOI: 10.5862/jcstcs.212.6.

14. Страница инструмента Retrascope. http://forge.ispras.ru/projects/retrascope (дата обращения: 18.07.17)

15. Страница библиотеки Fortress. http://forge.ispras.ru/projects/solver-api (дата обращения: 18.07.17)

16. Cavada D., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M., Tonetta S. The nuXmv symbolic model checker. Proceedings of the 16th International Conference on Computer Aided Verification (CAV), No.8559, 2014, pp. 334-342. DOI: 10.1007/978-3-319-08867-9_22.

17. Страница набора тестов ITC'99. http://www.cad.polito.it/tools/itc99.html (дата обращения: 18.07.17)

18. Liu X., Hsiao M.S. On Identifying Functionally Untestable Transition Faults. Proceedings of the Ninth IEEE International High-Level Design Validation and Test Workshop, 2004, pp. 121-126. DOI: 10.1109/hldvt.2004.1431252.


Для цитирования:


Чупилко М.М., Камкин А.С., Лебедев М.С., Смолов С.А. Генерация тестов для цифровой аппаратуры на основе высокоуровневых моделей. Труды Института системного программирования РАН. 2017;29(4):247-256. https://doi.org/10.15514/ISPRAS-2017-29(4)-16

For citation:


Chupilko M.M., Kamkin A.S., Lebedev M.S., Smolov S.A. Test Generation for Digital Hardware Based on High-Level Models. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):247-256. https://doi.org/10.15514/ISPRAS-2017-29(4)-16

Просмотров: 91


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)