FORMAL VERIFICATION OF DIGITAL CIRCUITS USING SYMBOLIC MODEL CHECKING
Aleš Časar, Zmago Brezočnik, Tatjana Kapus University of Maribor, Faculty of Electrical Engineering and Computer
Science, Slovenia
Keywords: electrotechnics, computer science, digital circuits, BDD, Binary Decision Diagrams, FSM, Final State Machines, transition relations, characteristic functions, reachable states, CTL, Computation Tree Logic, fairness constraints, formal verification, symbolic model checking, computer software, software packages, experimental results
Abstract: This paper presents efficient algorithms for digital circuit verification. The algorithms are based on symbolic CTL (Computation Tree Logic) model checking. We also present an extension of ordinary CTL with fairness constraints. They enable verification of circuits with symbolic model checking regarding only fair paths in the computation tree. The model checking algorithms were implemented as part of a fully home-made program package for manipulating finite state machine descriptions of digital circuits, represented with Boolean functions. The package is also based on a fully home-made program package for manipulating Boolean functions, represented with binary decision diagrams.
Formalna verifikacija digitalnih vezij s simboličnim
preverjanjem modelov
Ključne besede: elektrotehnika, računalništvo, vezja digitalna, BDD grafi odločitveni binarni, FSM stroji stanj končnih, relacije prehajalne, funkcije karakteristične, stanja dosegljiva, CTL logika drevesa izračunavanj, omejitve poštenostne, verifikacija formalna, preverjanje modelov simbolično, oprema programska računalniška, paketi opreme programske, rezultati eksperimentalni
Povzetek: V članku predstavljamo učinkovite algoritme za verifikacijo digitalnih vezij. Algoritmi temeljijo na simboličnem preverjanju modelov z logiko drevesa izvajanj ("Computation Tree Logic" - CTL). Prav tako predstavljamo razširitev navadnega CTL s poštenostnimi omejitvami, ki omogočajo verifikacijo vezij samo vzdolž poštenih poti v drevesu izvajanj. Algoritmi za preverjanje modelov so implementirani kot del povsem domačega programskega paketa za obdelavo opisov digitalnih vezij s končnimi avtomati, predstavljenih z logičnimi funkcijami, ki temelji na prav tako povsem domačem paketu za obdelavo logičnih funkcij, predstavljenih z binarnimi odločitvenimi grafi.
1 Introduction
The manipulation of finite state machines (FSMs) is very common nowadays in the areas of digital circuit design like formal verification, automatic synthesis, and testing [12], One of the main problems that must be solved is the verification of properties of FSMs representing digital circuits.
The properties are often specified by computation tree logic (CTL) because with a properly written CTL formula it can automatically be verified if certain property is valid in a FSM or not. Everything, CTL formulas, the set of states of the FSM, and its transition relation can be uniquely represented as Boolean functions, which can be very efficiently represented with binary decision diagrams (BDDs). Using symbolic state space traversal and model checking, we can avoid combinatorial explosion, which is one of the main problems with enumeration-based methods.
Unfortunately, it is impossible to specify all properties in CTL. A significant part of such properties are those that could be specified in CTL, but we want them to be verified only in a FSM constrained to normal (fair) paths in order to avoid singularities and similar things. The problem is solved by the introduction of fairness constraints, which constrain the FSM to fair paths, so that the properties can be verified in the usual way.
The purpose of this paper is to present the model checking algorithms which we implemented within fully home-made program package for manipulating finite state machine descriptions of digital circuits, represented with Boolean functions. The algorithms have performed very well.
In Section 2 we briefly review BDDs and show how to represent FSMs with them. Section 3 describes the methods of searching reachable states. The main part of the paper is Section 4 where we present algorithms for symbolic model checking in CTL. Algorithms for symbolic model checking using fairness constraints are described in Section 5. Experimental results for benchmark circuits are given in Section 6. We conclude with some discussion and plans for future work.
2 Preliminaries
Binary decision diagrams (BDDs) are compact canonical representations of Boolean functions [2], Their size is closely related to the variable ordering. The manipulation of Boolean functions represented with BDDs is very efficient. Hence, BDDs have become widely used in various CAD applications, including state space traversal and model checking.
BDDs can also be used for representing and manipulating sets if we represent sets by means of their
characteristic functions. If is a subset of {0,l}",
its characteristic function Xj ■ (O^l}' (Oj) 'S defined by
Xj

