Conference paper

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In: Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012, pp. 6-12. ISBN 978-1-4673-4441-8. Available from: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727
Publication language:english
Original title:Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description
Title (cs):Automatické formální ověření shody ISA a RTL návrhu mikroprocesoru
Pages:6-12
Proceedings:Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
Conference:Microprocessor Test and Verification 2012
Place:Austin, TX, US
Year:2012
URL:http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727
ISBN:978-1-4673-4441-8
Publisher:Institute of Electrical and Electronics Engineers
Files: 
+Type Name Title Size Last modified
iconmtv12.pdf181 KB2012-09-08 22:15:53
^ Select all
With selected:
Keywords
automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}} Smr{\v{c}}ka
	and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Automatic Formal Correspondence Checking of ISA and RTL
	Microprocessor Description},
   pages = {6--12},
   booktitle = {Proceedings of the 13th International Workshop on
	Microprocessor Test and Verification (MTV 2012)},
   year = {2012},
   location = {Austin, TX, US},
   publisher = {Institute of Electrical and Electronics Engineers},
   ISBN = {978-1-4673-4441-8},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10135}
}

Your IPv4 address: 54.161.25.213
Switch to IPv6 connection

DNSSEC [dnssec]