A FORMAL VERIFICATION ALGORITHM FOR PIPELINED PROCESSORS

Authors
SHONAI T SHIMIZU T
Citation
T. Shonai et T. Shimizu, A FORMAL VERIFICATION ALGORITHM FOR PIPELINED PROCESSORS, IEICE transactions on fundamentals of electronics, communications and computer science, E78A(5), 1995, pp. 618-631
Citations number
NO
Categorie Soggetti
Engineering, Eletrical & Electronic","Computer Science Hardware & Architecture","Computer Science Information Systems
Journal title
IEICE transactions on fundamentals of electronics, communications and computer science → ACNP
ISSN journal
09168508
Volume
E78A
Issue
5
Year of publication
1995
Pages
618 - 631
Database
ISI
SICI code
0916-8508(1995)E78A:5<618:AFVAFP>2.0.ZU;2-Q
Abstract
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 ne w type of mathematical induction: extended recursive induction. After the user indicates only selectors in the design, this algorithm can au tomatically prove processors having more than 10((1010)) states. The a lgorithm is manuary applied to benchmark processors with pipelined con trol, and we discuss how data width, memory size, and the numbers of p ipeline stages and instructions influence the computation cost of prov ing the correctness of the processors. Further, this algorithm can be used to generate a pipeline invariant.