YetmoreimagecomputationsforSMV,thesymbolicmodelverifier资源-CSDN文库

论文

需积分: 5 54 浏览量 2021-06-29 19:44:31 上传评论收藏 128KB PDF 举报

资源推荐

资源详情

资源评论

Yet More Image Computations for SMV, the Symbolic Model

Ve rifier

Hiromi Hiraishi

Faculty of Engineering, Kyoto Sangyo University, Kyoto, Japan 603-8555

SUMMARY

This paper describes a collection of techniques to

improve the efficiency of the pre- and postimage computa-

tions that are the core of the Symbolic Model Verifier

(SMV), which is used for formal logic design verification.

The proposed techniques aim mostly at improving the

efficiency of the verification of asynchronous processes.

The improvements are mainly made by (1) the early elimi-

nation of process variables in the postimage computations,

(2) the application of the conjunctive partitioning technique

to the verification of asynchronous processes, (3) the early

substitution of the stable state variables, and (4) the nonde-

terministic substitution method for the preimage computa-

tions. The experimental measurements show that the

proposed techniques are very effective and result in a

speedup of up to 50 times compared to the original SMV.

2000

Key words: Formal design verification; symbolic

model checking; image computation; asynchronous proc-

ess; SMV.

1. Introduction

As the logic systems to be designed become larger

and more complex, the designers are more apt to make

design errors. Logic simulations have been widely used to

find design errors. However, it is hard to guarantee the

correctness of the logic design by simulations because the

simulations cannot cover all cases. Therefore, formal de-

sign verification is important to guarantee that the designs

meet their specifications.

The symbolic model checking [2, 3] of Computation

Tree Logic (CTL) [1] is one of the most practical ap-

proaches to formal logic design verification. In this ap-

proach, logic systems to be designed are modeled as finite

state transition systems. Their specifications are described

in CTL. Then, symbolic model checking examines if the

designs satisfy the specifications. The Symbolic Model

Verifier (SMV) [6, 14] based on this approach has been

developed at Carnegie-Mellon University, which suc-

ceeded in verifying large logic systems whose state space

exceeds 10

In symbolic model checking, a set of states and a

transition relation are represented by Boolean expressions.

The verification algorithm is based on the manipulations of

these Boolean expressions. Furthermore, a Binary Decision

Diagram (BDD) [4, 5] is used to manipulate Boolean ex-

pressions. There have been proposed various methods to

improve the efficiency of symbolic model checking [712],

which enable us to verify large practical logic designs.

The size of the BDD is, however, apt to explode in

verification of large logic systems. We often have to con-

struct an abstract model in order to verify more complex

Systems and Computers in Japan, Vol. 31, No. 9, 2000

Translated from Denshi Joho Tsushin Gakkai Ronbunshi, Vol. J82-D-I, No. 7, July 1999, pp. 791798

The author would like to express his appreciation to Professor E.M. Clarke

of Carnegie-Mellon University for valuable suggestions. The major part

of this research was done during his stay at CMU supported by the foreign

research study program of Kyoto Sangyo University. Part of this research

was supported by a grant of scientific research from the Ministry of

Education of Japan.

and larger logic designs. In such an abstract model, a system

is often represented as a set of asynchronous processes

(modules).

In the verification of asynchronous processes, a cou-

ple of methods based on partial orders over events have

been proposed [15, 16] to improve the efficiency by de-

creasing the reachable state space. However, as far as the

author knows, no approaches have been proposed to im-

prove the efficiency of symbolic model checking directly

by considering the characteristics of asynchronous proc-

esses. Accordingly, we tried to improve the symbolic model

checking algorithm of SMV in order to improve the effi-

ciency of the verification of asynchronous processes. The

major techniques used for the improvement include:

x Early smoothing of the process selection vari-

ables, which accelerates the postimage computa-

tions that are used for computing the reachable

states.

x Provision for application of the conjunctive parti-

tioning technique to each asynchronous process.

x Early substitution of the corresponding next state

variables to the stable state variables in the

postimage computation for each process based on

the conjunctive partitioning technique.

x Preimage computation based on nondeterministic

substitution. This is an extension of the efficient

