Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F12%3APU102230" target="_blank" >RIV/00216305:26230/12:PU102230 - isvavai.cz</a>

  • Výsledek na webu

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

  • DOI - Digital Object Identifier

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

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

  • Popis výsledku v původním jazyce

    The paper proposes an automated approach with a formal basis designed for checking correspondence between an RTL implementation of a microprocessor and a description of its instruction set architecture (ISA). The goals of the approach are to find bugs not discovered by functional verification, to minimize user intervention in the verification process, and to provide a developer with practical results within a short period of time. The main idea is to use bounded model checking to check that the output produced by automatically derived RTL and ISA models of a given processor are the same for each instruction and each possible input. Although the approach does not provide full formal verification, experiments with the approach confirm that due to a different way it explores the state space of the design under test, it can find bugs not found by functional verification, and is thus a useful complement to functional verification.

  • Název v anglickém jazyce

    Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

  • Popis výsledku anglicky

    The paper proposes an automated approach with a formal basis designed for checking correspondence between an RTL implementation of a microprocessor and a description of its instruction set architecture (ISA). The goals of the approach are to find bugs not discovered by functional verification, to minimize user intervention in the verification process, and to provide a developer with practical results within a short period of time. The main idea is to use bounded model checking to check that the output produced by automatically derived RTL and ISA models of a given processor are the same for each instruction and each possible input. Although the approach does not provide full formal verification, experiments with the approach confirm that due to a different way it explores the state space of the design under test, it can find bugs not found by functional verification, and is thus a useful complement to functional verification.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

    JC - Počítačový hardware a software

  • OECD FORD obor

Návaznosti výsledku

  • 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>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Ostatní

  • Rok uplatnění

    2012

  • 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ů

Údaje specifické pro druh výsledku

  • Název statě ve sborníku

    Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)

  • ISBN

    978-1-4673-4441-8

  • ISSN

  • e-ISSN

  • Počet stran výsledku

    6

  • Strana od-do

    6-12

  • Název nakladatele

    Institute of Electrical and Electronics Engineers

  • Místo vydání

    Austin, TX

  • Místo konání akce

    Austin, TX

  • Datum konání akce

    10. 12. 2012

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

    WRD - Celosvětová akce

  • Kód UT WoS článku