Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F14%3APU116937" target="_blank" >RIV/00216305:26230/14:PU116937 - isvavai.cz</a>

Výsledek na webu

<a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240" target="_blank" >http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/MTV.2014.21" target="_blank" >10.1109/MTV.2014.21</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

20206 - Computer hardware and architecture

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2014

Kód důvěrnosti údajů

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

Název statě ve sborníku

Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)

ISBN

978-1-4673-6858-2

ISSN

—

e-ISSN

—

Počet stran výsledku

7

Strana od-do

83-89

Název nakladatele

IEEE Computer Society

Místo vydání

Austin, TX

Místo konání akce

Austin, TX

Datum konání akce

15. 12. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000380373200017