Tools for Functional Verification of Microprocessors

Ensuring the correctness of microprocessors and other microelectronic equipment is a fundamental problem. To deal with it, various tools for functional verification are used. Unlike bugs in software programs which are relatively easy to fix (it does not apply to their consequences), defects in integrated circuits (both design and manufacturing ones) cannot be removed. In spite of continuous development of computer-aided design (CAD) systems, test generation tools and approaches to analysis of circuits, verification remains the bottleneck of the microprocessor design cycle (it accounts for approximately 70 percent of total design resources). The article gives a brief overview of microprocessor verification tools, describes issues that commonly occur in industrial practice and analyzes possible ways to solve them. The main part of the article is dedicated to research in the field of hardware verification conducted at ISPRAS. It summarizes the outcomes of accomplished projects, describes the present works and formulates the directions of further research.

microprocessors, hardware, verification, validation, testing, test generation, modeling, architecture description languages, parallelization

1. Cok D.R. The SMT-LIBv2 Language and Tools: A Tutorial. GrammaTech, Inc., Version 1.1, 2011.

2. Kuliamin V.V. Metody verifikatsii programmnogo obespecheniya [Methods for Software Verification]. 2008, 111 p. (in Russian). (http://www.ispras.ru/~kuliamin/docs/VerMethods-2008-ru.pdf)

3. ZamiaCAD tool — http://zamiacad.sourceforge.net

4. Transistor count in microprocessors — http://en.wikipedia.org/wiki/Transistor_count

5. Kamkin A.S. Verifikatsiya mikroprotsessorov: bor'ba s oshibkami i upravlenie kachestvom [Microprocessor Verification. Combating Errors and Quality Control]. EHlektronika: NTB [Electronics: Science, Technology, Busincess], no. 3, 2010. pp. 98-104 (in Russian).

6. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, 2000. 354 p. doi:10.1007/978-1-4615-0302-6

7. Moore G.E. Cramming More Components onto Integrated Circuits. Electronics Magazine, vol. 86, no. 1, 1965. P. 82-85. (http://www.cs.utexas.edu/~fussell/courses/cs352h/papers/moore.pdf) doi:10.1109/JPROC.1998.658762

8. Bentley B. Validating the Intel® Pentium 4® Microprocessor. Proc. Design Automation Conference (DAC), 2001. pp. 244-248. doi:10.1145/378239.378473

9. Bentley B. Validating a Modern Microprocessor. Proc. International Conference on Computer Aided Verification (CAV), 2005. pp. 2-4. (http://www.cav2005.inf.ed.ac.uk/bentley_CAV_07_08_2005.ppt) (DOI 10.1007/11513988_2)

10. FDIV Replacement Program: Description of the Flaw — http://www.intel.com/support/processors/pentium/sb/CS-013007.htm

11. Revision Guide for AMD Family 10h Processors. Revision 3.84, August 2011. (http://developer.amd.com/wordpress/media/2012/10/41322.pdf)

12. Barak S. Intel Denies Core i7 TLB Bug. The Inquirer, December 02 2008. (http://www.theinquirer.net/inquirer/news/1049427/intel-denies-core-i7-tlb-bug)

13. Intel® Core™ i7-900 Desktop Processor Extreme Edition Series and Intel® Core™ i7-900 Desktop Processor Series. Specification Update, May 2011. (http://download.intel.com/design/processor/specupdt/320836.pdf)

14. Clarke E.M., Wing J.M. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, vol. 28, no. 4, 1996. pp. 626-643.

15. Harrison J. Formal Methods at Intel — An Overview. Second NASA Formal Methods Symposium (NFM), 2010. (http://www.cl.cam.ac.uk/~jrh13/slides/nasa-14apr10/slides.pdf)

16. McLellan P. History of Formal Verification at Intel. DAC Blog, December 05 2012. (http://blog.dac.com/post/2012/12/05/History-of-Formal-Verification-at-Intel.aspx)

17. Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodová A, Taylor C, Frolov V, Reeber E, Naik A. Replacing Testing with Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation. Proc. International Conference on Computer Aided Verification (CAV), 2009. pp. 414-429. doi:10.1007/978-3-642-02658-4_32

18. Bhadra J, Abadir M, Ray S, Wang L. A Survey of Hybrid Techniques for Functional Verification. IEEE Design & Test of Computers, vol. 24, no. 22, 2007. pp. 112-122. doi:10.1109/MDT.2007.30

19. Navabi Z. Languages for Design and Implementation of Hardware. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

20. Mikhani S, Navabi Z. System Level Design Languages. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

21. Mishra P, Dutt N (Eds.). Processor Description Languages. Systems on Silicon. Morgan Kaufmann, 2008. 432 p.

22. Kuliamin V.V. Perspektivy integratsii metodov verifikatsii programmnogo obespecheniya [Prospects for Integration of Software Verification Methods]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 16, 2009. pp. 73-88 (in Russian).

23. Agbaria S, Carmi D, Cohen O, Korchemny D, Lifshits M, Nadel A. SAT-Based Semiformal Verification of Hardware. Proc. Formal Methods in Computer-Aided Design (FMCAD), 2010. pp. 25-32.

24. Jain H, Kroening D, Sharygina N, Clarke E. VCEGAR: Verilog Counterexample Guided Abstraction Refinement. Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007. pp. 583-586. doi:10.1007/978-3-540-71209-1_45

25. Kamkin A, Smolov S, Melnichenko I. Static Analysis of HDL Descriptions: Extracting Models for Verification. Proc. East-West Design and Test Symposium (EWDTS), 2013. pp. 184-187. doi:10.1109/EWDTS.2013.6673126

26. Lam W.K. Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, 2005. 624 p.

27.

28.

29. Bombieri N, Fummi F, Pravadelli G, Marques-Silva J. Towards Equivalence Checking between TLM and RTL Models. Proc. IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2007. pp. 113-122. doi:10.1109/MEMCOD.2007.371236

30. Naveh Y, Rimon M, Jaeger I, Katz Y, Vinov M, Marcus E, Shurek G. Constraint-Based Random Stimuli Generation for Hardware Verification. AI Magazine, vol. 28, no. 3, 2007. pp. 13-30. doi:10.1609/aimag.v28i3.2052

31. UVM verification methodology — http://www.accellera.org/community/uvm

32. Barantsev A.V., Bourdonov I.B., Demakov A.V., Zelenov S.V., Kossatchev A.S., Kuliamin V.V., Omeltchenko V.A., Pakoulin N.V., Petrenko A.K., Khoroshilov A.V. Podkhod UniTesK k razrabotke testov: dostizheniya i perspektivy [UniTesK Approach to Test Development: Achievements and Prospects]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 5, 2004. pp. 151-156 (in Russian).

33. Sen K, Rosu G. Generating Optimal Monitors for Extended Regular Expressions. Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, 2003. pp. 162-181. doi:10.1016/S1571-0661(04)81051-X

34. 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, vol. 33, no. 5, 2007. pp. 272-282. doi:10.1134/S0361768807050039

35. Barringer H, Rydeheard D, Havelund K. Rule Systems for Run-Time Monitoring: From Eagle to RuleR. Proc. International Workshop on Runtime Verification, 2007. pp. 111-125. doi:10.1007/978-3-540-77395-5_10

36. Bauer A, Leucker M, Schallhart C. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, vol. 20, no. 4, 2011. pp. 14:1-14:64. doi:10.1145/2000799.2000800

37. Pnueli A. Temporal Logic of Programs. Proc. Symposium on Foundation of Computer Science (SFCS), 1977. pp. 46-57. doi:10.1109/SFCS.1977.32

38. Armoni R, Fix L, Flaisher A, Gerth R, Ginsburg B, Kanza T, Landver A, Mador-Haim S, Singerman E, Tiemeyer E, Vardi M, Zbar Y. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2002. pp. 296-311. doi:10.1007/3-540-46002-0_21

39. OpenVera® Language Reference Manual: Assertions. Version 1.4.1, November 2004.

40. 1850-2010 — IEEE Standard for Property Specification Language (PSL), 2010. doi:10.1109/IEEESTD.2005.97780

41. 1647-2011 — IEEE Standard for the Functional Verification Language e, 2011. doi:10.1109/IEEESTD.2011.6006495

42. 1800-2012 — IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, 2013. doi:10.1109/IEEESTD.2013.6469140

43. Pizialli A. Functional Verification Coverage Measurement and Analysis. Kluwer Academic Publishers, 2004. 216 p. doi:10.1007/b117979

44. Chupilko M, Kamkin A. A TLM-Based Approach to Functional Verification of Hardware Components at Different Abstraction Levels. Proc. Latin American Test Workshop (LATW), 2011. pp. 1-6. doi:10.1109/LATW.2011.5985902

45. Adir A, Almog E, Fournier L, Marcus E, Rimon M, Vinov M, Ziv A. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. IEEE Design & Test of Computers, vol. 21, no. 2, 2004. pp. 84-93. doi:10.1109/MDT.2004.1277900

46. Kamkin A.S. Generatsiya testovykh programm dlya mikroprotsessorov [Test Program Generation for Microprocessors]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 14, no. 2, 2008. pp. 23-63 (in Russian).

47. Test program PARANOIA — http://people.sc.fsu.edu/~%20jburkardt/c_src/paranoia/paranoia.html

48. Kamkin A.S., Sergeeva T.I., Smolov S.A., Tatarnikov A.D., Chupilko M.M. Extensible Environment for Test Program Generation for Microprocessors. Programming and Computer Software, vol. 40, no. 1, 2014. pp. 1-9. doi:10.1134/S0361768814010046

49. RAVEN test program generator — http://www.slideshare.net/DVClub/introducing-obsidian-software-and-ravengcs-for-powerpc

50. Gribkov I.V., Zakharov A.V., Koltsov P.P., Kotovich N.V., Kravchenko A.A., Koutsaev A.S., Osipov A.S., Khisambeev I.S. INTEG: A Stochastic Testing System for Microprocessor Verification. Proc. WSEAS International Conference on Circuits, Systems, Signal and Telecommunications (CSST), 2007. pp. 55-59.

51. MicroTESK tool — http://forge.ispras.ru/projects/microtesk

52. Genesys-Pro tool — https://www.research.ibm.com/haifa/projects/verification/genesys_pro/index.shtml

53. Mishra P., Dutt N. Specification-Driven Directed Test Generation for Validation of Pipelined Processors. ACM Transactions on Design Automation of Electronic Systems, vol. 13, no. 3, 2008. pp. 1-36. doi:10.1145/1367045.1367051

54. Dang T.N., Roychoudhury A., Mitra T., Mishra P. Generating Test Programs to Cover Pipeline Interactions. Proc. Design Automation Conference (DAC), 2009. pp. 142-147. doi:10.1145/1629911.1629953

55. Mokhoff N. Intel, Motorola Report Formal Verification Gains. EE Times, June 21 2001. (http://www.eetimes.com/document.asp?doc_id=1215957)

56. CTESK tool — http://forge.ispras.ru/projects/ctesk

57. Ivannikov V.P., Kamkin A.S., Kuliamin V.V., Petrenko A.K. Primenenie tekhnologii UniTesK dlya funktsional'nogo testirovaniya modelej apparatnogo obespecheniya [Application of the UniTESK Technology for Functional Testing of Hardware Models]. Preprint ISP RAN [Preprint of ISP RAS], 2005. 16 p. (in Russian).

58. Vorobyev D.N., Kamkin A.S. Generatsiya testovykh programm dlya podsistemy upravleniya pamyat'yu mikroprotsessora [Test Program Generation for Memory Management Units of Microprocessors]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 17, 2009. pp. 119-132 (in Russian).

59. Aryashev S.I., Kamkin A.S., Rogatkin B.Yu. Testirovanie RTL-modelej apparatury s pomoshh'yu tekhnologii UniTESK na primere bloka preobrazovaniya adresov mikroprotsessora [Using the UniTESK Technology for Testing RTL Hardware Models by the Example of the Microprocessor Translation Lookaside Buffer]. Proc. EHlektronika, mikro- i nanoehlektronika [Electronics, micro- and nanoelectronics], 2007. pp. 183-187 (in Russian).

60. Bourdonov I., Kossatchev A., Petrenko A., Galter D. KVEST: Automated Generation of Test Suites from Formal Specifications. Proc. World Congress on Formal Methods in the Development of Computing Systems (FM), vol. 1, 1999. pp. 608-621. doi:10.1007/3-540-48119-2_34

61. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V. Irredundant Algorithms for Traversing Directed Graphs: The Deterministic Case. Programming and Computer Software, vol. 29, no. 5, 2003. pp. 245-258. doi:10.1023/A:1025733107700

62. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V. Irredundant Algorithms for Traversing Directed Graphs: The Nondeterministic Case. Programming and Computer Software, vol. 30, no. 1, 2004. pp. 2-17. doi:10.1023/B:PACS.0000013436.72070.95

63. Meyer B. Design by Contract. Technical Report TR-EI-12/CO, Interactive Software Engineering Inc, 1986. doi:10.1109/2.161279

64. Floyd R.W. Assigning Meaning to Programs. Proc. Symposium on Applied Mathematics, 1967. pp. 19-32.

65. Hoare C.A.R. An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, no. 10, 1969. pp. 576-585. doi:10.1145/363235.363259

66. Dijkstra E.W. A Discipline of Programming. Prentice-Hall, 1976. 217 p.

67. Kuliamin V, Petrenko A, Pakoulin N, Kossatchev A, Bourdonov I. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. Proc. Perspectives of System Informatics, 2003. pp. 450-461. doi:10.1007/978-3-540-39866-0_45

68. Kamkin A. Contract Specification of Pipelined Designs: Application to Testbench Automation. Proc. Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2007. pp. 7-13.

69. Kamkin A. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications. Proc. East-West Design & Test Symposium (EWDTS), 2008. pp. 84-87. doi:10.1109/EWDTS.2008.5580153

70. Kamkin A.S. Metod formal'noj spetsifikatsii apparatury s konvejernoj organizatsiej i ego prilozhenie k zadacham funktsional'nogo testirovaniya [Method for Formal Specification of Pipelined Designs and Its Application to Functional Testing]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 16, 2009. pp. 107-128 (in Russian).

71. Chupilko M, Kamkin A. Developing Cycle-Accurate Contract Specifications for Synchronous Parallel-Pipeline Hardware: Application to Verification. Proc. Baltic Electronics Conference (BEC), 2010. pp. 185-188. doi:10.1109/BEC.2010.5631143

72. Chupilko M, Kamkin A. Specification-Driven Testbench Development for Synchronous Parallel-Pipeline Designs. Proc. NORCHIP, 2009. pp. 1-4. doi:10.1109/NORCHP.2009.5397808

73. Chupilko M, Kamkin A. Contract Specification of Hardware Designs at Different Abstraction Levels: Application to Functional Verification. Proc. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2010. pp. 125-129.

74. Khoroshilov A.V. Spetsifikatsiya i testirovanie sistem s asinkhronnym interfejsom [Specification and Testing of Systems with Asynchronous Interfaces]. Preprint ISP RAN [Preprint of ISP RAS], 2006. 139 p (in Russian).

75. Kamkin A.S., Chupilko M.M. Testirovanie modulej arifmetiki s plavayushhej tochkoj mikroprotsessorov na sootvetstvie standartu IEEE 754 [Testing Microprocessor Floating Point Arithmetic Modules for Conformity to the IEEE 754 Standard]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 14, no. 2, 2008. pp. 7-22 (in Russian).

76. Chupilko M, Kamkin A, Vorobyev D. Methodology and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications. Proc. Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2008. pp. 25-31.

77. Baratov R.A., Kamkin A.S., Mayorova V.M., Meshkov A.N., Sortov A.A., Yakusheva M.A. Trudnosti modul'noj verifikatsii apparatury na primere bufera komand mikroprotsessora Elbrus-2S [Difficulties of the Unit-Level Hardware Verification on the Example of the Instruction Buffer of the Elbrus-2S Microprocessor]. Voprosy radioehlektroniki [Issues of Radio Electronics], no. 3, 2013. pp. 84-96 (in Russian).

78. Dijkstra E. Guarded Commands, Non-determinacy and Formal Derivation of Programs. Communications of the ACM, vol. 18, no. 8, 1975. pp. 453-457. doi:10.1145/360933.360975

79. Rosenband D.L., Arvind. Hardware Synthesis from Guarded Atomic Actions with Performance Specifications. Proc. International Conference on Computer-Aided Design (ICCAD), 2005. pp. 784-791. doi:10.1109/ICCAD.2005.1560170

80. BluespecTM SystemVerilog Reference Guide, 2012.

81. Clare C. Designing Logic Systems Using State Machines. McGraw-Hill, 1973. 150 p.

82. Baranov S. Logic and System Design of Digital Systems. TUT Press, 2008. 266 p.

83. Ivannikov V.P., Kamkin A.S., Chupilko M.M. Proverka korrektnosti povedeniya HDL-modelej tsifrovoj apparatury na osnove dinamicheskogo sopostavleniya trass [Checking Behavior Correctness of HDL Models of Digital Hardware By On-the-Fly Trace Matching]. Proc. Tools & Methods of Program Analysis (TMPA), 2013. pp. 71-82 (in Russian).

84. Chupilko M, Kamkin A. Runtime Verification Based on Executable Models: On-the-Fly Matching of Timed Traces. Proc. Model-Based Testing Workshop (MBT), 2013. pp. 67-81. doi: 10.4204/EPTCS.111.6

85. C++TESK tool — http://forge.ispras.ru/cpptesk

86. von Bochmann G, Haar S, Jard C, Jourdan G.V. Testing Systems Specified as Partial Order Input/Output Automata. Proc. International Conference on Testing of Software and Communicating Systems (TestCom), 2008. pp. 169-183. doi:10.1007/978-3-540-68524-1_13

87. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V. Using Finite State Machines in Program Testing. Programming and Computer Software, vol. 26, no. 2, 2000, pp. 61–73.

88. Bourdonov I.B., Groshev S.G., Demakov A.V., Kamkin A.S., Kossatchev A.S., Sortov A.A. Parallel'noe testirovanie bol'shikh avtomatnykh modelej [Parallel Testing of Large Automata Models]. Vestnik Nizhegorodskogo universiteta im. N.I. Lobachevskogo [Vestnik of Lobachevsky State University of Nizhny Novgorod], no. 3, 2011. pp. 187-193 (in Russian).

89. Demakov A, Kamkin A, Sortov A. High-Performance Testing: Parallelizing Functional Tests for Computer Systems Using Distributed Graph Exploration. Proc. Open Cirrus Summit, 2011.

90. Bourdonov I.B., Kossatchev A.S. Obkhod neizvestnogo grafa kollektivom avtomatov [Traversal of an Unknown Graph by a Collective of Automata]. Proc. Nauchnyj servis v seti Internet: vse grani parallelizma [Scientific Service in Internet: All Facets of Parallelism], 2013. pp. 228-232 (in Russian).

91. Demakov A.V., Zelenova S.A., Zelenov S.V. Testirovanie parserov tekstov na formal'nykh yazykakh [Testing Parsers of Formal Languages]. Programmnye sistemy i instrumenty: Tematicheskij sbornik fakul'teta VMiK MGU [Software Systems and Tools: Proceedings of CMC Department of MSU], no. 2, 2001. pp. 150-156 (in Russian).

92. Zelenov S.V., Zelenova S.A., Kossatchev A.S., Petrenko A.K. Primenenie model'nogo podkhoda dlya avtomaticheskogo testirovaniya optimiziruyushhikh kompilyatorov [Application of the Model-Based Approach to Automated Testing of Optimized Compilers], 2003 (in Russian). (http://citforum.ru/SE/testing/compilers)

93. Wu L.-M., Wang K, Chiu C.-Y. A BNF-Based Automatic Test Program Generator for Compatible Microprocessor Verification. ACM Transactions on Design Automation of Electronic Systems, vol. 9, no. 1, 2004. pp. 105-132. doi:10.1145/966137.966142

94. Kamkin A.S. Nekotorye voprosy avtomatizatsii postroeniya testovykh programm dlya modulej obrabotki perekhodov mikroprotsessorov [Some Issues of Automation of Test Program Generation for Branch Units of Microprocessors]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 18, 2010. pp. 129-149 (in Russian).

95. Vorobyev D.N., Kamkin A.S. Generatsiya testovykh programm dlya mikroprotsessorov na osnove shablonov konvejernykh konfliktov [Test Program Generation for Microprocessors Based on Pipeline Hazards Templates]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 18, 2010. pp. 91-113 (in Russian).

96. MIPS64™ Architecture For Programmers, Revision 2.0. MIPS Technologies Inc, June 9 2003.

97. RM7000 Family User Manual. Issue 1, May 2001.

98. Kamkin A.S. Kombinatornaya generatsiya testovykh programm dlya mikroprotsessorov na osnove modelej [Combinatorial Model-Based Test Program Generation for Microprocessors]. Preprint ISP RAN [Preprint of ISP RAS], 2008. 18 p. (in Russian).

99. Kamkin A, Kornykhin E, Vorobyev D. Reconfigurable Model-Based Test Program Generator for Microprocessors. Proc. International Conference on Software Testing, Verification and Validation Workshops (ICSTW), 2011. pp. 47-54. doi:10.1109/ICSTW.2011.35

100. Kamkin A, Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Proc. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2012. pp. 64-69.

101. Freericks M. The nML Machine Description Formalism. Techical Report. TU Berlin, FB20, Bericht, 1991/15. 47 p.

102. Target Compiler Technologies — http://www.retarget.com

103. Chandra S, Moona R. Retargetable Functional Simulator using High Level Processor Models. VLSI Design, 2000. pp. 424-429. doi:10.1109/ICVD.2000.812644

104. GLISS tool — http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=54

105. Cassé H, Barre J, Vaillant R, Sainrat P. Fast Instruction-Accurate Simulation with SimNML. Proc. Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO), 2011. pp. 8-12.

106. Kamkin A, Sergeeva T, Tatarnikov A, Utekhin A. MicroTESK: An Extendable Framework for Test Program Generation. Proc. Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2013. pp. 51-57.

107. Ruby programming language — http://www.ruby-lang.org

108. Kornykhin E. SMT-Based Test Program Generation for Cache-Memory Testing. Proc. East-West Design & Test Symposium (EWDTS), 2009. pp. 124-127.

109. Kornykhin E. Generation of Test Data for Verification of Caching Mechanisms and Address Translation in Microprocessors. Programming and Computing Software, vol. 36, no. 1, 2010. pp. 28-35. doi:10.1134/S0361768810010056

110. Brandt J, Gemünde M, Schneider K, Shukla S, Talpin J.-P. Integrating System Descriptions by Clocked Guarded Actions. Proc. Forum on Design Languages (FDL), 2011. pp. 1-8.

111. Guglielmo G, Guglielmo L, Fummi F, Pravadelli G. Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs. Journal of Electronic Testing, vol. 27, no. 2, 2011. pp. 37-162. doi:10.1007/s10836-011-5209-8

112. Karaçali B, Tai K.-C., Vouk M.A. Deadlock Detection of EFSMs using Simultaneous Reachability Analysis. Proc. Dependable Systems and Networks (DSN), 2000. pp. 315-324. doi:10.1109/ICDSN.2000.857555

113. Kim A.K., Perekatov V.I., Ermakov S.G. Mikroprotsessory i vychislitel'nye kompleksy semejstva Elbrus [Microprocessors and Computer Systems of the Elbrus Family]. Saint-Petersburg, Piter, 2013. 272 p. (in Russian).

114. UML language — http://www.uml.org

115. Chatterjee S, Kishinevsky M, Ogras U. xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification. IEEE Design & Test of Computers, vol. 29, no. 3, 2011.pp. 80-88. doi:10.1109/MDT.2011.72

116. Holzmann G.J. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. 608 p.

117. Kamkin A.S., Petrochenkov M.V. Sistema podderzhki verifikatsii realizatsij protokolov kogerentnosti s ispol'zovaniem formal'nykh metodov [A System to Support Formal Methods-Based Verification of Coherence Protocol Implementations]. Voprosy radioehlektroniki [Issues of Radio Electronics], no. 3, 2014. pp. 27-38 (in Russian).

118. Schneider K, Kropf T. A Unified Approach for Combining Different Formalisms for Hardware Verification. Proc. International Conference on Formal Methods in Computer Aided Design (FMCAD), 1996. pp. 202-217. doi:10.1007/BFb0031809

119. Dutertre B, Moura L. The YICES SMT Solver, 2006. (http://yices.csl.sri.com/tool-paper.pdf).

120. Moura L, Bjørner N. Z3: An Efficient SMT Solver. Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. pp. 337-340. doi:10.1007/978-3-540-78800-3_24

121. McMillan K.L. Symbolic Model Checking. Kluwer Academic, 1993. 194 p.

122. Java Constraint Solver API — http://forge.ispras.ru/projects/solver-api

123. Cok D.R. The SMT-LIBv2 Language and Tools: A Tutorial. GrammaTech, Inc., Version 1.1, 2011.

124. ZamiaCAD tool — http://zamiacad.sourceforge.net