Title :
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
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;
Conference_Titel :
Test Symposium, 1994., Proceedings of the Third Asian
Conference_Location :
Nara
Print_ISBN :
0-8186-6690-0
DOI :
10.1109/ATS.1994.367217
