Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D., UIFS (FIT), UITS (FIT)
Smrčka Aleš, Ing., Ph.D., UIFS (FIT), UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

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.

Klíčová slova

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

URL
Rok
2012
Strany
6–12
Sborník
Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
Konference
Microprocessor Test and Verification 2012
ISBN
978-1-4673-4441-8
Vydavatel
Institute of Electrical and Electronics Engineers
Místo
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"
}
Soubory
Projekty
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, zahájení: 2011-01-01, ukončení: 2013-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Systém pro programování a realizaci vestavěných systémů, MPO, TIP, FR-TI1/038, zahájení: 2009-07-01, ukončení: 2013-06-30, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Výzkumná skupina Hardware-Software Codesign (VZ LISSOM)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru