Test Generation for Digital Hardware Based on High-Level Models

Hardware testing is a process aimed at detecting manufacturing faults in integrated circuits. To measure test quality, two main metrics are in use: fault detection abilities (fault coverage) and test application time (test length). Many algorithms have been suggested for test generation; however, no scalable solution exists. In this paper, we analyze applicability of functional tests generated from high-level models for low-level manufacturing testing. A particular test generation method is considered. The input information is an HDL description. The key steps of the method are system model construction and coverage model construction. Both models are automatically extracted from the given description. The system model is a representation of the design in the form of high-level decision diagrams. The coverage model is a set of LTL formulae defining reachability conditions for the transitions of the extended finite state machine. The models are translated into the input format of a model checker. For each coverage model formula the model checker generates a counterexample, i.e. an execution that violates the formula (makes the corresponding transition to fire). The approach is intended for covering of all possible execution paths of the input HDL description and detecting dead code. Experimental comparison with the existing analogues has shown that it produces shorter tests, but they achieve lower stuck-at fault coverage comparing with the dedicated approach. An improvement has been proposed to overcome the issue.

digital hardware, hardware description language, manufacturing testing, stuck-at fault, high-level decision diagram, extended finite state machine, model checking, fault propagation

1. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Springer, 2003, 478 p. DOI: 10.1007/978-1-4615-0302-6.

2. Ivannikov V.P., Kamkin A.S., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. The Use of Contract Specifications for Representing Requirements and for Functional Testing of Hardware Models. Programming and Computer Software, 33(5), 2007, pp. 272-282. DOI: 10.1134/s0361768807050039.

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. Smolov S., Kamkin A. A Method of Extended Finite State Machines Construction From HDL Descriptions Based on Static Analysis of Source Code. St. Petersburg State Polytechnical University Journal. Computer Science, Telecommunications, 1(212), 2015, pp. 60-73 (in Russian). DOI: 10.5862/jcstcs.212.6.

14. Retrascope site. http://forge.ispras.ru/projects/retrascope

15. Fortress library site. http://forge.ispras.ru/projects/solver-api

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 benchmark site. http://www.cad.polito.it/tools/itc99.html

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.