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.
@techreport{BUT192973,
author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
title="Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors",
year="2014",
publisher="Faculty of Information Technology BUT",
address="Brno",
pages="18",
url="http://www.fit.vutbr.cz/research/groups/verifit/tools/hades/techrep/hades-techrep.pdf"
}