deterministic substitution method for preimage

computation.

The experimental measurements for these techniques have

shown that they are effective and can enhance efficiency

greatly.

Section 2 presents the notations and the basic opera-

tions of symbolic model checking. The transition relations

generated by SMV are also explained. In Section 3 a

postimage computation algorithm based on early smooth-

ing of the process selection variables is proposed. Section

4 shows how to apply the conjunctive partitioning tech-

nique to the image computations of asynchronous proc-

esses. A postimage computation algorithm based on early

substitution to the stable state variables is proposed in

section 5, and a preimage computation algorithm based on

nondeterministic substitution is proposed in Section 6. Sec-

tions 3, 5, and 6 also present the results of the experimental

measurements, all of which were measured on a Sparc Ultra

II 250 MHz clock.

2. Preliminaries

This section presents the basic notations and the

definitions related to symbolic model checking. The transi-

tion relations generated by SMV are also explained.

2.1. Symbolic model checking

In SMV the logic systems under verification are

represented by the finite state transition systems called

Kripke structures. The specifications that the logic sys-

tems should satisfy are described in CTL temporal logic

formulas.

Definition 1 Kripke structure is defined by a 4-tuple



S, R

I, S

, where S is a finite set of states, R  S u S

is a total binary relation on the states. It is assumed that

every state has at least one next state. Let AP be a set of

atomic propositions. I : S o 2

gives a set of atomic

propositions true at the state. S

 S is a set of initial states.

Whether the designed system meets its specifications

is verified by symbolic model checking. In symbolic model

checking, the set of states where the specification holds is

calculated by postimage computations and/or preimage

computations. Postimage computation gives a set of the

next states of the given set of current states, whereas the

preimage computation gives a set of the previous states of

the given current states. These image computations are done

by Boolean formula manipulations based on BDD.

Let B = {0, 1} be a set of Boolean values. Let s

be a

variable over B. s

s

, s

, . . . , s



denotes a vector of

state variables. Then a subset A of the state space

can be represented by the n-variable Boolean func-

tion F

s : S o B that satisfies the following equation:

is called a characteristic function of A.

Let s

be a next state variable over B.

s

, . . .

 denotes a vector of next state variables.

Then the transition relation can be given by the 2n-variable

Boolean function F

s, sc : S u S o

that satisfies the

following equation:

is called a transition relation function.

If there are no possibilities of confusions, we will use

A and R instead of F

and F

hereafter.

Let fs be a Boolean function of n variables. Smooth-

ing operations, s

. and s., are defined as follows:

The machine used for the measurements was an Ultra Enterprise 6000

(20 CPU, 8 GB memory). Up to 18 measurements were done in parallel.

The maximum memory required for each measurement was at most 200

MB.

In the case of S 

, we can regard B

as the state space by appropriately

adding the states unreachable from the initial states.

剩余8页未读，继续阅读

评论收藏

内容反馈

weixin_38576811

粉丝: 6
资源: 890

Yet more image computations for SMV, the symbolic model verifier

最新资源

Yet more image computations for SMV, the symbolic model verifier

符号模型验证器 SMV 的更多图像计算

SMV 模型检测

Symbolic data analysis

形式化建模验证SMV模型检验器

Programming for Computations – MATLAB/Octave

Matrix_Computations_for_Signal_Processing

英文原版-Hidden Markov Models for Time Series 2nd Edition

Web Microanalysis of Big Image Data

Statistics for Machine Learning: Techniques for exploring supervised

statistic books for machine learning

Statistics for Machine Learning

rotating data for neural network computations

Programming for Computations Python pdf 0分

Programming for Computations - Python

Matrix Computations Fourth Edition

Getting Started with TensorFlow

Matlab 总学术人数 (TAH) 工具箱.pdf

Handbook for matrix computations.pdf

Programming-for-Computations-Python-A-Gentle-Introduction-to-Numerical-Simulations-with-Python (1).pdf.pdf

Parallelism in Matrix Computations pdf

Introduction to MATLAB for Engineers

matrix computations 4th edition

Factor Graphs for Robot Perception.pdf

Numerical Methods for StochasticComputations-A Spectral Method Approach

最新资源