Preview

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

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

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

https://doi.org/10.15514/ISPRAS-2016-28(4)-3

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

Аннотация

Разработка методов автоматической генерации тестов составляет перспективное направление в области верификации цифровой аппаратуры. На текущий момент большое распространение имеют методы генерации функциональных тестов на основе моделей. В данной работе представлен метод генерации функциональных тестов на основе проверки моделей и результаты его сравнения с существующими решениями. В методе используется автоматическое извлечение моделей из исходного кода HDL-описания аппаратуры. Поддерживаются языки VHDL и Verilog. Метод генерации тестов включает автоматическое построение моделей следующих типов: решающие диаграммы системы охраняемых действий (Guarded Action Decision Diagram,GADD), высокоуровневые решающие диаграммы (High-Level Decision Diagrams, HLDD) и расширенные конечные автоматы (Extended Finite-State Machines, EFSM). HLDD-модель используется в качестве функциональной модели. Модель EFSM используется в качестве модели покрытия. Целью тестирования является покрытие всех переходов расширенного конечного автомата. Выбор такого критерия позволяет получить высокое покрытие исходного кода HDL-описания. Из EFSM-модели извлекаются спецификации, основанные на ограничениях на переходы и состояния. Затем спецификации и функциональная модель автоматически транслируются во входной формат инструмента проверки моделей nuXmv. Инструмент выполняет проверку модели и строит контрпримеры. Контрпримеры транслируются в функциональные тесты, которые могут быть исполнены с помощью HDL-симулятора. Предлагаемый метод был реализован программно в инструменте HDL Rertrascope. Результаты экспериментов показывают, что метод генерирует более короткие тесты, чем методы FATE и RETGA, при обеспечении такого же или лучшего покрытия исходного кода.

Об авторах

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


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


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

1. J. Bergeron. Writing Testbenches: Functional Verification of HDL Models. Springer, 2003. 478 p.

2. Лазарев В.Г., Пийль Е.И. Синтез управляющих автоматов. Энергоатомиздат, Москва, 1989. 328 с.

3. E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking. MIT Press, Cambridge, 2000. 314 p.

4. R.J. Ubar, J. Raik, A. Jutman, M. Jenihhin. Diagnostic modeling of digital systems with multi-level decision diagrams. Design and Test Technology for Dependable Systems-on-Chip, 2011. pp. 92-118.

5. IEEE Standard VHDL Language Reference Manual. IEEE Std 1076-2008 (Revision of IEEE Std 1076-2002), 2009. pp.c1-626.

6. IEEE Standard for Verilog Hardware Description Language. IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001), 2006. pp.0_1-560.

7. D. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta. The nuXmv symbolic model checker. Proceedings of the 16th International Conference on Computer Aided Verification (CAV), 2014, № 8559. pp. 334-342.

8. D. Deharbe, S. Shankar, E.M. Clarke. Model checking VHDL with CV. Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD), 1998. pp. 508-514.

9. CBMC model checker. Доступно по ссылке: http://www.cprover.org/cbmc/

10. G. Guglielmo, L. Guglielmo, F. Fummi, G. Pravadelli. Efficient generation of stimuli for functional verification by backjumping across extended FSMs. Journal of Electronic Functional Testing: Theory and Application, 2011, № 27(2). pp. 137-162.

11. I. Melnichenko, A. Kamkin, S. Smolov. An extended finite state machine-based approach to code coverage-directed test generation for hardware designs. Proceedings of the Institute for System Programming, 2015, № 27(3). pp. 161-182. DOI: 10.15514/ISPRAS-2015-27(3)-12.

12. E. Dijkstra. A Discipline of Programming. Prentice Hall, 1976. 217 p.

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

14. J. Brandt, M. Gemünde, K. Schneider, S. Shukla, J.-P. Talpin. Integrating system descriptions by clocked guarded actions. Forum on Design Languages, 2011. pp. 1-8.

15. R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, F.K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, № 13(4), 1991. pp. 451-490.

16. M. Bozzano, R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta. NuXmv 1.0 User Manual. 2014. pp. 7-44. Доступно по ссылке: https://es-static.fbk.eu/tools/nuxmv/index.php?n=Documentation.Home.

17. Fortress library. Доступно по ссылке: http://forge.ispras.ru/projects/solver-api.

18. ITC’99 benchmark. Доступно по ссылке: http://www.cad.polito.it/tools/itc99.html.

19. QuestaSim simulator. Доступно по ссылке: https://www.mentor.com/products/fv/questa/.

20. E. Clarke, A. Biere, R. Raimi, Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 2001, Vol. 19 Iss. 1. pp. 7-34.

21. E. Clarke, M. Talupur, H. Veith, D. Wang. SAT based predicate abstraction for hardware verification. Lecture Notes in Computer Science, 2004, Vol. 2919. pp. 78-92.


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


Лебедев М.С., Смолов С.А. Генерация функциональных тестов для HDL-описаний на основе проверки моделей. Труды Института системного программирования РАН. 2016;28(4):41-56. https://doi.org/10.15514/ISPRAS-2016-28(4)-3

For citation:


Lebedev M.S., Smolov S.A. A Model Checking-Based Method of Functional Test Generation for HDL Descriptions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):41-56. https://doi.org/10.15514/ISPRAS-2016-28(4)-3

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


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


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