Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach--
Summary :
The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.
- Publication
- IEICE TRANSACTIONS on Information Vol.E78-D No.7 pp.791-795
- Publication Date
- 1995/07/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems)
- Category
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
Hiromi HIRAISHI, "Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach--" in IEICE TRANSACTIONS on Information,
vol. E78-D, no. 7, pp. 791-795, July 1995, doi: .
Abstract: The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.
URL: https://global.ieice.org/en_transactions/information/10.1587/e78-d_7_791/_p
Copy
@ARTICLE{e78-d_7_791,
author={Hiromi HIRAISHI, },
journal={IEICE TRANSACTIONS on Information},
title={Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach--},
year={1995},
volume={E78-D},
number={7},
pages={791-795},
abstract={The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.},
keywords={},
doi={},
ISSN={},
month={July},}
Copy
TY - JOUR
TI - Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach--
T2 - IEICE TRANSACTIONS on Information
SP - 791
EP - 795
AU - Hiromi HIRAISHI
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E78-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 1995
AB - The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.
ER -
English
