Publication detail

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

CHARVÁT, L. SMRČKA, A. VOJNAR, T.

Original Title

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

English Title

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

Type

conference paper

Language

en

Original Abstract

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.

English abstract

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.

Keywords

automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking

RIV year

2012

Released

10.12.2012

Publisher

Institute of Electrical and Electronics Engineers

Location

Austin, TX

ISBN

978-1-4673-4441-8

Book

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

Edition

NEUVEDEN

Edition number

NEUVEDEN

Pages from

6

Pages to

12

Pages count

6

URL

BibTex


@inproceedings{BUT97556,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description",
  annote="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.",
  address="Institute of Electrical and Electronics Engineers",
  booktitle="Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)",
  chapter="97556",
  doi="10.1109/MTV.2012.19",
  edition="NEUVEDEN",
  howpublished="online",
  institution="Institute of Electrical and Electronics Engineers",
  year="2012",
  month="december",
  pages="6--12",
  publisher="Institute of Electrical and Electronics Engineers",
  type="conference paper"
}