IEICE TRANSACTIONS on Fundamentals
Formal Verification System for Pipelined Processors
Summary :
This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. 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. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E79-A No.6 pp.883-891
- Publication Date
- 1996/06/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, "Formal Verification System for Pipelined Processors" in IEICE TRANSACTIONS on Fundamentals,
vol. E79-A, no. 6, pp. 883-891, June 1996, doi: .
Abstract: This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. 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. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e79-a_6_883/_p
Copy
@ARTICLE{e79-a_6_883,
author={Toru SHONAI, Tsuguo SHIMIZU, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Formal Verification System for Pipelined Processors},
year={1996},
volume={E79-A},
number={6},
pages={883-891},
abstract={This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. 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. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.},
keywords={},
doi={},
ISSN={},
month={June},}
Copy
TY - JOUR
TI - Formal Verification System for Pipelined Processors
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 883
EP - 891
AU - Toru SHONAI
AU - Tsuguo SHIMIZU
PY - 1996
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E79-A
IS - 6
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - June 1996
AB - This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. 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. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.
ER -
English
