DocumentCode :
1096611
Title :
A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification
Author :
Manolios, Panagiotis ; Srinivasan, Sudarshan K.
Author_Institution :
Northeastern Univ., Boston
Volume :
16
Issue :
4
fYear :
2008
fDate :
4/1/2008 12:00:00 AM
Firstpage :
353
Lastpage :
364
Abstract :
We present a refinement-based compositional framework for showing that pipelined machines satisfy the same safety and liveness properties as their non-pipelined specifications. Our framework consists of a set of convenient, easily applicable, and complete compositional proof rules. We show how to apply our compositional framework in the context of microprocessor verification to verify both abstract, term-level models and executable, bit-level models. Our framework enables us to verify machine models that are significantly more complex than the kinds of models that can be verified using current state-of-the-art automated decision procedures. For example, using our framework, we can verify a 32-bit, 10-stage, executable pipelined machine model. In addition, our compositional framework offers drastic improvements in the context of design debugging over monolithic approaches, in part because bugs are isolated to particular steps in the compositional proof and because the counter examples generated are much smaller.
Keywords :
inference mechanisms; microcomputers; pipeline processing; automated decision; compositional proof rules; design debugging; microprocessor verification; monolithic approaches; pipelined machine model; pipelined machine verification; refinement-based compositional reasoning; Compositional reasoning; pipelined machine verification; refinement;
fLanguage :
English
Journal_Title :
Very Large Scale Integration (VLSI) Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
1063-8210
Type :
jour
DOI :
10.1109/TVLSI.2008.918120
Filename :
4469914
Link To Document :
بازگشت