• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Maintaining ISA Specifications in MicroTESK Test Program Generator
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2028
  • 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
August 25, 2026
Scientists Develop Algorithm for More Reliable Processors in Data Centres
Researchers from HSE MIEM and Samara University have developed the LRF-3D algorithm to automatically bypass idle nodes in three-dimensional networks-on-chip. Thanks to its hierarchical architecture, the algorithm outperforms existing solutions in both speed and path accuracy, improving processor reliability for use in data centres, supercomputers, and AI computing. The source code and test results are publicly available.
August 24, 2026
Researchers Develop Method for Direct Generation of Regulatory DNA
Researchers at HSE University have developed a model for generating promoters and enhancers—DNA sequences that regulate gene activity. The model works directly with DNA nucleotides, without first transforming them into a continuous numerical representation. This solution could be useful for applications in synthetic biology and gene therapy. The study results were presented at the ICLR 2026 Workshop ‘Generative AI in Genomics (Gen^2): Barriers and Frontiers.’
August 21, 2026
Social Integration: At the Crossroads of Knowledge and Values
The International Laboratory for Social Integration Research (ILSIR) at HSE University studies the challenges faced by vulnerable groups and explores ways to help them participate fully in everyday life. To develop effective solutions, the laboratory’s researchers combine cutting-edge methods with practical fieldwork. In this interview with the HSE News Service, Laboratory Head Elena Iarskaia-Smirnova discusses the laboratory’s work.

 

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

?

Maintaining ISA Specifications in MicroTESK Test Program Generator

P. 10–14.
Kamkin A., Tatarnikov A., Проценко А. С., Смолов С. А., Коцыняк А. М., Чупилко М. М.

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 on MicroTESK, a tool that generates test programs for microprocessors based on specifications of the instruction set architectures. The specifications are created in a specialized language, called nML, extended with facilities to manage revision-specific and implementation-defined features. The tool has been applied to ARMv8, MIPS64, PowerPC, RISC-V, and x86 microprocessors. This paper describes our experience in maintaining specifications and the approach we use to simplify this process.

Language: English
DOI
Keywords: formal specificationsfunctional verificationtest program generationmicroprocessorsinstruction set architecture

In book

2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV)
IEEE, 2017.
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
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
Расширяемая среда генерации тестовых программ для микропроцессоров
Tatarnikov A., Kamkin A., Смолов С. А. et al., Программирование 2014 Т. 1 № 40 С. 3–14
Development of test programs and analysis of the results of their execution is the basic approach to verification of microprocessors at the system level. There is a variety of methods for the automation of test generation, starting with the generation of random code and ending with directed model-based test generation. However, there is no cure-all ...
Added: February 5, 2018
Построение поведенческих моделей микропроцессоров для генерации тестовых программ
Tatarnikov A., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
The paper proposes a method of automated construction of behavior models of microprocessors, which are used in the process of test program generation to predict the results. The proposed method is based on using formal specifications of instruction set architecture. The method is implemented in MicroTESK, a test program generation tool being developed at ISP ...
Added: February 2, 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