Time-space modal model checking towards verification of bit-slice architecture

Author

Hiraishi, Hiromi

Author_Institution

Dept. of Inf. & Commun. Sci., Kyoto Sangyo Univ., Japan

fYear

1994

fDate

15-17 Nov 1994

Firstpage

287

Lastpage

291

Abstract

The goal of this paper is to propose a new symbolic model checking approach named time-space modal modal 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

bit-slice computers; computer architecture; formal logic; logic testing; symbolic substitution; systolic arrays; VLSI; benchmark; bit-slice architecture; bit-slice microprocessor; effectiveness; infinite bit width; one dimensional systolic array; symbolic model; time-space modal model; verification; Formal verification; Logic circuits; Logic design; Microprocessors; Protocols; Sequential circuits; Signal processing; Signal processing algorithms; Systolic arrays; Very large scale integration;

fLanguage

English

Publisher

ieee

Conference_Titel

Test Symposium, 1994., Proceedings of the Third Asian

Conference_Location

Nara

Print_ISBN

0-8186-6690-0

Type

conf

DOI

10.1109/ATS.1994.367217

Filename

367217

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=287949