The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We present a refinement-based compositional framework for showing that pipelined machines satisfy the same safety and liveness properties as their non-pipelined specifications. Our framework consists of a set of convenient, easily applicable, and complete compositional proof rules. We show how to apply our compositional framework in the context of microprocessor verification to verify both abstract, term-level models and executable, bit-level models. Our framework enables us to verify machine models that are significantly more complex than the kinds of models that can be verified using current state-of-the-art automated decision procedures. For example, using our framework, we can verify a 32-bit, 10-stage, executable pipelined machine model. In addition, our compositional framework offers drastic improvements in the context of design debugging over monolithic approaches, in part because bugs are isolated to particular steps in the compositional proof and because the counter examples generated are much smaller.
How it got here
How it got here
agent via openalex
Added
2026-10-25 17:20 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@article{manolios2008refinementbased,
title = {A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification},
author = {Panagiotis Manolios and Sudarshan K. Srinivasan},
year = {2008},
journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
publisher = {Institute of Electrical and Electronics Engineers},
volume = {16},
number = {4},
pages = {353--364},
doi = {10.1109/tvlsi.2008.918120},
}