IEICE TRANSACTIONS on Fundamentals
A Formal Verification Algorithm for Pipelined Processors
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E78-A No.5 pp.618-631
- Publication Date
- 1995/05/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- VLSI Design Technology and CAD
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Toru SHONAI, Tsuguo SHIMIZU, "A Formal Verification Algorithm for Pipelined Processors" in IEICE TRANSACTIONS on Fundamentals,
vol. E78-A, no. 5, pp. 618-631, May 1995, doi: .
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 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e78-a_5_618/_p
Copy
@ARTICLE{e78-a_5_618,
author={Toru SHONAI, Tsuguo SHIMIZU, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={A Formal Verification Algorithm for Pipelined Processors},
year={1995},
volume={E78-A},
number={5},
pages={618-631},
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 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.},
keywords={},
doi={},
ISSN={},
month={May},}
Copy
TY - JOUR
TI - A Formal Verification Algorithm for Pipelined Processors
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 618
EP - 631
AU - Toru SHONAI
AU - Tsuguo SHIMIZU
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E78-A
IS - 5
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - May 1995
AB - 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.
ER -
English
