The productivity and scalability of verifying pipelined circuits can be increased by exploiting the structural and behavioural characteristics that distinguish pipelines from other circuits. This paper presents a formal model of pipelines that augments a state machine with information to describe the transfer of parcels between stages, and reading and writing state variables. Using our model, we created a definition of correctness that is based on the well-established principles of structural, control, and data hazards. We have proved that any pipeline that satisfies our hazards-based definition of correctness is guaranteed to satisfy the conventional correctness statement of Burch-Dill style flushing.

Original document

The different versions of the original document can be found in:

Back to Top

Document information

Published on 01/01/2011

Volume 2011, 2011
DOI: 10.1007/978-3-540-39724-3_8
Licence: CC BY-NC-SA license

Document Score


Views 1
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?