Conference paper

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014). Austin, TX: IEEE Computer Society, 2014, pp. 83-89. ISBN 978-1-4673-6858-2. Available from: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240
Publication language:english
Original title:Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
Title (cs):Analýza RAW hazardů v mikroprocesorech pomocí formální verifikace parametrizovaných systémů
Pages:83-89
Proceedings:Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)
Conference:Microprocessor Test and Verification 2014
Place:Austin, TX, US
Year:2014
URL:http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240
ISBN:978-1-4673-6858-2
Publisher:IEEE Computer Society
Keywords
automatic formal verification, microprocessor, register transfer level description, parameterised system, RAW hazard
Annotation
Implementation of a pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting design. Various techniques were proposed for this purpose, but they usually require a significant manual intervention of the developers. In this work, we propose a novel, highly automated approach for discovering RAW hazards in in-order pipelined instruction execution. Our approach combines static analysis of data paths to detect anomalies and possible hazards, followed by a transformation of detected problematic paths to a parameterised system, and a subsequent formal verification to check the possibility of unhandled hazards using techniques for formal verification of parameterised systems. We have implemented our approach and successfully applied it on multiple non-trivial microprocessors.
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 = {Using Formal Verification of Parameterized Systems in RAW
	Hazard Analysis in Microprocessors},
   pages = {83--89},
   booktitle = {Proceedings of 15th International Workshop on Microprocessor
	Test and Verification (MTV 2014)},
   year = {2014},
   location = {Austin, TX, US},
   publisher = {IEEE Computer Society},
   ISBN = {978-1-4673-6858-2},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10742}
}

Your IPv4 address: 54.166.245.10
Switch to IPv6 connection

DNSSEC [dnssec]