Hades: 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%2F16%3APU122432" target="_blank" >RIV/00216305:26230/16:PU122432 - isvavai.cz</a>
Výsledek na webu
<a href="http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9" target="_blank" >http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4204/EPTCS.233.9" target="_blank" >10.4204/EPTCS.233.9</a>

Jazyk výsledku
angličtina
Název v původním jazyce
Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Popis výsledku v původním jazyce
Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses on single-pipeline microprocessors designed at the register transfer level (RTL) and deals with read-after-write, write-after-write, and write-after-read hazards. Hades combines several techniques, including data-flow analysis, error pattern matching, SMT solving, and abstract regular model checking. It has been successfully tested on several microprocessors for embedded applications.
Název v anglickém jazyce
Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Popis výsledku anglicky
Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses on single-pipeline microprocessors designed at the register transfer level (RTL) and deals with read-after-write, write-after-write, and write-after-read hazards. Hades combines several techniques, including data-flow analysis, error pattern matching, SMT solving, and abstract regular model checking. It has been successfully tested on several microprocessors for embedded applications.

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)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění
2016
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 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)
ISBN
978-80-210-8362-2
ISSN
2075-2180
e-ISSN
—
Počet stran výsledku
7
Strana od-do
87-93
Název nakladatele
Faculty of Informatics MU
Místo vydání
Brno
Místo konání akce
Telč
Datum konání akce
21. 10. 2016
Typ akce podle státní příslušnosti
EUR - Evropská akce
Kód UT WoS článku
000390333200010

Podobné výsledky(10)