A Model Checking-Based Method of Functional Test Generation for HDL Descriptions

Automated test generation is a promising direction in hardware verification research area. Functional test generation methods based on models are widespread at the moment. In this paper, a functional test generation method based on model checking is proposed and compared to existing solutions. Automated model extraction from the hardware design’s source code is used. Supported HDLs include VHDL and Verilog. Several kinds of models are used at different steps of the test generation method: guarded action decision diagram (GADD), high-level decision diagram (HLDD) and extended finite-state machine (EFSM). The high-level decision diagram model (which is extracted from the GADD model) is used as a functional model. The extended finite-state machine model is used as a coverage model. The aim of test generation is to cover all the transitions of the extended finite state machine model. Such criterion leads to the high HDL source code coverage. Specifications based on transition and state constraints of the EFSM are extracted for this purpose. Later, the functional model and the specifications are automatically translated into the input format of the nuXmv model checking tool. nuXmv performs model checking and generates counterexamples. These counterexamples are translated to functional tests that can be simulated by the HDL simulator. The proposed method has been implemented as a part of the HDL Retrascope framework. Experiments show that the method can generate shorter tests than the FATE and RETGA methods providing the same or better source code coverage.

hardware design, functional verification, static analysis, test generation, guarded action, high-level decision diagram, extended finite state machine, model checking

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

2. V.G. Lazarev, E.I. Piil'. Control automata synthesis. Energoatomizdat, Moscow, 1989. 328 p. (in Russian).

3. E.M. Clarke, O. Grumberg, and 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. Available at: 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. Trudy ISP RAN / Proc. ISP RAS, 2015, vol. 27, issue 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. S. Smolov, A. Kamkin. A method of extended finite state machines construction from HDL descriptions based on static analysis of source code. Nauchno-tehnicheskie vedomosti Sankt-Peterburgskogo gosudarstvennogo politehnicheskogo universiteta. Informatika. Telekommunikacii. Upravlenie. [St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunication and Control Systems], № 1(212), 2015. pp. 60-73 (in Russian).

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. Available at: https://es-static.fbk.eu/tools/nuxmv/index.php?n=Documentation.Home.

17. HDL Retrascope toolkit. Available at: http://forge.ispras.ru/projects/retrascope.

18. Fortress library. Available at: http://forge.ispras.ru/projects/solver-api.

19. ITC’99 benchmark. Available at: http://www.cad.polito.it/tools/itc99.html.

20. QuestaSim simulator. Available at: https://www.mentor.com/products/fv/questa/.

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

22. 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.