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

Тестирование аппаратуры - это процесс, нацеленный на обнаружение неисправностей, внесенных в интегральные схемы в процессе производства. Для оценки качества таких тестов используют две основные метрики: способность обнаруживать ошибки (покрытие ошибок) и время тестирования (длина теста). Известно множество методов генерации тестов, однако масштабируемого решения, применимого к сложной цифровой аппаратуре, нет до сих пор. В данной статье анализируется возможность использования функциональных тестов, построенных по высокоуровневым моделям (прежде всего, моделям уровня регистровых передач), для низкоуровневого производственного тестирования. Рассматривается конкретный метод генерации тестов, использующий технику проверки моделей (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.