Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU117129" target="_blank" >RIV/00216305:26230/15:PU117129 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf" target="_blank" >http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-27340-2_75" target="_blank" >10.1007/978-3-319-27340-2_75</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Popis výsledku v původním jazyce

The current stress on having a rapid development cycle for microprocessors featuring pipeline-based execution leads to a high demand of automated techniques supporting the design, including a support for its verification. We present an automated technique exploiting static analysis of data paths and formal verification of parameterized systems in order to discover flaws caused by improperly handled data hazards. In particular, as a complement of our previous work on read-after-write hazards, we focus on write-after-write and write-after-read hazards in microprocessors with a single pipeline.

Název v anglickém jazyce

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Popis výsledku anglicky

The current stress on having a rapid development cycle for microprocessors featuring pipeline-based execution leads to a high demand of automated techniques supporting the design, including a support for its verification. We present an automated technique exploiting static analysis of data paths and formal verification of parameterized systems in order to discover flaws caused by improperly handled data hazards. In particular, as a complement of our previous work on read-after-write hazards, we focus on write-after-write and write-after-read hazards in microprocessors with a single pipeline.

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í

2015

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

Computer Aided Systems Theory - EUROCAST 2015

ISBN

978-3-319-27340-2

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

10

Strana od-do

605-614

Název nakladatele

Springer International Publishing

Místo vydání

Zurich

Místo konání akce

Las Palmas de Gran Canaria

Datum konání akce

8. 2. 2015

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

WRD - Celosvětová akce

Kód UT WoS článku

000376687100075