About: Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727
Description	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. 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. (en)
Title	Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description (en)
skos:prefLabel	Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description (en)
skos:notation	RIV/00216305:26230/12:PU102230!RIV14-MPO-26230___
http://linked.open...avai/predkladatel	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(ED1.1.00/02.0070), P(FR-TI1/038), P(GAP103/10/0306), P(OC10009), S, Z(MSM0021630528)
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš Smrčka, Aleš Charvát, Lukáš
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	124189
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/12:PU102230
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking (en)
http://linked.open.../riv/klicoveSlovo	ISA automatic formal verification correspondence checking RTL bounded model checking microprocessor instruction
http://linked.open...ontrolniKodProRIV	[9CB13FCB590E]
http://linked.open...v/mistoKonaniAkce	Austin, TX
http://linked.open...i/riv/mistoVydani	Austin, TX
http://linked.open...i/riv/nazevZdroje	Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	IT4Innovations Centre of Excellence System for Programming and Realization of Embedded Systems Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
http://linked.open...UplatneniVysledku	2012
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Smrčka, Aleš Charvát, Lukáš
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2012-12-10 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
number of pages	6 (xsd:int)
http://bibframe.org/vocab/doi	10.1109/MTV.2012.19
http://purl.org/ne...btex#hasPublisher	Institute of Electrical and Electronics Engineers
https://schema.org/isbn	978-1-4673-4441-8
http://localhost/t...ganizacniJednotka	26230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software