A Formal Verification Algorithm for Pipelined Processors

Toru SHONAI  Tsuguo SHIMIZU  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E78-A   No.5   pp.618-631
Publication Date: 1995/05/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: VLSI Design Technology and CAD
Keyword: 
formal verification,  hardware verification,  specifications,  design correctness,  proof,  pipeline invariant,  

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




Summary: 
We describe a formal verification algorithm for pipelined processors. This algorithm proves the equivalence between a processor's design and its specifications by using rewriting of recursive functions and a new type of mathematical induction: extended recursive induction. After the user indicates only selectors in the design, this algorithm can automatically prove processors having more than 10(1010) states. The algorithm is manuary applied to benchmark processors with pipelined control, and we discuss how data width, memory size, and the numbers of pipeline stages and instructions influence the computation cost of proving the correctness of the processors. Further, this algorithm can be used to generate a pipeline invariant.