Browse Prior Art Database

Technique for Verifying Finite State Machines

IP.com Disclosure Number: IPCOM000035753D
Original Publication Date: 1989-Aug-01
Included in the Prior Art Database: 2005-Jan-28
Document File: 4 page(s) / 57K

Publishing Venue

IBM

Related People

Bahnsen, RJ: AUTHOR [+2]

Abstract

This invention provides a way of verifying the behavior of a (target) finite state machine by means of an assertion machine. The observable behavior of a state machine is the set of sequences of input and output vectors that can occur during the operation of the machine. A statement about some property of these sequences is an assertion. A general way to describe a property is to describe a machine which recognizes that property. (Image Omitted)

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 48% of the total text.

Page 1 of 4

Technique for Verifying Finite State Machines

This invention provides a way of verifying the behavior of a (target) finite state machine by means of an assertion machine. The observable behavior of a state machine is the set of sequences of input and output vectors that can occur during the operation of the machine. A statement about some property of these sequences is an assertion. A general way to describe a property is to describe a machine which recognizes that property.

(Image Omitted)

A target machine is the machine, e.g., an IBM 370 CPU, for which assertions are made.

An assertion machine is a state machine whose input vectors are the concatenation of the input and output vectors of a target machine, and whose output vector is a single bit whose value is 0 (false) as long as the inputs and outputs of the target machines are behaving properly, and 1 (true) if an improper sequence of target machine inputs and outputs is detected.

A mapping machine can be used to translate between the input and output vectors of the target machine and those of an architectural machine in terms of which the assertions are made. This allows one assertion machine to be used for a class of several similar target machines.

The target, assertion, and (optional) mapping machines are connected as in Fig. 1 to form a new verification machine, shown in Fig. 2, with an input vector JV,

an output vector PV (single bit),

a state vector LV = LT LA LM,

a transition function TV:JV LV- LV, and

an output function ZV:JV LV- PV

(where LT, LA, and LM are the state vectors of the target, assertion, and mapping machines, respectively, and represents concatenation). The initial state of the machine must be at least partially specified. A general way to do this is to provide a valid initial state recognition function V(LV), which is true for a valid initial state LV.

The verification problem then becomes: starting from an initial state LV for which V(LV)=1, is there a sequence of input vectors that ever causes the output vector (a single bit) to become true? That is, the verification machine is a model that is used to find a concrete sequence of input vectors which cause a target machine to exhibit improper behavior.

This invention uses Bryant's canonical graphic expressions [*] for Boolean functions to develop a characteristic function G*(LV,LV'), from which the possibility of improper behavior of the target machine can be determined. A sequence of input vectors which will cause the improper behavior can also be discovered.

1

Page 2 of 4

From the verification machine's transition function TV: (JV, LV) LV' form a new function G0: (LV, LV') B where B is the set of Boolean values 0 and 1. The meaning of G0 is, can the state LV' follow immediately from the state LV, for some input values of the verification machine? If so, then G0(LV, LV') = 1; otherwise G0(LV, LV') = 0.

An expression for G0 can be produced by the following technique. First, form an intermediate function...