The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
이 문서에서는 알고리즘과 해당 프로토타입 시스템인 VeriProc/1에 대해 설명합니다. 1--파이프라인 불변, 인간 상호 작용 또는 추가 정보 없이 파이프라인 및 수퍼스칼라 프로세서 제어의 정확성을 자동으로 증명할 수 있습니다. 이 알고리즘은 행동 커버링과 부분 전개를 기반으로 합니다. 추상 함수나 β-관계와 같은 타이밍 관계는 필요하지 않습니다. 필요한 유일한 정보는 디자인에서 선택기의 위치를 지정하는 것입니다. 부분 전개를 통해 기존 사양에서 수퍼스칼라 사양을 도출할 수 있습니다. 부분 전개의 정확성 증명이 제공됩니다. 프로토타입 시스템은 간단한 프로세서의 다양한 수퍼스칼라 제어 설계를 검증할 수 있습니다.
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.
부
Toru SHONAI, Tsuguo SHIMIZU, "Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding" in IEICE TRANSACTIONS on Information,
vol. E82-D, no. 2, pp. 376-388, February 1999, doi: .
Abstract: This paper describes an algorithm and its prototype system--VeriProc/1. 1--which can prove the correctness of pipelined and superscalar processor controls automatically without a pipeline invariant, human interaction, or additional information. This algorithm is based on behavior-covering and partial unfolding. 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. Partial unfolding makes it possible to derive superscalar specifications from conventional specifications. Correctness proof of the partial unfolding is given. The prototype system can verify various superscalar control designs of simple processors.
URL: https://global.ieice.org/en_transactions/information/10.1587/e82-d_2_376/_p
부
@ARTICLE{e82-d_2_376,
author={Toru SHONAI, Tsuguo SHIMIZU, },
journal={IEICE TRANSACTIONS on Information},
title={Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding},
year={1999},
volume={E82-D},
number={2},
pages={376-388},
abstract={This paper describes an algorithm and its prototype system--VeriProc/1. 1--which can prove the correctness of pipelined and superscalar processor controls automatically without a pipeline invariant, human interaction, or additional information. This algorithm is based on behavior-covering and partial unfolding. 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. Partial unfolding makes it possible to derive superscalar specifications from conventional specifications. Correctness proof of the partial unfolding is given. The prototype system can verify various superscalar control designs of simple processors.},
keywords={},
doi={},
ISSN={},
month={February},}
부
TY - JOUR
TI - Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding
T2 - IEICE TRANSACTIONS on Information
SP - 376
EP - 388
AU - Toru SHONAI
AU - Tsuguo SHIMIZU
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E82-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 1999
AB - This paper describes an algorithm and its prototype system--VeriProc/1. 1--which can prove the correctness of pipelined and superscalar processor controls automatically without a pipeline invariant, human interaction, or additional information. This algorithm is based on behavior-covering and partial unfolding. 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. Partial unfolding makes it possible to derive superscalar specifications from conventional specifications. Correctness proof of the partial unfolding is given. The prototype system can verify various superscalar control designs of simple processors.
ER -