A Formal Verification Algorithm for Pipelined Processors


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: 
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: VLSI Design Technology and CAD
formal verification,  hardware verification,  specifications,  design correctness,  proof,  pipeline invariant,  

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

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.