| A Method of Functional Test Generation for HDL Descriptions Based on Model Checking of High-Level Decision Diagrams |
|
 |
|
|
| Authors |
| | Lebedev M.S. |
| | Smolov S.A. |
| Date of publication |
| | 2016 |
|
| Abstract |
| | Functional verification is an expensive and time-consuming stage of the hardware design process. Automated methods are one of the promising directions in this research area. A number of functional test generation methods based on model extraction have been proposed recently. Automated verification methods often use abstract models of hardware. Properties of a model may be represented in the form of specifications. Model checking is one of the techniques for proving these properties. Functional tests can be obtained by parsing the counterexamples – sequences of states and variable values which violate the specification and are generated by the model checking tool.
Actual problems of functional test generation methods based on symbolic model checking techniques are state explosion and the necessity to translate the device under verification to the model checker format. The first one remains a challenging task though bounded model checking and predicate abstraction techniques can be helpful. As for the second problem, automated methods should be proposed to extract testable models from HDL descriptions and to analyze them with model checking tools.
The method proposed in this paper is based on automated extraction of high-level decision diagrams (HLDD) and extended finite-state machines (EFSM) from the HDL description. For the specified variable its high-level decision diagram is a directed acyclic graph which represents the variable’s values at every condition specified in the description. A set of HLDDs for all non-input variables forms a HLDD model of the process.
Another kind of abstractions that are used in the proposed method is an EFSM model. EFSM can be treated as a finite state machine (FSM) including both a set of internal variables and Boolean conditions (called guards) on transitions between states and sequences of statements (actions) which should be executed when corresponding guards are fired. For every transition of the EFSM that is extracted from the HDL description the constraint is created that encodes its feasibility condition (safety property).
HLDD model and specifications that are extracted from EFSM model are then translated into SMV language format. SMV model is checked by the nuXmv model checker. Counterexamples generated by nuXmv are translated into HDL-based tests and can be simulated by a HDL simulator.
The proposed method was implemented as a part of the HDL Retrascope tool. Some designs from the ITC’99 benchmark were used as examples. Experimental results were compared to FATE, RETGA and random test generation methods. Comparison shows that tests obtained by the proposed method are shorter than produced by the FATE method and much shorter than generated by random test generation method. Tests generated by the RETGA method have comparable lengths to the new ones.
All tests were simulated by the QuestaSim HDL simulator. Statement and branch coverage of the original HDL descriptions was collected. Coverage results show that the proposed method provides better coverage than the FATE and random generation methods and not worse than the RETGA method. |
| Keywords |
| | hardware design; functional verification; static analysis; test generation; guarded action; high-level decision diagram; extended finite state machine; model checking. |
| Library reference |
| | Lebedev M.S., Smolov S.A. A Method of Functional Test Generation for HDL Descriptions Based on Model Checking of High-Level Decision Diagrams // Problems of Perspective Micro- and Nanoelectronic Systems Development - 2016. Proceedings / edited by A. Stempkovsky, Moscow, IPPM RAS, 2016. Part 2. P. 24-31. |
| URL of paper |
| | http://www.mes-conference.ru/data/year2016/pdf/D122.pdf |
