Detail publikace

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Originální název

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Anglický název

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Jazyk

en

Originální abstrakt

The current stress on having a rapid development cycle for microprocessors featuring pipeline-based execution leads to a high demand of automated techniques supporting the design, including a support for its verification. We present an automated technique exploiting static analysis of data paths and formal verification of parameterized systems in order to discover flaws caused by improperly handled data hazards. In particular, as a complement of our previous work on read-after-write hazards, we focus on write-after-write and write-after-read hazards in microprocessors with a single pipeline.

Anglický abstrakt

The current stress on having a rapid development cycle for microprocessors featuring pipeline-based execution leads to a high demand of automated techniques supporting the design, including a support for its verification. We present an automated technique exploiting static analysis of data paths and formal verification of parameterized systems in order to discover flaws caused by improperly handled data hazards. In particular, as a complement of our previous work on read-after-write hazards, we focus on write-after-write and write-after-read hazards in microprocessors with a single pipeline.

BibTex


@inproceedings{BUT120023,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  annote="The current stress on having a rapid development cycle for microprocessors
featuring pipeline-based execution leads to a high demand of automated techniques
supporting the design, including a support for its verification. We present an
automated technique exploiting static analysis of data paths and formal
verification of parameterized systems in order to discover flaws caused by
improperly handled data hazards. In particular, as a complement of our previous
work on read-after-write hazards, we focus on write-after-write and
write-after-read hazards in microprocessors with a single pipeline.",
  address="Springer International Publishing",
  booktitle="Computer Aided Systems Theory - EUROCAST 2015",
  chapter="120023",
  doi="10.1007/978-3-319-27340-2_75",
  edition="Lecture Notes in Computer Science",
  howpublished="online",
  institution="Springer International Publishing",
  number="1",
  year="2015",
  month="december",
  pages="605--614",
  publisher="Springer International Publishing",
  type="conference paper"
}