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%3APU116940" target="_blank" >RIV/00216305:26230/15:PU116940 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

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

Implementation of pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting designs. Our long-term goal is to develop a set of verification techniques with formal roots, each of them specialised in checking absence of a certain kind of errors in purpose-specific microprocessors. The main idea is that, this way, a high degree of automation and scalability can be achieved since only parts of a design related to a specific error are to be investigated. In our previous works, we proposed, with the above goal in mind, fully automated approaches for checking correctness of the implementation of individual instructions and for verifying absence of read-after-write (RAW) hazards. In this paper, we extend our approach by aiming at write-after-write (WAW) and write-after-read (WAR) 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

Implementation of pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting designs. Our long-term goal is to develop a set of verification techniques with formal roots, each of them specialised in checking absence of a certain kind of errors in purpose-specific microprocessors. The main idea is that, this way, a high degree of automation and scalability can be achieved since only parts of a design related to a specific error are to be investigated. In our previous works, we proposed, with the above goal in mind, fully automated approaches for checking correctness of the implementation of individual instructions and for verifying absence of read-after-write (RAW) hazards. In this paper, we extend our approach by aiming at write-after-write (WAW) and write-after-read (WAR) in microprocessors with a single pipeline.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

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í

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

Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)

ISBN

978-84-606-5438-4

ISSN

—

e-ISSN

—

Počet stran výsledku

2

Strana od-do

193-194

Název nakladatele

The Universidad de Las Palmas de Gran Canaria

Místo vydání

Las Palmas de Grand Canaria

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

—