Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F12%3APU102230" target="_blank" >RIV/00216305:26230/12:PU102230 - isvavai.cz</a>
Result on the web
<a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727" target="_blank" >http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/MTV.2012.19" target="_blank" >10.1109/MTV.2012.19</a>

Result language
angličtina
Original language name
Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description
Original language description
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.
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
ISBN
978-1-4673-4441-8
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
6-12
Publisher name
Institute of Electrical and Electronics Engineers
Place of publication
Austin, TX
Event location
Austin, TX
Event date
Dec 10, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)