Level Oriented Formal Model for Asynchronous Circuit Verification and
its Efficient Analysis Method
Tomoya Kitai, Yusuke Oguro
Tokyo Institute of Technology
f kitai, yoguro g @ yt. cs. titech. ac. jp
Tomohiro YonedaLevel Oriented Formal Model for Asynchronous Circuit Verification and
its Efficient Analysis Method
Tomoya Kitai, Yusuke Oguro
Tokyo Institute of Technology
f kitai, yoguro g @ yt. cs. titech. ac. jp
Tomohiro Yoneda
National Institute of Informatics
yoneda@ nii. ac. jp
Eric Mercer
Brigham Young University
egm@ cs. byu. edu
Chris Myers
University of Utah
myers@ vlsigroup. ece. utah. edu
Abstract
Using a level- oriented model for verification of asyn-chronous
circuits helps users to easily construct formal
models with high readability or to naturally model data-path
circuits. On the other hand, in order to use such a
model on large circuits, techniques to avoid the state ex-plosion
problem must be developed. This paper first intro-duces
a level- oriented formal model based on time Petri
nets, and then proposes its partial order reduction algo-rithm
that prunes unnecessary state generation while guar-anteeing
the correctness of the verification.
Key words Level- oriented model, timed asynchronous cir-cuits,
formal verification, time Petri nets.
1 Introduction
Many formal verification algorithms for asynchronous
circuits that are based on the exploration of reachable states
use transition- oriented models such as Petri nets and CSP
in order to model circuits and specifications [ 1, 2, 3, 4, 5].
In this approach, the behavior of an asynchronous circuit
is represented using transitions of signals. This represen-tation
has the potential ability to model the real nature of
asynchronous control circuits. It is, however, not easy for
nonexpert users to construct good and comprehensive rep-resentations
on this model. Furthermore, in asynchronous
circuit design, control signals are sometimes embedded in
data- path circuits. An example of this is a dual- rail encod-ing,
which requires some ( abstracted) data- path circuits to
be formally modeled for verification. In this type of appli-cation,
a transition- oriented model is not suitable.
This paper tries to represent the behavior of asyn-chronous
circuits also using values of signals like those used
This research is supported by NSF Japan Program award INT-
0087281, SRC contract 99- TJ- 694, a grant from Intel Corporation, and
JSPS Joint Research Projects.
in the synchronous circuit design process. For this purpose,
a level- oriented model is first introduced. Our model, which
we call L T N ( Level Time Petri Net), is obtained by extend-ing
time Petri nets such that firing an L T N transition can as-sign
values to a set of boolean variables and that the validity
of an expression over the boolean variables is also used as
an enabling condition of an L T N transition in addition to
the marking. Thus, an L T N can easily model the behavior
based on both changes of signals and values of signals.
On the other hand, an approach to analyzing this new
model in a traditional total order manner is not acceptable
for large circuits due to state explosion. In other words,
a new model is useless without an efficient analysis algo-rithm.
For transition- oriented models, two major methods
are proposed for this purpose, implicit state space enumer-ation
based on BDDs [ 3] and partial order reduction [ 4, 5].
Since our current interest is in verifying timed circuits with
bounded delays and the implicit state representation method
often fails to efficiently represent timed states ( in particular,
sets of inequalities), this work chooses the partial order re-duction
approach.
Timed automata [ 6] can also be used as a level oriented
model, and partial order reduction has been applied to their
analysis [ 7, 8]. Our experience, however, has found that
the generality of timed automata comes at an increase in
analysis complexity, and this increased generality does not
appear to be necessary for verifying asynchronous circuits.
Several alternative level- oriented Petri net models have
been proposed such as TEL structures [ 9], level- ruled Petri
nets ( LPNs) [ 10], and an extension of time Petri nets [ 11].
An L T N is obtained by refining the one proposed in [ 11].
An L T N is somewhat less expressive than TEL structures
and LPNs. In particular, timing annotations and Boolean
conditions are placed on the transition in an L T N while they
are placed on the edge between the place and transition in
TEL structures and LPNs. This increased expressiveness,
however, comes at a cost in the analysis algorithm’s com-plexity.
As a result, the algorithms for analysis of these nets
have tended to be conservative rather than exact [ 9, 10].
To the best of our knowledge, the work in [ 10, 12] is the
1
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
only one that proposes a partial order reduction for a level-oriented
Petri net model, namely the LPN model, though
the algorithm is conservative. The goal of this work is to
obtain the exact verification results using the L T N model.
This paper is organized as follows. The next section
introduces the L T N model. Section 3 briefly reviews the
verification method used in this paper. Section 4 proposes
the partial order reduction algorithm for an L T N . Section 5
shows the experimental results obtained by verifying sev-eral
examples with the proposed algorithm. Finally, we
summarize our results in Section 6.
2Le vel Oriented Model
A traditional time Petri net consists of transitions ( thick
bars), places ( circles), and arcs between transitions and
places. A token ( large dot) can occupy a place, and when
every source place of a transition is occupied, the transition
becomes enabled. Each transition has two times, the earli-est
firing time and the latest firing time. An enabled tran-sition
becomes ready to fire ( i. e., firable) when it has been
continuously enabled for its earliest firing time, and cannot
be continuously enabled for more than the latest firing time,
i. e., it must fire unless it is disabled. The firing of a transi-tion
occurs instantly. It consumes tokens in its source places
and produces tokens into its destination places.
In an L T N , two additional functions a s s i g n and c o n d i t i o n
can be associated with a transition. The a s s i g n function re-lates
a transition to assignments on Boolean variables, and
the c o n d i t i o n function relates a transition to an expression
over boolean variables. The enabling condition of an L T N
is extended, and a transition is enabled if both the expres-sion
given by c o n d i t i o n is true and every source place is
occupied. For example, in the L T N shown in Figure 1( a),
t c is enabled only if b 1 ^ b 2 is true. The firing rule of an
L T N is also extended in that when a transition fires, the as-signments
specified by the a s s i g n function are done while
consuming and producing tokens. For example, in an L T N
shown in Figure 1( b), when t a fires, a 1 and a 2 are set to
1 and 0 , respectively. Using a s s i g n and c o n d i t i o n , a level-oriented
model can easily be described.
t c [ 2 ; 4 ]
( b 1 ^ b 2 )
t a [ 3 ; 5 ]
f a 1 = 1 ; a 2 = 0 g
( a) ( b)
Figure 1. An example of an L T N
2.1 Formal Definitions of L T N
An L T N N is a ten- tuple, N = ( P ; T ; F ; E f t ; L f t ; V ;
a s s i g n ; c o n d i t i o n ; 0 ; v a l 0 ) . The members P , T , F , E f t ,
L f t , and 0 are the same as those of the time Petri net;
although the members V , a s s i g n , c o n d i t i o n , and v a l 0 are
newly added for an L T N , and defined as follows:
V is a finite set of Boolean variables.
a s s i g n : T ! 2 A , where A = f v = b j v 2 V ; b 2 f 0 ;
1 g g .
c o n d i t i o n : T ! C , where C = f f 1 _ f 2 j f 1 ; f 2 2
C [ F g and F = f g 1 ^ g 2 j g 1 ; g 2 2 F [ V [ V g . V
denotes f v 0 ; v 1 ; v 2 ; : : : g if V = f v 0 ; v 1 ; v 2 ; : : : g .
v a l 0 : V ! f 0 ; 1 g is for the initial values of Boolean
variables.
The a s s i g n function relates a transition to assignments on
Boolean variables performed on the firing of the transition.
For example, a s s i g n ( t ) = f a = 1 ; b = 0 g . The c o n d i t i o n
function specifies a Boolean expression that should be true
for the transition to be enabled. This expression is repre-sented
by a sum- of- products such as,
c o n d i t i o n ( t ) = a b c _ d e ;
where a ; b ; c ; d ; e are Boolean variables ( ^ are omitted
here).
A state of an L T N is a tuple ( ; I ; v a l ) , where is a
marking, I is a set of inequalities, and v a l is an assignment
of a value to each Boolean variable. For a transition t , two
kinds of timing variables, a past variable and a future vari-able
are used. A past variable represents its most recent fir-ing
time, and a future variable represents its next firing time.
This paper uses t also for the past variable, and t for the fu-ture
variable. Inequalities in I are over these variables. For
a Boolean expression f and an assignment v a l , e v a l ( f ; v a l )
denotes the value of f under v a l . Thus, a set of enabled
transition in a state s = ( ; I ; v a l ) can be expressed as
e n a b l e d ( ; v a l ) =
f t j t ; e v a l ( c o n d i t i o n ( t ) ; v a l ) = 1 g ;
where t denotes the set of source places of t . A transition
is firable, if it is enabled and possible to fire earlier than any
other enabled transitions. That is,
r a b l e ( s ) =
f t j ( I [ f t t 0 j t 0 2 e n a b l e d ( ; v a l ) g ) is consistent g :
In this work, only 1- safe L T N s are considered, i. e., in
any reachable state s = ( ; I ; v a l ) , no transition t such that
( ?? t ) \ t = 6 ; is firable. Similarly, it is assumed that no
transition has vacuous assignment, i. e., for any variable v ,
and in any reachable state s = ( ; I ; v a l ) with v a l ( v ) = b ,
no transition t such that \ v = b 0 0 2 a s s i g n ( t ) is firable.
These assumptions are just for simplification of our algo-rithm,
and with an increase in complexity they can be re-moved.
Figure 2( a) shows a NOR gate model with a hazard de-tection
mechanism represented by a time Petri net. The
2
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
marking shown in this figure represents the state with input
a = 0 ; b = 0 and output c = 1 . If a or b goes high, c ?? is en-abled.
However, after a goes high, a ?? is not enabled until c
goes low. Therefore, a hazard caused by a + and a ?? before
c ?? is detected as a failure ( as described in the next section).
Figure 2( b) shows the corresponding NOR gate model by a
L T N . In this model, the enabling conditions are straightfor-wardly
represented by c o n d i t i o n functions. When a hazard
occurs, a dummy transition e r r + is enabled, and it immedi-ately
fires resulting in a failure, because the corresponding
input transition is always disabled. It can be seen that an
L T N represents a model more concisely than a time Petri
net.
NOR gate
c-a+
a-b+
b-a-b-a+
b+
b-a-b+
a+
[ 0,0]
[ 0,0]
[ 0,0]
a
b
c
( 0)
( 0)
( 1)
( a _ b ) f c = 0 g
f c = 1 g ( a ^ b ) e r r +
( a ^ b )
( a _ b )
[ 1,2]
c+
[ 1,2]
[ 0,0] [ 1,2]
[ 0,0]
[ 0,0]
[ 0,0]
[ 1,2] [ 0,0]
( a)
( b)
Figure 2. NOR gate models expressed by a
time Petri net and an L T N .
3 Verification Method
This paper uses the timed trace theoretic verification
method [ 13]. A module is a tuple ( I ; O ; N ) , where I and
O are sets of input and output wires respectively, and N is
an L T N . We use a module as a formal model for a circuit
element ( e. g., a gate) and a specification. Some transitions
in N correspond to wires, and the firing of those transitions
change the values of the wires. A transition related to an in-put
wire of the module is called an input transition. An out-put
transition is defined similarly. Moreover, the Boolean
variables of an L T N correspond to input or output wires. A
circuit consists of a set of modules. In a set of modules,
input transitions fire only in synchronization with the cor-responding
output transition with the same wire name in
some different module. When an output transition fires, if
no input transitions are enabled in a module, a failure oc-curs.
This represents that a module tries to send an output
but some other module cannot receive it as a corresponding
input. Thus, it is the case that some bad output can be pro-duced.
In this sense, our verification method checks safety
properties. Note that Boolean variables can be changed at
any time without failures.
We define the following, where s = ( ; I ; v a l ) :
o u t t r a n s ( t ) is the output transition that corresponds
to t . If t is an output transition, then o u t t r a n s ( t ) is t
itself.
i n t r a n s ( t ) is a set of input transitions that correspond
to o u t t r a n s ( t ) .
s y n c t r a n s ( s ; t ) = f o u t t r a n s ( t ) g [
?? i n t r a n s ( t ) \ e n a b l e d ( ; v a l ) .
4 Verification Algorithm
The following shows a skeleton of the verification algo-rithm
based on the partial order reduction.
1 : v e r i f y ( s )
2 : begin
3 : if ( s is already visited) then return( true);
4 : if ( s is a failure state) then return( false);
5 : Mark s as visited;
6 : forall ( t f 2 r e a d y ( s ) );
7 : forall ( s 0 2 s u c c e s s o r ( s ; t f ) );
8 : if ( v e r i f y ( s 0 ) is false) then return( false);
9 : return( true);
10 : end
Although this algorithm is quite similar to the usual
depth- first search algorithm, there are some major differ-ences
that characterize the partial order reduction. One is
that r e a d y ( t ) is the subset of firable transitions, and the
other is that multiple states are generated at the firing of
t f by s u c c e s s o r ( s ; t f ) . We show how to construct r e a d y ( s )
and s u c c e s s o r ( s ; t f ) for an L T N in the next subsections.
4.1 r e a d y ( s )
r e a d y ( s ) is the set of output transitions firable and nec-essary
to fire in s in order to determine if a circuit is cor-rect.
For a firable output transition t and a state s , if
d e p e n d e n t ( s ; t ) denotes the set of output transitions ( in-cluding
t ) such that the interleaving of the firings of those
transitions should be considered, r e a d y ( s ) is defined as
r e a d y ( s ) = m i n s e t ( m ) if m > 0
r a b l e ( s ) otherwise
where
f m g = f d e p e n d e n t ( s ; t ) j
t 2 r a b l e ( s ) ; d e p e n d e n t ( s ; t ) r a b l e ( s ) g :
3
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
m i n s e t ( ) chooses the set with smallest cardinality
from . Since d e p e n d e n t ( s ; t ) may include tran-sitions
which are not firable, those dependent sets are not
chosen.
d e p e n d e n t ( s ; t f ) is the smallest set which satisfies the
following:
1. t f 2 d e p e n d e n t ( s ; t f ) .
2. If t 2 d e p e n d e n t ( s ; t f ) , then
( a) 8 t x 2 S t 0 2 s y n c t r a n s ( s ; t ) c o n
i c t ( t 0 ) : [
a c t i v e ( s ; t ; n e c e s s a r y ( s ; t x ; f t g ) )
d e p e n d e n t ( s ; t f ) ] .
( b) 8 t x 2 S t 0 2 s y n c t r a n s ( s ; t ) h i d e f a i l ( t 0 ) : [
a c t i v e ( s ; t ; n e c e s s a r y ( s ; t x ; f t g ) )
d e p e n d e n t ( s ; t f ) ] .
( c) 8 t x 2 S t 0 2 s y n c t r a n s ( s ; t ) a c c o n f ( s ; t 0 ) : [
a c t i v e ( s ; t ; n e c e s s a r y ( s ; t x ; f t g ) )
d e p e n d e n t ( s ; t f ) ] .
( d) 8 t x 2 f t 0 j
t 0 2 s y n c t r a n s ( s ; t ) ; c o n d i t i o n ( t 0 ) 6 = ; g : [
a c t i v e ( s ; t ; a c n e c e s s a r y ( s ; c o n d i t i o n ( t x ) ; 0 ; f t g ) )
d e p e n d e n t ( s ; t f ) ] .
( e) 8 t x 2 S t 0 2 s y n c t r a n s ( s ; t ) a e c t e d ( t 0 ) : [
a c t i v e ( s ; t ; a c d e p e n d e n t ( s ; c o n d i t i o n ( t x ) ; t ) )
d e p e n d e n t ( s ; t f ) ] .
As mentioned later, n e c e s s a r y , a c n e c e s s a r y and
a c d e p e n d e n t contain sets of pairs ( u ; ) , where u is a tran-sition
and is the minimal time necessary to fire u . Thus,
if is large enough, the algorithm does not have to con-sider
the firing order of t f and u because u is enabled too
late. Those transitions which fire too late are omitted from
the sets by a c t i v e . In other words, a c t i v e ( s ; t ; T T ) repre-sents
a set of transitions u such that ( u ; ) 2 T T and u can
fire time units earlier than t . Therefore, d e p e n d e n t ( s ; t f )
includes only those active transitions.
Now, we explain each of the above conditions using ex-amples.
Conditions 2.( a) and 2.( b) are the same as those for
the transition- oriented model, so we omit them here. The
details can be found in [ 14]. Condition 2.( c) states that the
firing order of t and t x should be considered, if t is in the
dependent set and t makes the condition of t x false. In this
condition,
a c c o n f ( s ; t ) = f t c j e v a l ( c o n d i t i o n ( t c ) ; v a l ) = 1 ;
e v a l ( c o n d i t i o n ( t c ) ; n e w v a l ( s ; t ) ) = 0 g ;
where n e w v a l ( s ; t ) represents the assignment of variables
after t fires. Consider the case shown in Figure 3( a). If t
and t 1 are fired only in this order and the initial value of a
is 0, the firing of t 2 is missed. However, t 2 can actually fire,
if t 1 and t x fire earlier than t . If the firing of t 2 causes a
failure, omitting Condition 2.( c) implies that the algorithm
misses a failure that may actually occur. Thus, if t is in
the dependent set, the algorithm must obtain t 1 by using
n e c e s s a r y ( s ; t x ; f t g ) so that the chance that t x fires earlier
than t is covered.
n e c e s s a r y ( s ; t ; T D ) contains the set of pairs ( u ; ) ,
where u is an output transition enabled in s which must fire
in order to fire t under the condition that transitions in T D
are not fired, and is the minimal time difference between
the firings of u and t . n e c e s s a r y ( s ; t ; T D ) is defined as fol-lows.
Note that t o u t = o u t t r a n s ( t ) , because if t is an in-put
transition, its corresponding output transition should be
considered.
1. If t o u t 2 T D , then n e c e s s a r y ( s ; t ; T D ) = ; .
2. If t o u t 2 e n a b l e d ( ; v a l ) , then
n e c e s s a r y ( s ; t ; T D ) = f ( t o u t ; 0 ) g .
3. Otherwise,
n e c e s s a r y ( s ; I ; v a l ) , of which
firing is necessary to let the expression f take value
b . a c n e c e s s a r y ( s ; f ; b ; T D ) is defined as follows, where
a s s i g n t r a n s ( v ; b ) = f t j “ v = b ” 2 a s s i g n ( t ) g :
1. If b = e v a l ( f ; v a l ) , then a c n e c e s s a r y ( s ; f ; b ; T D ) =
; .
2. If f is a positive form of variable v , then
a c n e c e s s a r y ( s ; f ; b ; T D ) =
S t 0 2 a s s i g n t r a n s ( v ; b ) n e c e s s a r y ( s ; t 0 ; T D ) .
3. If f is the negative form of variable v , then
a c n e c e s s a r y ( s ; f ; b ; T D ) =
S t 0 2 a s s i g n t r a n s ( v ; b ) n e c e s s a r y ( s ; t 0 ; T D ) .
On the other hand, for a transition t in the dependent set,
Condition 2.( d) of d e p e n d e n t ( s ; t f ) checks the fireability of
transitions that make the condition of t false. For example,
4
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
t [ 2 ; 3 ] t x [ 1 ; 2 ]
( a )
t 1 [ 0 ; 5 ]
t 2 [ 1 ; 3 ]
( a )
f a = 1 g
t ( o u t )
[ 0,5]
t ( i n )
[ 0,5]
( a )
t 1 [ 2 ; 3 ]
f a = 0 g
( a) ( b)
Figure 3. Examples of 2.( c) and ( d)
t 1 t 2 t 3
[ 0,15] [ 6,10] [ 8,14]
t [ 1 ; 2 ]
( a)
t [ 0 ; 0 ] t a [ 1 ; 1 ] t b [ 1 ; 1 ]
( b)
t c [ 1 ; 1 ]
( a b c ) f a = 1 g f b = 1 g f c = 1 g
t a [ 1 : 2 ]
f a = 1 g
t b [ 1 ; 2 ]
f b = 1 g
t c [ 0 ; 0 ]
( a _ b )
( c)
Figure 4. Examples for handling true parents
in Figure 3( b), if the output transition t ( out) fires, the corre-sponding
input transition t ( in) also fires synchronously, and
no failure occurs. However, if t 1 fires earlier than t ( in), then
t ( in) is disabled, and a failure occurs when t ( out) fires. If
t ( out) is always fired earlier than t 1 , this failure is missed.
Thus, we need Condition 2.( d) in order to fire transitions
which make conditions of other transitions false. This is
done by a c n e c e s s a r y .
Conditions 2.( e) is for making it easier to decide true
parents of newly enabled transitions. A true parent of an
enabled transition t is a transition that actually makes t en-abled
and hence decides its firing time. For example, since
t has multiple source places in Figure 4( a), the transition
that produces the final token to the source places of t can
be a true parent. Moreover, if c o n d i t i o n ( t ) is a simple prod-uct
as shown in Figure 4( b), the transition that assigned true
to a Boolean variable last can be a true parent. Note that
even if t 3 fires last in a firing sequence that enables t in Fig-ure
4( a), it does not mean that only t 3 is a true parent of t in
that firing sequence. This is because the partial order reduc-tion
algorithm does not usually give the ordering relation
among concurrent transitions such as t 1 , t 2 , and t 3 . Thus,
when t becomes enabled, the possibilities that each of t 1 , t 2
and t 3 is a true parent of t is checked, and a new state is gen-erated
by giving timing constraints for such a transition to
be a true parent. However, if c o n d i t i o n ( t ) contains logical
OR operators, true parents should be decided in a different
way. For example, in Figure 4( c), either a transition t a or
t b that fires earlier than the other can be a true parent of
t c , and the firing of such a transition immediately makes t
enabled. Therefore, the decision of true parents cannot be
postponed until all candidates of true parents fire. Hence,
in the case where c o n d i t i o n ( t c ) is a sum of product terms,
when one of the product terms becomes true by firing t , we
check whether other product terms of c o n d i t i o n ( t c ) can be
true by firing transitions t 0 , and give the ordering relation
between t and t 0 . This implies that all of possible true par-ent
candidates of t c are explicitly ordered, and it allows us
to decide true parents of this type according to the firing
sequences.
In Condition 2.( e),
v a r ( f ) = f v j v is a variable included in f g :
By using a c d e p e n d e n t ( s ; f ; t ) , which is defined below,
Condition 2.( e) checks the fireability of the transitions that
makes the other products true.
5
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
a c d e p e n d e n t ( s ; f ; t ) =
S i = 1 ; n a c n e c e s s a r y ( s ; f i ; 1 ; f t g )
2. Otherwise,
a c d e p e n d e n t ( s ; f ; t ) = ; .
4.2 s u c c e s s o r ( s ; t f )
When we fire t f such that t f 2 r e a d y ( s ) in s = (I ;
v a l ) , the following processes are needed.
For each u 2 r e a d y ( s ) , the constraint t u is added
to I , where u is the future variable of u .
For a transition t n newly enabled by firing of t f , its
true parent is decided, and the appropriate constraints
for it are added to I .
We can consider two types of true parents for t n , the
transitions that produce tokens in source places of t n , and
the transitions that satisfy c o n d i t i o n ( t n ) . The former are
called place- related true parents, and the latter are called
condition- related true parents. In order to decide true par-ents
of t n , t r u e p a r e n t ( s ; t n ) , which is actually defined in
4.2.1, denotes a set of pairs ( t p ; I p ) , where t p is a true parent
of t n , and I p is a set of inequalities that are necessary for t p
to be a true parent. Note that if adding I p to I of the current
state makes I inconsistent, such ( t p ; I p ) is discarded during
the state generation process.
When a true parent t p of newly enabled transition t n is
decided, the following constraint
is added to I . In this case, if t p does not become a true
parent of any other transitions, t p can be removed from I
by d e l e t e ( I ; D ) . d e l e t e ( I ; D ) removes from I the inequal-ities
including variables in the set D without affecting the
solution set projected to the remaining variables. Since the
behavior of the transition t n can be represented by a future
variable t n , failures are not missed by removing t p . Further-more,
if t p is not removed, the state enumeration process
may not terminate.
On the other hand, for a transition t which is not en-abled
in s , it is possible that I contains the past variables
of transitions that can be true parents of t when it becomes
enabled, e. g., the transitions which produce tokens in the
source places of t . Such past variables must not be re-moved
in general. n e e d t o k e e p ( s ; t ) shown in 4.2.3 de-notes
the set of such transitions. Using this, the set of vari-ables
that can be removed is defined as T ?? f t j 9 t 0 2
T ?? e n a b l e d ( ; v a l ) : [ t 2 n e e d t o k e e p ( s ; t 0 ) ] g , where T is
the set of all output transitions.
In 7., since more than one true parent assignment,
( I ) denote a set of candidates
of place- related true parents for t n , and a set of the pairs of
place- related true parents and their necessary constraints is
denoted by
t r u e p a r e n t p l a c e ( s ; t n ) =
S t p 2 r u l e r ( t n ; I ) f ( t p ; I p ) j I p = f t 0
t r u e p a r e n t c o n d ( s ; f ) denotes a set of pairs ( t p ; I p ) ,
similarly. The definition of t r u e p a r e n t c o n d ( s ; f ) is given
in the next subsection.
¿ From these, for cases where a place- related true par-ent
becomes the actual true parent, t 0
p t p is necessary
for each ( t p ; I p ) 2 t r u e p a r e n t p l a c e ( s ; t n ) and ( t 0
p ; I 0
p ) 2
t r u e p a r e n t c o n d ( s ; c o n d i t i o n ( t n ) ) , and
T P 1 = f ( t p ; f t 0
p ) j
( t p ; I p ) 2 t r u e p a r e n t p l a c e ( s ; t n ) ;
( t 0
p ; I 0
p ) 2 t r u e p a r e n t c o n d ( s ; c o n d i t i o n ( t n ) ) g
is obtained. Similarly, for cases where a condition- related
true parent becomes the actual true parent, t p t 0
p is nec-essary,
and
T P 2 = f ( t 0
p ; f t p t 0
p g [ I p [ I 0
p ) j
( t p ; I p ) 2 t r u e p a r e n t p l a c e ( s ; t n ) ;
( t 0
p ; I 0
p ) 2 t r u e p a r e n t c o n d ( s ; c o n d i t i o n ( t n ) ) g
6
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
is obtained. Therefore, t r u e p a r e n t ( s ; t n ) can be defined as
follows:
1. If c o n d i t i o n ( t n ) = ; , only place- related true parents
exist, and hence
t r u e p a r e n t ( s ; t n ) = t r u e p a r e n t p l a c e ( s ; t n )
holds.
2. Otherwise, by considering both cases,
t r u e p a r e n t ( s ; t n ) = T P 1 [ T P 2
holds.
4.2.2 t r u e p a r e n t c o n d ( s ; f )
The candidates of true parent for the condition of the form
“ v = b ” is denoted by v r u l e r ( v ; b ; I ) = a s s i g n t r a n s ( v ; b ) \
v a r ( I ) . A set of pairs of the condition- related true parents
for f and their necessary constraints is obtained as follows:
1. If f is a positive form of variable v , then
t r u e p a r e n t c o n d ( s ; f ) =
f ( t p ; ; ) j t p 2 v r u l e r ( v ; 1 ; I ) g .
2. If f is the negative form of variable v , then
t r u e p a r e n t c o n d ( s ; f ) =
f ( t p ; ; ) j t p 2 v r u l e r ( v ; 0 ; I ) g .
3. If f is f 1 ^ f 2 , then
t r u e p a r e n t c o n d ( s ; f ) =
f ( t p ; f t 0
p g [ I p [ I 0
p ) j
( t p ; I p ) 2 T T 1 ; ( t 0
p ; I 0
p ) 2 T T 2 g ;
where T T 1 = t r u e p a r e n t c o n d ( s ; f 1 ) , and T T 2 =
t r u e p a r e n t c o n d ( s ; f 2 )
4. If f is f 1 _ f 2 , then
p ; I 0
p ) 2 T T 2 ; t 2 T 1 g ;
where T T 1 = t r u e p a r e n t c o n d ( s ; f 1 ) , T T 2 =
t r u e p a r e n t c o n d ( s ; f 2 ) , T 1 = f t p j ( t p ; I p ) 2 T T 1 g ,
and T 2 = f t 0
p j ( t 0
p ; I 0
p ) 2 T T 2 g .
Note that if f consists of more than two terms in ( 3) or ( 4),
t r u e p a r e n t c o n d ( s ; f ) is applied recursively.
Consider the example shown in Figure 5. Suppose that
the state s 1 is obtained by the firing sequence t a ; t b ; t c ; t 1 .
In this case, for f = a
holds.
t a [ 1 ; 2 ]
f a = 1 g
t b [ 1 ; 2 ]
f b = 1 g
t [ 0 ; 0 ]
( a _ b c )
t 1 [ 1 ; 5 ]
t c [ 1 ; 2 ]
f c = 1 g
Figure 5. Example of t r u e p a r e n t c o n d ( s ; f )
4.2.3 n e e d t o k e e p ( s ; t )
For a disabled transition t , n e e d t o k e e p ( s ; t ) is a set of
transitions that can be true parents of t . First, let
l a s t ( T p ; I ) = is consistent g
denote the set of transitions which can fire later than any
other transitions in T p .
There are two cases to consider: first, a place- related
true parent becomes the actual true parent; and second a
condition- related true parent becomes the actual true par-ent.
The set of place- related true parents is T P 1 =
l a s t ( r u l e r ( t ; I ) ; I ) , and the set of condition- related true
parents is T P 2 = n e e d c o n d ( s ; c o n d i t i o n ( t ) ) , where
n e e d c o n d ( s ; f ) is obtained as follows:
1. If f is the positive form of variable v , and
n e e d c o n d ( s ; f ) = S i = 1 ; n n e e d c o n d ( s ; f i )
The set of true parents can be obtained by applying l a s t
to the union of these two sets, that is, l a s t ( T P 1 [ T P 2 ; I ) .
However, in order to make t enabled, the firings of other
transitions t 0 are necessary, and if t p 2 l a s t ( T P 1 [ T P 2 ; I )
cannot fire later than those transitions, t p cannot be the ac-tual
true parent. c a n r e l a s t ( s ; t ; t p ; T D ) checks this pos-sibility.
Therefore, n e e d t o k e e p ( s ; t ) can be defined as follows
n e e d t o k e e p ( s ; t ) = f t p j t p 2 l a s t ( T P 1 [ T P 2 ; I ) ;
7
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
Table 1. Experimental results ( 1).
Total Partial
No. of stages 6 7 8 9 6 7 8 9
No. of states 9096 16376 24784 37728 270 324 334 402
CPU times ( sec) 13.8 26.7 48.3 84.0 0.05 0.08 0.04 0.09
Memory usage ( MB) 17.2 37.4 68.5 116 0.28 0.32 0.33 0.38
Table 2. Experimental results ( 2).
Proposed VINAS- P
No. of stages 15 16 17 18 15 16 17 18
No. of states 1205 3598 13765 19861 3348 19146 22382 27742
CPU times ( sec) 0.29 0.85 3.71 6.00 1.52 12.8 13.9 19.0
Memory usage ( MB) 1.24 3.27 12.0 18.8 1.82 10.9 12.8 16.9 checks all enabled transitions
t 0 0 , and returns true if it is possible that t p can fire later
than any other descendant transitions of t 0 0 that make t en-abled. ( s ; t ; t p ; T D ) considers all t 0 0 , while n e c e s s a r y
checks some selected paths using m i n s e t .
5 Experimental Results
We have naively implemented the proposed method in
the C language. Here, we demonstrate the verification of the
STARI example [ 15, 16, 14] by using L T N models. In these
experiments, the time Petri net models used in [ 14] are just
replaced with L T N models, e. g., a NOR gate is modeled as
shown in Figure 2( b) instead of Figure 2( a). The remaining
verification settings are not changed.
In Table 1, the column labeled “ Partial” shows the num-ber
of generated states, CPU times ( Pentium III, 866MHz,
360MB, on VMware), and memory amount required for the
verification of various sizes of STARI circuits. For compar-ison,
the results by the total order algorithm where the set of
all firable transitions is used as a ready set are also shown in
the column labeled “ Total”. The results show a significant
performance improvement of the partial order reduction al-gorithm
over the total order algorithm.
Table 2 shows the performance comparison between the
level- oriented method and the transition- oriented method.
For this experiment, VINAS- P[ 17], which works for time
Petri net models, is used as the transition- oriented method.
Both methods use a partial order reduction algorithm. Since
the L T N models are much simpler than the time Petri net
models as shown in Figure 2, our naive implementation out-performs
VINAS- P.
6 Conclusion
This paper proposes a level- oriented model, L T N , for
formal verification that naturally models the behavior of
asynchronous circuits. This new model allows for the speci-fication
of causality through both transitions and signal val-ues.
This paper also develops a partial order verification
algorithm for this new model. In particular, the ready set
construction is enhanced to be aware that disablings can
now occur not only as a result of conflict in the net but also
through the change of signal values in the level. The calcu-lation
of true parents in disjunctive conditions must also be
considered in the calculation of the ready set. Finally, the
necessary set construction used in the ready set calculation
must be updated to allow for the recursion to proceed from a
condition to the transition that assigns to the variables used
in the condition. The zone construction used by the tim-ing
analysis algorithm must also be enhanced. In particular,
true parents may now be found in conditions and more care
must be taken in deciding when transitions can be safely
pruned from the zone. This updated algorithm has been im-plemented
and applied to the the timed circuit benchmark,
STARI, and it has been found to outperform a verifier based
on the time Petri net model.
References
[ 1] D. L. Dill. Trace Theory for Automatic Hierarchi-cal
Verification of Speed- Independent Circuits. MIT
press, 1988.
[ 2] J. Ebergen and R. Berks. VERDECT: A verifier
for Asynchronous Circuits. IEEE TCCA Newsletter,
1995.
[ 3] Oriol Roig, Jordi Cortadella, and Enric Pastor. Verifi-cation
of asynchronous circuits by BDD- based model
checking of Petri nets. LNCS 935 Application and
Theory of Petri Nets 1995, pages 374– 391, 1995.
[ 4] K. L. McMillan. Trace theoretic verification of asyn-chronous
circuits using unfoldings. LNCS 939 Com-puter
aided verification, pages 180– 195, 1995.
[ 5] T. Yoneda and T. Yoshikawa. Using partial orders
for trace theoretic verification of asynchronous cir-cuits.
Proc. of Second International Symposium on
8
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.
Advanced Research in Asynchronous Circuits and Sys-tems,
pages 152– 163, 1996.
[ 6] R. Alur and D. Dill. The Theory of Timed Automata.
LNCS 443 ( 17th ICALP), pages 322– 335, 1990.
[ 7] Johan Bengtsson, Bengt Jonsson, Johan Lilius, and
Wang Yi. Partial order reductions for timed systems.
Proc. of CONCUR98, pages 485– 500, 1998.
[ 8] Marius Minea. Partial order reduction for verification
of timed systems. PhD thesis, Carnegie Mellon Uni-versity,
1999.
[ 9] W. Belluomini, C. J. Myers, and H. P. Hofstee. Timed
Circuit Verification Using TEL Structures. IEEE
Transactions on Computer- Aided Design of Integrated
Circuits, 20( 1): 129– 146, January 2001.
[ 10] Eric G Mercer, Chris J. Myers, Tomohiro Yoneda, and
Hao Zheng. Modular Synthesis of Timed Circuits us-ing
Partial Orders on LPNs. Proc. of TPTS2002, 2002.
[ 11] Y. Oguro, O. Okano, and T. Yoneda. Verification of
asynchronous circuits including data- paths. IEICE
Technical Report ( in Japanese) FTS2000( 9), pages
65– 72, 2000.
[ 12] Eric G Mercer. Correctness and Reduction in Timed
Circuit Analysis. PhD thesis, University of Utah,
2002.
[ 13] B. Zhou, T. Yoneda, and C. Myers. Framework of
Timed Trace Theoretic Verification Revisited. Proc.
of 10th Asian Test Symposium, pages 437– 442, 2001.
[ 14] Tomohiro Yoneda and Hiroshi Ryu. Timed trace the-oretic
verification using partial order reduction. Proc.
of Fifth International Symposium on Advanced Re-search
in Asynchronous Circuits and Systems, pages
108– 121, 1999.
[ 15] S. Tasiran and R. Brayton. STARI: A case study
in compositional and hierarchical timing verification.
LNCS 1254 Computer Aided Verification, pages 191–
201, 1997.
[ 16] W. Belluomini and C. Myers. Verification of timed
systems using POSETs. LNCS 1427 Computer Aided
Verification, pages 403– 415, 1998.
[ 17] http:// yoneda- www. cs. titech. ac. jp/ ˜ yoneda/ pub. html.
9
Proceedings of the 2002 Pacific Rim International Symposium on Dependable Computing ( PRDC’ 02)
0- 7695- 1852- 4/ 02 $ 17.00 © 2002 IEEE
Authorized licensed use limited to: Brigham Young University. Downloaded on August 16,2010 at 17: 29: 19 UTC from IEEE Xplore. Restrictions apply.