Генерация функциональных тестов для HDL-описаний на основе проверки моделей
https://doi.org/10.15514/ISPRAS-2016-28(4)-3
Аннотация
Об авторах
М. С. Лебедев
Институт системного программирования РАН
Россия
Россия
С. А. Смолов
Институт системного программирования РАН
Россия
Россия
Список литературы
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
Послать статью по эл. почте 