Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 451

Fig. 21.1 Finite automaton

0 , 1

1

s 1 s 2 s 3

0 , 1

Example 21.5. The alphabet of the automaton depicted in Fig. 21.1 consists of two
letters: 0 and 1. The automaton has three states: s 1 , s 2 , and s 3 . There is one initial
state, s 1 , and one final state, s 3 . The transition relation consists of the following
triples: .s 1 ;0;s 1 /, .s 1 ;1;s 1 /, .s 1 ;1;s 2 /, .s 2 ;0;s 3 /, and .s 2 ;1;s 3 /.
This automaton is nondeterministic in the following sense: from state s 1 on
letter 1, the automaton can transition either to s 1 or to s 2 . t

accepts a word w on ˙ iff there is a path from one of its
initial states to one of its final states such that the successive transitions are labeled
by the consecutive letters from w . The set of the words accepted by the automaton
A

A finite automaton A

forms the language L. A /, called the language of the automaton A .

A

Example 21.6. defined in Example 21.5 accepts all words over

the alphabet f 0; 1 g that have length of at least two and 1 as the penultimate letter.

The automaton

t

21.2 Formal Verification Model

The DUT in FV is represented as a formal verification model , also known as a
Kripke structure .
The formal verification model M is a tuple h Q; I; V; R i , where Q is a set of
states, 2 I Q is the set of initial states, V is a finite set of Boolean variables, and
R Q Q is the transition relation. We also assume that the transition relation R
is total , i.e., for any q 2 Q there exists q 0 2 Q such that .q; q 0 / 2 R. In other words,
the relation is such that from any state there is at least one transition (possibly to the
same state). 3
Each state is characterized by the set of variables that are true in it. If two different
states have exactly the same set of variables true in them, then these states may be
merged into one. R contains all state pairs such that it is possible to transition from
the first state of the pair to the second one.

2 The definition does not require having a finite number of states, but we assume that their number
is finite since this is true for any RTL model.
3 In general, one includes in the definition of a Kripke structure a labeling function L W Q ! 2 V ,
which defines which Boolean variables are true in each state. In our case we just identify Q with
2 V , assuming that each state corresponds to some specific valuation of the variables.