(Created page with " == Abstract == The productivity and scalability of verifying pipelined circuits can be increased by exploiting the structural and behavioural characteristics that distinguis...") |
|||
| (One intermediate revision by the same user not shown) | |||
| Line 3: | Line 3: | ||
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. | 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. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| Line 15: | Line 10: | ||
* [https://link.springer.com/content/pdf/10.1007%2F978-3-540-39724-3_8.pdf https://link.springer.com/content/pdf/10.1007%2F978-3-540-39724-3_8.pdf] | * [https://link.springer.com/content/pdf/10.1007%2F978-3-540-39724-3_8.pdf 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://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 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://link.springer.com/chapter/10.1007%2F978-3-540-39724-3_8], | ||
| + | : [https://dblp.uni-trier.de/db/conf/charme/charme2003.html#Aagaard03 https://dblp.uni-trier.de/db/conf/charme/charme2003.html#Aagaard03], | ||
| + | : [https://www.scipedia.com/public/Aagaard_2011a https://www.scipedia.com/public/Aagaard_2011a], | ||
| + | : [https://rd.springer.com/chapter/10.1007/978-3-540-39724-3_8 https://rd.springer.com/chapter/10.1007/978-3-540-39724-3_8], | ||
| + | : [https://academic.microsoft.com/#/detail/1582175290 https://academic.microsoft.com/#/detail/1582175290] | ||
Latest revision as of 14:10, 21 January 2021
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:
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
Share this document
Keywords
claim authorship
Are you one of the authors of this document?