Conference paper

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2015, pp. 193-194. ISBN 978-84-606-5438-4.
Publication language:english
Original title:Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Title (cs):Analýza hazardů v mikroprocesorech pomocí formální analýzy parametrizovaných systémů
Pages:193-194
Proceedings:Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)
Conference:Fifteenth International Conference on Computer Aided Systems Theory
Place:Las Palmas de Grand Canaria, ES
Year:2015
ISBN:978-84-606-5438-4
Publisher:The Universidad de Las Palmas de Gran Canaria
Keywords
microprocessor analysis, pipelined execution, WAW hazard, WAR hazard, formal verification, parameterized systems
Annotation
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.
Abstract
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{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}} Smr{\v{c}}ka
	and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Microprocessor Hazard Analysis via Formal Verification of
	Parameterized Systems},
   pages = {193--194},
   booktitle = {Proceedings of the 15th International Conference on Computer
	Aided Systems Theory (EUROCAST 2015)},
   year = {2015},
   location = {Las Palmas de Grand Canaria, ES},
   publisher = {The Universidad de Las Palmas de Gran Canaria},
   ISBN = {978-84-606-5438-4},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=10767}
}

Your IPv4 address: 54.163.209.109
Switch to IPv6 connection

DNSSEC [dnssec]