Ing. Lukáš Charvát

CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. Brno: Fakulta informačních technologií VUT v Brně, 2014.
Jazyk publikace:angličtina
Název publikace:Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
Název (cs):Analýza RAW hazardů v mikroprocesorech pomocí formální verifikace parametrizovaných systémů
Strany:18
Místo vydání:Brno, CZ
Rok:2014
Vydavatel:Fakulta informačních technologií VUT v Brně
URL:http://www.fit.vutbr.cz/research/groups/verifit/tools/hades/techrep/hades-techrep.pdf [PDF]
Klíčová slova
automatic formal verification, microprocessor, register transfer level description, parameterised system, RAW hazard
Anotace
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:
@TECHREPORT{
   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 = {18},
   year = {2014},
   location = {Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=10743}
}

Vaše IPv4 adresa: 3.84.182.112
Přepnout na https