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

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.

Anglický abstrakt

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.

BibTex


@inproceedings{BUT119797,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  annote="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.",
  address="The Universidad de Las Palmas de Gran Canaria",
  booktitle="Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)",
  chapter="119797",
  edition="NEUVEDEN",
  howpublished="print",
  institution="The Universidad de Las Palmas de Gran Canaria",
  year="2015",
  month="february",
  pages="193--194",
  publisher="The Universidad de Las Palmas de Gran Canaria",
  type="conference paper"
}