Paper Info
Title
Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study
Abstract
There is a large class of circuits (including pipeline and out-of-order execution components) which can be formally verified while completely ignoring the precise characteristics (e.g. word-size) of the data manipulated by the circuits. In the literature, this is often described as the use of uninterpreted functions, implying that the concrete operations applied to the data are abstracted into unknown and featureless functions. In this paper, we briefly introduce an abstract unifying model for such data-insensitive circuits, and claim that the development of such models, perhaps even a theory of circuit schemas, can significantly contribute to the development of efficient and comprehensive verification algorithms combining deductive as well as enumerative methods.As a case study, we present in this paper an algorithm for out-of-order execution with in-order retirement and show it to be a refinement of the sequential instruction execution algorithm. Refinement is established by deductively proving (using pvs) that the register files of the out-of-order algorithm and the sequential algorithm agree at all times if the two systems are synchronized at instruction retirement time.
Year
DOI
Venue
1998
10.1007/3-540-49519-3_23
FMCAD
Keywords
Field
DocType
out-of-order algorithm,out-of-order execution component,circuit schema,abstract unifying model,sequential algorithm,in-order retirement,sequential instruction execution algorithm,data-insensitive circuits,case study,in-order-retirement case study,instruction retirement time,out-of-order execution,out of order execution,unified model,out of order,register file
Transition system,Synchronization,Computer science,Program counter,Circuit design,Real-time computing,Finite-state machine,Theoretical computer science,Formal specification,Electronic circuit,Sequential algorithm,Distributed computing
Conference
ISBN
Citations 
PageRank 
3-540-65191-8
8
0.69
References 
Authors
28
2
Name
Order
Citations
PageRank
Amir Pnueli1129642377.59
Tamarah Arons227814.59