Publication Details
Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
automatic formal verification, microprocessor, register transfer level description, parameterised system, RAW hazard
Implementation of a pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting design. Various techniques were proposed for this purpose, but they usually require a significant manual intervention of the developers. In this work, we propose a novel, highly automated approach for discovering RAW hazards in in-order pipelined instruction execution. Our approach combines static analysis of data paths to detect anomalies and possible hazards, followed by a transformation of detected problematic paths to a parameterised system, and a subsequent formal verification to check the possibility of unhandled hazards using techniques for formal verification of parameterised systems. We have implemented our approach and successfully applied it on multiple non-trivial microprocessors.
@inproceedings{BUT119794,
author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
title="Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors",
booktitle="Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)",
year="2014",
pages="83--89",
publisher="IEEE Computer Society",
address="Austin, TX",
doi="10.1109/MTV.2014.21",
isbn="978-1-4673-6858-2",
url="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240"
}