Achieving high coverage in hardware equivalence checking via concolic verification
Tóm tắt
A concolic approach, called slec-cf, to find counterexamples (CEXs) to sequential equivalence between a high-level (e.g., SystemC) hardware description and an RTL (e.g., Verilog) is presented. slec-cf works by searching for CEXs over the possible values of a set of “control signals” in a depth-first lexicographic manner, and avoiding values that cannot be realized by any concrete input. In addition, slec-cf respects user-specified design constraints during search, thus only producing stimuli that are of relevance to users. It is a superior alternative to random simulations, which produce an overwhelming number of irrelevant stimuli for user-constrained designs, and are therefore of limited effectiveness. Two strategies for concolic exploration are presented—searching all control signal values exhaustively, and only exploring values which share a common prefix with an initial random sample. In addition, two choices of control signals are proposed—the set of all MUX selectors in the RTL, and the MUX selectors that are derived from branch conditions in the SystemC description. Finally, slec-cf is made incremental by iteratively increasing the search depth, and set of control signals, and using a cache to reuse prior results. The approach is implemented on top an existing industrial sequential equivalence checker (slec) which compares C++/SystemC against RTL, created either manually, or by a high level synthesis tool, such as catapult. Experimental results indicate that slec-cf clearly outperforms random simulation in terms of finding CEXs quickly, and achieving coverage, over an industrial benchmark. On complex designs, incremental slec-cf demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental slec-cf.
Tài liệu tham khảo
Ahmed A, Mishra P (2017) QUEBS: qualifying event based search in concolic testing for validation of RTL models. In: Proceedings of the 1996 international conference on computer design (ICCD ’17). IEEE Computer Society, Boston, MA, pp 185–192
Biere A, Cimatti A, Clarke EM et al (2003) Bounded model checking, advances in computers, vol 58. Academic Press, Boca Raton
Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 12th USENIX symposium on operating system design and implementation (OSDI ’08), San Diego, pp 209–224
Catapult C Synthesis. http://calypto.agranderdesign.com/catapult_c_synthesis.php
Chauhan P, Goyal D, Hasteer G et al (2009) Non-cycle-accurate sequential equivalence checking. In: Proceedings of the 46th ACM IEEE design automation conference (DAC ’09). Association for Computing Machinery, San Francisco, CA, USA, pp 460–465
Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons for branching time temporal logic. In: Kozen D (ed) Proceedings of workshop on logic of programs, lecture notes in computer science, vol 131. Springer, Yorktown Heights, New York, May 4–6, 1981. Berlin, Germany, pp 52–71
Duran JW, Ntafos SC (1984) An evaluation of random testing. IEEE Trans Softw Eng (TSE) SE–10(4):438–444
Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In: Sarkar V, Hall MW (eds) Proceedings of the ACM SIGPLAN 2005 conference on programming language design and implementation (PLDI ’05). Association for Computing Machinery, Chicago, Illinois, USA, pp 213–223
Godefroid P, Levin MY, Molnar D (2007) Automated whitebox fuzz testing. Technical report TR-2007-58, Microsoft Research, Redmond, WA
Kelly JH, Dan SV, John JC et al (2001) A practical tutorial on modified condition/decision coverage. Technical report NASA/TM-2001-210876, NASA Langley Research Center, Langley, VA, USA. https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20010057789.pdf
Liu L, Vasudevan S (2009) STAR: generating input vectors for design validation by static analysis of RTL. In: Proceedings of IEEE international high level design validation and test workshop (HLDVT ’09). IEEE Computer Society, San Francisco, CA, pp 32–37
Liu L, Vasudevan S (2011) Efficient validation input generation in RTL by hybridized source code analysis. In: Proceedings of 2011 design, automation and test in Europe conference and exposition (DATE ’11). IEEE Computer Society, Grenoble, France, pp 1596–1601
Martin G, Smith G (2009) High-level synthesis: past, present, and future. IEEE Des Test Comput 26(4):18–25
Matsumoto T, Nishihara T, Kojima Y et al (2009) Equivalence checking of high-level designs based on symbolic simulation. In: Proceedings of the international conference on communications, circuits and systems (ICCAS). IEEE Computer Society, pp 1129–1133
Pinto S, Hsiao MS (2017) RTL functional test generation using factored concolic execution. In: Proceedings of the IEEE international test conference (ITC ’17). IEEE Computer Society, Fort Worth, TX, USA, pp 1–10
Pixley C (1992) A theory and implementation of sequential hardware equivalence. IEEE Trans Comput-Aided Des Integr Circuits Syst (TCAD) 11(12):1469–1478
Roy P, Chaki S, Chauhan P (2019) High coverage concolic equivalence checking. In: Proceedings of 2019 design, automation and test in Europe conference and exposition (DATE ’19). IEEE Computer Society, Florence, Italy, March 25-29, 2019. Los Alamitos, CA, pp 462–467
Sen K, Agha G (2006) CUTE and jcute: concolic unit testing and explicit path model-checking tools. In: Ball T, Jones RB (eds) Proceedings of the 18th international conference on computer aided verification (CAV ’06), lecture notes in computer science, vol 4144. Springer, Seattle, WA, pp 419–423
Zhang Y, Feng W, Huang M (2016) Automatic generation of high-coverage tests for RTL designs using software techniques and tools. In: Proceedings of the IEEE 11th conference on industrial electronics and applications (ICIEA ’16). IEEE Computer Society, Hefei, China, pp 856–861