This paper extends Floyd's inductive assertion method to formal verification of register transfer level (RTL) hardware descriptions. An RTL description with imbedded assertions about machine state will be the input to the verifier. The formal semantics ...
An automated framework for verification of low power transformations in register transfer level (RTL) designs is presented in this paper. Our verification method consists in two steps. In the first step, the data path interconnection and the controller ...
Out-of-order execution is a fundamental technique to achieve instruction-level parallelization in processor designs. The verification of out-of-order processor is a main challenge in processor design. This paper presents a formal method to model and ...
IEEE Computer Society Press
Washington, DC, United States
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in