• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • An Approach to Instruction Stream Generation for Functional Verification of Microprocessor Designs
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
October 19, 2026
'Cultural Studies Seeks to Understand What Lies Beneath the Surface of Everyday Things'
Maxim Zhiganov has been exploring different aspects of sound for many years—first in relation to his native Perm and then on a broader, global scale. In this interview for the HSE Young Scientists project, he talks about sound maps, the special issue of the journal Logos, and why it is important to make the familiar less clear and obvious.
October 14, 2026
At HSE University–St Petersburg, Experts Discuss How AI Changes Tourist Routes and Cultural Heritage
Neural networks are no longer simple travel assistants; now they decide what to include on the route and what to skip. Artificial intelligence changes how people perceive a place and shapes the image of tourist centres. At the II International Scientific and Practical Conference ’Information Technologies in the Preservation and Promotion of Cultural Heritage,’ researchers discussed who controls algorithmic solutions and in what ways, and whether authentic traditions get lost in them.
October 12, 2026
Road Injuries Leading Cause of Death Among Men Aged 10 to 39
Worldwide, road injuries are the leading cause of death among males aged 10–39. An international team of researchers reached this conclusion as part of the Global Burden of Disease Study 2023, analysing data from 204 countries between 1990 and 2023. Their findings have been published in The Lancet Public Health, with HSE University Professor Vasily Vlassov listed among the collaborators.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

An Approach to Instruction Stream Generation for Functional Verification of Microprocessor Designs

P. 270–273.
Tatarnikov A.

The paper proposes an approach to instruction stream generation for verification of microprocessor designs. The approach is based on using formal specifications of the instruction set architecture as a source of knowledge about the design under verification. This knowledge is processed with generic engines implementing an extensible set of generation strategies to produce stimuli in the form of instruction sequences. Generation tasks are formulated using high-level descriptions that specify target instructions and strategies of sequence construction and data generation. This provides a flexible way to generate deterministic, random and constraint-based stimuli for verification of arbitrary architectures with minimum effort. The proposed approach has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessor designs.

Language: English
DOI
Text on another site
Keywords: formal specificationsформальные спецификациисистема командмикропроцессорыinstruction setфункциональная верификациягенерация тестовых программfunctional verificationtest program generationinstruction stream generationmicroprocessorsгенерация потоков команд

In book

Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016)
Yerevan: IEEE, 2016.
Similar publications
Towards the Flexible Distribution Networks Design Using the Reliability Performance Metric
Shushpanov I., Suslov K., Ilyushin P. et al., Energies 2021 No. 14 Article 6193
At present, the entire world is moving towards digitalization, including in the electric power industry. Digitalization is in its heyday and a lot of articles and reports are devoted to this topic. At the same time, the least digitalized of the electrical networks are distribution networks that account for a very large share in electric ...
Added: December 29, 2021
Программная модель процессора и базовые инструкции процессоров Intel И MIPS
М.: НИУ ВШЭ, 2019.
Educational and methodical manual is an integral part of the methodological support for the discipline "Computer Systems and Computer Networks", studied by students of the program 09.03.01 - "Computer Science and Computer Engineering". The main content is computer architecture example of the of 32-bit Intel and MIPS processors, their Insrtuction Set, the sequence of information processing in ...
Added: November 16, 2019
Test Program Generator MicroTESK for RISC-V
Kamkin A., Чупилко М. М., Смолов С. А. et al., , in: 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV).: Austin: IEEE Computer Society, 2018. P. 6–11.
The paper presents a test program generator for functional verification of RISC-V microprocessors. The generator is implemented on the base of MicroTESK framework and consists of formal specifications of RISC-V ISA and ISA-independent core. The specifications describe instructions' syntax and semantics and can be easily modified to support more instructions (including custom extensions). The core ...
Added: July 3, 2019
Введение в формальные методы верификации программ: учебное пособие
Kamkin A., М.: МАКС Пресс, 2018.
This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...
Added: November 2, 2018
Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK
Tatarnikov A., Kamkin A., Проценко А. С. et al., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
In this paper, a specification-based test program generator for functional verification of RISC-V microprocessors is presented. The tool is based on the MicroTESK framework and consists of two main parts: (1) the formal specifications of the RISC-V ISA and (2) the ISA-independent generation core. Test programs are generated on the basis of the ISA specifications and test templates ...
Added: October 30, 2018
Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the ninth workshop dedicated to formalisms for program semantics, formal models and verification, programming and specification languages, algebraic and logical aspects of programming. ...
Added: October 26, 2018
Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units
Kamkin A., Tatarnikov A., Смолов С. А. et al., , in: 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2015. P. 1–6.
In this paper, a tool for automatically generating test programs for ARM VMSAv8-64 memory management units is described. The solution is based on the MicroTESK framework being developed at ISP RAS. The tool consists of two parts: an architecture-independent test program generation core and VMSAv8-64 specifications. Such separation is not a new principle in the ...
Added: July 18, 2018
Maintaining ISA Specifications in MicroTESK Test Program Generator
Kamkin A., Tatarnikov A., Проценко А. С. et al., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
The specification-based approach is widely used for test program generation for functional verification of microprocessors. The size of microprocessor specifications is measured in thousands lines of code. Consequently, their maintenance requires significant effort. Typical maintenance activities include regular updates, substitution of deprecated functionality, and support for new revisions and implementation-defined features. Our team is working ...
Added: July 18, 2018
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit