A hazards based correctness statement for pipelined circuits

Abstract

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:

• https://link.springer.com/content/pdf/10.1007%2F978-3-540-39724-3_8.pdf

• http://link.springer.com/content/pdf/10.1007/978-3-540-39724-3_8,

http://dx.doi.org/10.1007/978-3-540-39724-3_8

• https://link.springer.com/chapter/10.1007%2F978-3-540-39724-3_8,

https://dblp.uni-trier.de/db/conf/charme/charme2003.html#Aagaard03,

https://www.scipedia.com/public/Aagaard_2011a,

https://rd.springer.com/chapter/10.1007/978-3-540-39724-3_8,

https://academic.microsoft.com/#/detail/1582175290