(Created page with " == Abstract == The productivity and scalability of verifying pipelined circuits can be increased by exploiting the structural and behavioural characteristics that distinguis...") |
m (Scipediacontent moved page Draft Content 554539835 to Aagaard 2011a) |
(No difference)
| |
Revision as of 13:21, 14 October 2020
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.
Document type: Part of book or chapter of book
Full document
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?