Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding

Toru SHONAI  Tsuguo SHIMIZU  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E82-D   No.2   pp.376-388
Publication Date: 1999/02/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Computer Hardware and Design
Keyword: 
formal verification,  processor,  pipeline,  superscalar,  

Full Text: PDF(2MB)>>
Buy this Article




Summary: 
This paper describes an algorithm and its prototype system--VeriProc/1. 1--which can prove the correctness of pipelined and superscalar processor controls automatically without a pipeline invariant, human interaction, or additional information. This algorithm is based on behavior-covering and partial unfolding. No timing relations such as an abstract function or β-relation is required. The only information required is to specify the location of the selectors in the design. Partial unfolding makes it possible to derive superscalar specifications from conventional specifications. Correctness proof of the partial unfolding is given. The prototype system can verify various superscalar control designs of simple processors.