\-yeJ
(1)
Thus, set operations can be perfonned by Boolean operations over the corresponding characteristic functions (e.g., xjc = Xj • Xj^b X^^g - Xj ■ Xß)-	shorter notation
we will denote x_j by A in the rest of the paper.
Since the characteristic functions are Boolean, we can efficiently manipulate them with BDDs.
A detenninistic finite state machine (FSM) M is a sixtuple M =	, where I is a
finite set of input symbols, ^ a finite set of states, 0 a finite set of output symbols, 5 . S xY. S a state transition function,	an output
function, and ^^ e an initial state.
If we want to realize a FSM by a digital circuit, we will have to encode the sets S, 2, and 0 by binary symbols (e.g., 0 and 1). States are encoded by state variables. At least n = S\ state vari-
ables.
m =
logj E input variables, and
I = logj 0 output variables of the circuit are
needed. Let IJ, X, and .Z represent the set of state variables, the set of input variables, and the set of output variables, respectively.
Once the states and the input symbols of the circuit are encoded, we denote a state transition function as 5 : (0,1)" x {0,l}'" ^ {O,!}". Then, next state variables are functions of present state variables and input variables. We denote next state variables by an added prime (') and write a transition function of a
state variable y. as

(2)
for i -	We rather introduce transition
relations
Namely, relations have much greater expressive power than functions [3]. With relations it is very easy to handle nondeterminism and to perfonn
backward reachability search that is relatively difficult with functions. Transition relations T. can be combined by tal<ing their conjunction to form the monolithic transition relation T -T^-T^ •... • .
3 Searching Reachable States of FSM
First, let us show how we search reachable states of a FSM. Let denote a set of states
reachable in at most i steps, ii'o represents a set of initial states. In our case we have = [s-g}. A set of states reachable in at most one step is given by
S A 5 e ^Sg A (^(.v, a) = .v']} (4)
= u {s' 13a3s
a e
After finding states reachable in at most one step we search for those reachable in at most two steps. In general, a set of states reachable in at most i steps is represented by
= ^ {s' I	G Z A g A S{S, a) = .y'
(5)
We continue with this procedure until in a step k no new state is reached. In any case, this happens sooner or later, because we deal with FSMs, where the set of states ^^ is finite. Then, S\ = is a set of all reachable states.
introducing the characteristic functions for the sets (e.g., the is represented by its characteristic
function Sj = Xs,")'	rewrite (5) into the fol-
lowing logical expression:
= ^M + 3 fe-. • T)
yiil/uX
(6)
The function S, depends on next state variables / / yj . To obtain S^ we have to replace each yj with
the corresponding yj. Therewith, next states are considered to be new present states for the next step. The procedure terminates in a step k , when
The most time and space consuming operation in (6) is the computation of	• f). The
source of problems is usually very large monolithic transition relation T . In order to avoid this problem, we do not build a single BDD for the whole transition
relation T , but rather partition T in some groups of transition relations of individual state variables and represent each group by a smaller BDD. T is then called a partitioned transition relation [3][9][5].
Formula (6) can be written in an extended form
as
=	+3xo3x,
(7)
Although existential quantification does not distribute over conjunction, conjuncts can be moved out of the scope of an existential quantification if they do not depend on any of the variables being quantified. FSMs that represent circuit behaviour exhibit locality,
so it is very common that many of the Tj depend on only small number of the input and state variables.
We developed a heuristic algorithm for the partitioning and reordering of functions and variables for existential quantification in (7) that allows us to apply some existential quantifiers before the BDD for the whole transition relation has been built. The function in (7) represents a set of present states in step / - 1. Therefore, it may depend on all state variables y,. So we leave it within the scope of ad existential
quantifiers of state variables yj . In contrast to the
function , functions Tj are constant throughout
the computation and at the beginning we can determine their place with respect to the existential quantifiers in (7) once and for all.
The dependencies of functions Tj on individual input and state variables are represented by matrix
A =
a
0,0
a
O.n-l
a
a
a
n,0
/1-1,«-1
a
'n+m-1,0	
t	.. T
To ■	

yo
yn^i
^m-l
which is of size {m +n)xn and a, ^ has value 1 if and only if the function Tj depends on the variable that points to row / from the right side, and value 0 otherwise. First, we fill the matrix with Os and 1 s. Then we choose one of the rows (there might be several) with minimal number of Is and thus one of the variables that the least number of the
functions depend on. We put into the scope of its existential quantifier all the functions that depend on this variable. We will be no more concerned with these functions during the partitioning procedure. Therefore, the selected row and all the columns whose functions were taken are no more needed and we delete them. The whole procedure is then repeated over the reduced matrix as long as we do not run out of functions and variables.
A group of functions which find themselves together in one step of this procedure is called a blocl<.
We denote it if we got it in the z-th step and p. represents the z'-th block of partition p over the set {0,1,1}. Accordingly, the block can be written as 7 = a T. . Let us denote a set of
Pi	J
variables whose existential quantifiers are immediately in front of block by , where
={v| vgIJVJX/X
Vy g /?, : 7,. depends on v a (8) Vy ^ /?, : T J does not depend on v)
Thus, using partitioned transition relation we got the following formula for a general step in computing reachable states:
= + 3
T ■
Pi-i —1

(9)

The algorithm based on (9) has proved itself very well. Just in few cases it was considerably worse (see the example of an up/down counter in Section 6) than the method with monolithic transition relation. However, in many cases it has been shown to be better for many orders of magnitude.
4 Symbolic Model Checking
The logic that we use to specify properties of FSMs is a prepositional termporal logic of branching time, called Computation Tree Logic — CTL [4]. In this logic each of the usual future time operators of linear temporal logic (G — globally or invariantly, F — sometimes in the future, X — next time, U — until) must be immediately preceded by path quantifier A (for all computation paths) or E (for some computational path). We thus obtain eight different CTL operators: AG, EG, AF, EF, AX , EX , AU,EU.
CTL formulas are constructed from atomic propositions using Boolean connectives and CTL opera-
tors. In our case of verifying FSMs, the set of atomic propositions is equal to the set Ž/ of state variables
of the circuit. If yj is an atomic proposition in y, the formula yj is true in a state s (we say that i' satisfies yj and write \=yj if and only if the state variable y^ is true in this state.
The formula AG / , for example, will hold in a state provided that / holds in all states along all possible computation paths starting from that state, and EF / will hold in a state provided that there is a computation path from that state to the future state where / holds [1][9]I5]. The meaning of all CTL operators is shown in Figure 1 in the fonri of computation trees. In the figure, full circle represents a state where formula / is true. In states that are represented by full square, formula g is true. We know
nothing about the truthfulness of formulas in all other states (empty circles).
a) EXf
b) AXf
C) EFf
d) AFf
e) EGf
1)AGf	g)E[fUg]	h)A[fUg]
Figure 1: Meaning of CTL operators
Model checking is the problem of detennining whether a given CTL formula / is true in a given FSM M . The formula / is true in the FSM M if and only if / is true in all initial states of M . We can say that FSM M is a model of / {M [=/),
In this section, we present an efficient symbolic model checking algorithm for CTL that recurses over the structure of a given CTL formula / and determines in a bottom up fashion in which states of the model the subfonnulas of / are true. Finally, it re-
turns the BDD (the function) S that represents exactly the set of states S of the FSM in which / is true and checks whether ^^ e .
The CTL formulas constructed only from the atomic propositions (state variables) and ordinary Boolean connectives are handled using standard algorithms for computing Boolean connectives with BDDs. The temporal formulas are treated otherwise. Although there are eight different CTL operators, it is sufficient to realize only three of them, since the remaining five can be easily expressed with the three realized. We decided to realize the operators EX , EU , and EG [7][1].
First, let us have a look at the formula EX f , where / represents a characteristic function Sf = / of the set of states Sf where it is true. Fonnula EX / is true in all predecessors of states in Sf. The characteristic function of these states is computed by
EX/= 3 (/'-r)
y'iy'yjX
(10)
where /' represents the function / with each state
variable y. substituted by the corresponding next t
state variable y. and T is a transition relation of a
given FSM. The relational product (10) is quite similar to the relational product (6) defined in Section 3 except that in (10) we compute one step in a backward reachability search instead of a fonward reachability search.
Formula E f g means that either g is true in the current state, or f is true in the current state and there exists a successor state where E g is true. Consequently, the B.DD that represents the states where E [/ U g] is true can be computed by finding the least fixed point of the predicate transformer F defined by
(11)
Formula EG / means that / is true in the current state and there exists a successor state where EG / is true. The BDD that represents the states
where EG / is true is computed as the greatest fixed point of the predicate transformer
F(6') = /-EX5'	(12)
After determining the set of states that satisfy a given CTL fonnula /, the algorithm checks
whether this set includes all initial states S^ (SqI^S). Checking the condition Sg Q S is
easy in our BDD-based algorithm. It has to be checked whether the Boolean expression
S is a tautology.
5 Fairness Constraints
Many times we want to check if a given property is true in a given FSM only along the fair paths in a computation tree. For example, at checking of a bus arbiter we might be interested only in those paths where none of the devices which the bus was granted to holds the bus to the eternity.''
Such properties can not be expressed directly by CTL. To solve the problem, the meaning of CTL should be changed. Therefore, we introduce fairness constraints, which are ordinary CTL formulas. A path in the computation tree is fair regarding to a set of fairness constraints if every constraint is true infinitely often along the path. Path quantifiers in CTL fomnulas are then constrained to these fair paths [8].
Let the set of CTL formulas JJ ^ be fairness constraints. Let us have a look at solving formula EG/ with fairness constraints JJ (we
write EG,.^,^ /). Formula / is again characteristic function of set of states where formula / is true, just like with ordinary CTL formulas. Formula EGf.i, / says that there exists a path in the computation tree, where / is invariantly true and every formula in JJ is true infinitely often. The set of such states ^ is the largest of the sets for which the following two properties are true:
. /is true in every state from S and
• for every fairness constraint hf, & J4 and
every state s e S, there exists a path of length one or more from state s to some state in S, where constraint h^. is true and / is true in every state along that path.
It could be proved that every state in the set S is the beginning of an infinite path in the computation tree, where fonnula / is always true and every
constraint in J4 is true infinitely often. By searching for the greatest fixed point of the predicate transformer

(13)
' This example shows us, where the name of fair paths comes from. It would be unfair from a device if it held the bus to the eternity and had never released the bus and left it to other devices, By excluding such paths in some way we stay only at fair paths.
k=\
where CTL operators EX and EU are resolved as ordinary CTL operators without considering the fairness constraints, we get a characteristic function of the set of states where formula EGf^,^ / is true
considering the fairness constraints. The fixed point is evaluated in the same manner as without fairness constraints, but note that each computation of the above expression leads to several nested fixed point computations (resolving of operators EU).
Resolving of operators EX and EU with fairness constraints is simpler. Characteristic function of the set of states that can be starting states of fair paths in the computation tree is defined as
^fa. =	1
(14)
There exists a path from every state in this set along which every fairness constraint in J4 is true infinitely often. Fonnula EXf^j^ / is true in state 5 if
and only if there exists a successor state s' of such that / is true in s' and s' is the beginning of
a fair path. Therefore, the formula EXj.^.^ / considering only fair paths is equal to the formula EX {f • ) over all paths. Thus, let us define

(15)
This way we transform the problem from dealing with fair paths to considering all paths in the computation tree, and that is something what we already know how to handle with.
Following analogy the fonnula E[/Ug
fair
is
equal to the fonnula E [/ U g • considering all computation paths. Therefore, we define
El/Udfa. ^El/Ug.^'.J (16)
and once again the problem is transfomned into something we already know how to solve,
5.1 Example
To illustrate symbolic CTL model checking using fairness constraints we took a parametric bus arbiter with n devices {n is parameter) which grants a bus to the device with the highest priority [11], An instance of such an arbiter for « = 3 is shown in Figure 2. All others are constructed in a similar way. Devices with lower number have higher priority.
We want to know if formulas
efeg(/a^,, -Wf)
(17)
REQo
REQi
REQ2
OUTo
—0-
r
GRo
INQ Ct		INi --—TT		IN2 \J
OUTi
-i=
GRi
OUT2
—O-


GR2
Figure 2: A 3-request bus arbiter
are true, in other words, if there exists a path from the initial state, where at some point device 7 (/=	-1) would request a bus and bus
would never be granted to it. in general case without any fairness constraints the formulas are true, because every other device could hold the bus for itself and never release it again.
Because such behaviour could be described as unfair, we will try to constrain all possible paths to those where the bus is free infinitely often along the path. This is written by fairness constraint

(18)
in the formal language. It could be shown that formula EFEg(/A^o •'^f^^o) is not true any more. If
the device 0 requests a bus and it insists on that request, the bus will be eventually granted to it. All other formulas are still true, because every other device might request the bus, but the bus would never be granted to it. Actually, this is the expected behaviour, since fairness constraint (18) has eliminated only those paths where some device would hold the bus to the eternity. Because nothing stops a device to request a bus again immediately after device has released it, there is a possibility that the bus is always granted to device 0 as device with the highest priority. In that case the bus will never be granted to any other device.
The next level of fairness is achieved by preventing the device 0 such aggressive behaviour in spite of its highest priority. It should be required that infinitely often, after the bus is released, it is not granted to device 0. That is, infinitely often along the path we must reach a state where the bus is released (fairness constraint (18) is true) and in all possible successor states the bus is not granted to
device 0. Therefore, formula AXOUT^ will be true
in that state, too. This leads us to new fairness constraint
OUT, + Om\ +... + 01JT„_^ ■ AX OUT, (19)
Beside the formula for device 0, now also formula EFEg(/7/, -out) for device 1 is false. Since
devices 0 and 1 can interchange in possessing the bus, all other devices can stay without the bus forever. So, other formulas are still true.
To prevent interchanging of the bus holding between two most prioritised devices, the fairness constraint should be extended. Infinitely many times it should happen that after the bus was released it is neither granted to the device 0 nor to the device 1. So, we get fairness constraint
OUT, + OUT, +... + OUT„^, ■ AX OUT, + OUT,
(20)
Now device 2 also gets its time slots where the bus is granted to it, Its CTL formula is now also false, but all others for / > 2 are still true.
In the same manner we could proceed, what leads us to fairness constraint
OUT +OUT +... + OUT
n-\
AX OUT
-OUT, +... + OUT,
(21) forO <k <n
where all CTL formulas from (17) with index / <k are false, while all others are true.'
If a device /, / = 0,1,..., A: , requests the bus and it insists on that request, the bus will eventually be granted to it. All other devices could stay without the bus to the eternity.
Well, if « -1 is chosen for k, we get as fair system as a priority system could be. Not only that none of the devices may hold the bus forever, but also the bus will be granted to each and every device from time to time.
6 Experimental results
Experiments were done on a Sun Ultra 30 creator workstation with 300 MHz UltraSPARC II processor, 256 MB of physical memory and 793 MB of virtual memory under Solaris 2.5.1 operating system. We have used our own BDD package ([6]) that is an efficient ;fe-based implementation of reduced ordered binary decision diagrams with complemented edges.
If A: = 0 , formula (21) becomes formula (18).
Table 1: Computing reachable states for IS-CAS'89 circuits and a parametric up/down counter
			nrionolittiic TR		partitioned TR	
circuit	# states	# steps	# nodes	time	# nodes	time
s344	2625	7	11966	0.13	19462	0.19
5349	2625	7	11966	0,14	19462	0.20
s382	8865	151	48580	1.98	46411	0.86
s420,1	65536	65535	278572	7.67	282476	35.86
s444	8865	151	13660	0.14	20863	0.22
s525	8868	151	19610	0.18	36560	0.36
s526n	8868	151	19508	0.18	38558	0.36
s541	1544	7	1299567	170.27	23649	0,36
s713	1544	7	1299622	173.09	23673	0.37
s953	504	11	37187	0.32	11967	0,16
S1186	2616	3	236067	29.87	28788	0,42
si 238	2616	3	236086	29.86	28810	0,40
counts	8	4	66	0.00	56	0.00
counts	64	32	598	0.00	1005	0.00
count9	512	256	3922	0.04	11111	0,11
count12	4096	2048	28558	0.42	44905	1,31
countIS	32768	16384	85708	4.32	88920	13,91
countIS	262144	131072	427938	36.78	433475	141,48
count21	2097152	1048576	3180807	414.54	3185888	1773,71
Table 1 shows the results obtained by symbolic searching of reachable states on some ISCAS'89 circuits and on the parametric up/down counters. From left to right the columns in Table 1 refer to the circuit name, the number of reachable states, the number of steps needed to compute all reachable states, and the maximal number of BDD nodes whenever generated during the symbolic state space traversal of a given circuit together witb the CPU time in seconds both for the search using monolithic transition relation and partitioned transition relation.
Great power of the symbolic state space traversal is demonstrated in the next example. Table 2 shows results on computing reachable states for the previously described parametric arbiter using partitioned transition relation. Although the number of reachable states grows with n extremely fast, the number of BDD nodes and CPU time grow much slower.
Table 2: Computing reachable states for a parametric arbiter
# dev.	# state	# reachable	#	# BDD	time
n	variab.	states	steps	nodes	hi
100	200	1.28032710 -10"	3	66443	2.39
200	400	3.22994546 -10"	3	203180	13.52
300	600	6.13147828 -10®^	3	454743	37.60
400	800	1.03548220 'lO"'	3	806369	80.66
500	1000	1.63996869 -10'"	3	1257932	148.41
600	1200	2.49385885 -lO'"	3	1809558	246.24
700	1400	3.68735526 -lO'"	3	2461121	386.41
800	1600	5.34107956 '10^"	3	3212747	570.30
900	1800	7.61589396 lO'"	3	4064373	809.61
1000	2000	1.07258011 -10™	3	5015936	1100.22
We verified the behavior of the parametric arbiter with symbolic model checking in CTL. The properties being verified together with the corresponding CTL formulas are as follows:
• Exclusivity. At most one output is set to '1'. In order to decrease the complexity of the CTL formula we weaken the exclusivity and rather write (as in [11]) that either odd number of outputs is set to '1' or all outputs are set to '0'.
AG {{OUT, e 0U7\ ®... © ) +
Causality. If device i (/= 0,1,...,« - 1) requests the bus, the access will eventually be granted to device /.
Starvation. There is a possibility that a request from device i is never serviced. This behavior will happen if another device being granted the bus never releases its request.

Allocation. If a request from device i {i ~~ 0,l,...,n - I) is loaded and no higher priority device requests the bus, then the bus is granted to device / at the next state.
AG{pUT,-...-OUT„_,-IN,
AX OUZ

■AKOUT
AG {pUf, •... ■ -IN,-...- ■ IN„_, =i> AX
In Table 3 we collected the results obtained from the verification of the parametric bus arbiter.^ The columns from left to right represent the number of devices (»). the number of state variables (latches) of the circuit («), the number of CTL formulas being verified for each n (3/7 + 1), and the maximal number of BDD nodes whenever generated during symbolic model checking of a given circuit together with the CPU time in seconds both for the model checking using monolithic transition relation and partitioned transition relation. An overflow on BDD nodes is denoted by a dash '—'.
We did not perform a lot of experiments with fairness constraints. Well, checking of CTL fomiulas (17) for /7 = 4 with fairness constraint (21) for k = 3 took less than of a second.
7 Conclusions
We reviewed two different algorithms for searching of reachable states in FSMs, using either monolithic transition relation or partitioned transition relation. The introduction of partitioned transition relation may decrease the CPU times for large circuits dra-
^ Although an arbiter with n = I is a totally senseless circuit, it is Included in Table 3 for the sake of completeness. Anyway, a model checking algorithm does not care whether it handles useful or senseless circuits.
Table 3: Checking of parametric arbiter in CTL
	#	#	monolithic TR J		1 partitioned TR	
dev.	state	CTL	#BDD	time	#BDD	time
n	var.	form.	nodes	Is1	nodes	M
1	2	4	18	0.00	11	0.00
2	4	7	174	0.00	76	0.00
3	6	10	947	0.01	298	0.01
4	8	13	4403	0.10	929	0,01
5	10	16	19171	0.64	2299	0,01
6	12	19	78044	4.63	7540	0.11
7	14	22	297614	38.37	15095	0.23
8	16	25	1214392	291.79	40247	0.98
S	18	28	4912359	2019.25	40301	1.77
10	20	31	—	—	100861	9.09
11	22	34	—	—	136629	15.55
12	24	37	—	—	616346	100.33
13	26	40	—	—	745319	184.85
14	28	43	—	—	3827900	1534.16
15	30	45	—	—	4303558	3603.01
maticaliy. Then, we showed methods for verifying synchronous sequential circuits by symbolic model checking [7][9]. Properties to be verified were expressed in CTL.
We illustrated the usage of fairness constraints by verifying a parametric bus arbiter which selects the highest priority device from n devices. We checked if it is possible that some device requests a bus and the bus is never granted to it regarding different fairness constraints.
All algorithms are realized as part of a homemade package for manipulating FSMs which is also based on a fully home-made very efficient package for manipulating Boolean functions represented by BDDs [10],
Our future work will consist in the implementation of searching for counterexamples for false properties and then of automatic generation of testing sequences for digital circuits based on found counterexamples.
8 References
/1/ Zmago Brezočnik, Aleš Časar, and Tatjana Kapus. Efficient Symbolic Traversal Algorithms using Partitioned Transition Relations, in Zmago Brezočnik and Tatjana Kapus, editors, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, pages 146-155, Maribor, Slovenia, June 1996.
/2/ Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35{8):677-691, August 1986.
/3/ Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, and David L. Dill. Symbolic Model Checking for Sequential Circuit Verification, IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems, 13(4):401-424, April 1994.
/4/ E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.
/5/ Aleš Časar. Verification of Finite State Machines with Symbolic Model Checking. Master's thesis. University of Maribor, Faculty of Electrical Engineering and Computer Science, Maribor, Slovenia, June 1998. in Slovene.
/6/ Aleš Časar and Zmago Brezočnik. Symbolic State Space Traversal of Finite State Automata. In Franc Solina and Baldomir Zajc, editors. Proceedings of the Fourth Electrotechnical and Computer Science Conference ERK'95, volume A, pages 85-88, Portorož, Slovenia, September 1995. In Slovene.
/7/ Aleš Časar, Zmago Brezočnik, and Tatjana Kapus, Exploiting Partitioned Transition Relations for Efficient Symbolic Model Checking in CTL, In Penny Storms, editor, Proceedings of the European Design & Test Conference ED&TC'96, pages 606-606, Paris, France, March 1996. IEEE Computer Society Press.
/8/ Aleš Časar, Zmago Brezočnik, and Tatjana Kapus. Fairness Constraints in Symbolic CTL Model Checking. In Baldomir Zajc and Franc Solina, editors. Proceedings of the seventh Electrotechnical and Computer Science Conference ERK'98, volume B, pages 39-42, Portorož, Slovenia, September 1998, In Slovene,
/9/ Aleš Časar, Zmago Brezočnik, and Tatjana Kapus, Symbolic Model Checking of Finite State Machines with CTL, In Baldomir Zajc and Franc Solina, editors. Proceedings of the fifth Electrotechnical and Computer Science Conference ERK'96, volume A, pages 51-54, Portorož, Slovenia. September 1996. In Slovene.
Aleš Časar, Robert Meolic, Zmago Brezočnik, and Bogomir Horvat. Representation of Boolean Functions with ROBDDs, Electrotechnical Review, 59(5):299-307, December 1992, In Slovene,
David Deharbe and Dominique Borrione. Symbolic Model Checking of VHDL Design Entities. Technical report, Atelier de Recherche sur les Techniques Mathematiques et Informatiques des Systemes, Grenoble, France, November 1993.
Aarti Gupta. Formal Hardware Verification Methods: A survey. Formal Methods in System Design, 1(2/3):151-238, October 1992,
/10/
/11/
/12/
mag. Aleš Časar, univ. dipl. inž. rač. izr. prof. dr Zmago Brezočnik, univ. dipl. inž. e/. izr. prof. dr. Tatjana Kapus, univ. dipl. inž. el.
Univerza v Mariboru Fakulteta za elektrotehniko, računalništvo
In informatiko Smetanova 17 2000 Maribor tel.: +386-2-22-07-211 fax: +386-2-25-11-178 email: (casar,brezočnik,kapus}@uni-mb.si
Prispelo (Arrived): 10.5.00
Sprejeto (Accepted): 30.8.00