Result Details

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012. p. 6-12. ISBN: 978-1-4673-4441-8.
Type
conference paper
Language
English
Authors
Charvát Lukáš, Ing., Ph.D., DIFS (FIT), DITS (FIT)
Smrčka Aleš, Ing., Ph.D., DIFS (FIT), DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

The paper proposes an automated approach with a formal basis designed for checking correspondence between an RTL implementation of a microprocessor and a description of its instruction set architecture (ISA). The goals of the approach are to find bugs not discovered by functional verification, to minimize user intervention in the verification process, and to provide a developer with practical results within a short period of time. The main idea is to use bounded model checking to check that the output produced by automatically derived RTL and ISA models of a given processor are the same for each instruction and each possible input. Although the approach does not provide full formal verification, experiments with the approach confirm that due to a different way it explores the state space of the design under test, it can find bugs not found by functional verification, and is thus a useful complement to functional verification.

Keywords

automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking

URL
Published
2012
Pages
6–12
Proceedings
Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
Conference
Microprocessor Test and Verification 2012
ISBN
978-1-4673-4441-8
Publisher
Institute of Electrical and Electronics Engineers
Place
Austin, TX
DOI
10.1109/MTV.2012.19
BibTeX 
@inproceedings{BUT97556,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description",
  booktitle="Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)",
  year="2012",
  pages="6--12",
  publisher="Institute of Electrical and Electronics Engineers",
  address="Austin, TX",
  doi="10.1109/MTV.2012.19",
  isbn="978-1-4673-4441-8",
  url="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727"
}
Files
Projects
Advanced secured, reliable and adaptive IT, BUT, Vnitřní projekty VUT, FIT-S-11-1, start: 2011-01-01, end: 2013-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
System for Programming and Realization of Embedded Systems, MPO, TIP, FR-TI1/038, start: 2009-07-01, end: 2013-06-30, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Hardware-Software Codesign research group (RG LISSOM)
Departments
Department of Intelligent Systems (DITS)
Back to top