Time-space modal logic for verification of bit-slice circuits

Hiromi Hiraishi

doi:10.1117/12.235564

22 March 1996 Time-space modal logic for verification of bit-slice circuits

Hiromi Hiraishi

Proceedings Volume 2644, Fourth International Conference on Computer-Aided Design and Computer Graphics; (1996) https://doi.org/10.1117/12.235564
Event: Fourth International Conference on Computer-Aided Design and Computer Graphics, 1995, Wuhan, China

Abstract

The major goal of this paper is to propose a new modal logic aiming at formal verification of bit-slice circuits. The new logic is called as time-space modal logic and its major feature is that it can handle two transition relations: one for time transition and the other for space transition. As for a verification algorithm, a symbolic model checking algorithm of the new logic is shown. This could be applicable to verification of bit-slice microprocessor of infinite bit width and 1D systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.

Citation Download Citation

Hiromi Hiraishi "Time-space modal logic for verification of bit-slice circuits", Proc. SPIE 2644, Fourth International Conference on Computer-Aided Design and Computer Graphics, (22 March 1996); https://doi.org/10.1117/12.235564

ACCESS THE FULL ARTICLE

INSTITUTIONAL
Select your institution to access the SPIE Digital Library.

SELECT YOUR INSTITUTION

PERSONAL
Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.

PERSONAL SIGN IN

No SPIE Account? Create one

PURCHASE THIS CONTENT

SUBSCRIBE TO DIGITAL LIBRARY

50 downloads per 1-year subscription

Members: $195

Non-members: $335 ADD TO CART

25 downloads per 1 - year subscription

Members: $145

Non-members: $250 ADD TO CART

PURCHASE SINGLE ARTICLE

Includes PDF, HTML & Video, when available