TELKOM
NIKA
, Vol. 11, No. 2, Februa
ry 2013, pp. 740~746
ISSN: 2302-4
046
740
Re
cei
v
ed Se
ptem
ber 18, 2012; Revi
se
d De
ce
m
ber
28, 2012; Accepted Janu
ary 13, 201
3
On the Model Checking of the SpaceWire Link Interface
Wei Hu
a*
1,2
, Xiaojuan
Li1,
1,2
, Yong Guan
1,2
, Zhipin
g
Shi
1,2
, Jie
Zhang
1,2
, Lingling Dong
1,2
1
Beijin
g Eng
i
n
e
e
rin
g
Rese
arch
Center of Hig
h
Relia
bl
e Embe
dde
d S
y
stem
，
Coll
eg
e of Information
Engi
neer
in
g, Capita
l Norma
l Univers
i
t
y
, Be
ij
ing 1
0
0
048 C
h
i
n
a
2
Colle
ge of Info
rmation Sci
enc
e &
T
e
chnol
og
y, Beij
in
g Univ
ersit
y
of C
hemi
c
al T
e
chnolo
g
y, China
*Corres
p
o
ndi
n
g
author, e-ma
i
l
: begi
n_
dream
@12
6
.com, jzh
ang
@mai
l.buct
.
edu.cn
A
b
st
r
a
ct
In this
pap
er
w
e
disp
lay
a
p
r
actical
ap
pro
a
c
h a
dopt
ed for
the for
m
al v
e
rificatio
n
of S
p
aceW
ire
usin
g
mo
del
ch
eckin
g
to s
o
lve
state ex
plos
io
n. Spac
eW
ire i
s
a h
i
gh-s
p
e
e
d
,
full-du
pl
ex se
rial
bus sta
n
d
a
r
d
w
h
ich is
app
lie
d in
aer
osp
a
ce
, so its functio
n
s
have
very
hi
gh
a
ccu
ra
cy requ
i
r
em
en
ts. In
ord
e
r
to
p
r
o
v
e
the
desi
gn of the S
paceW
ir
e w
a
s faithfully
i
m
ple
m
e
n
ts the Spa
c
eW
ire protoc
o
l
’
s
spec
ificatio
n
,
w
e
present ou
r
exper
ienc
e on
the mo
de
l che
cking of Spac
e
W
ire link
interf
ace usi
ng the
Cad
ence SMV
tool. W
e
appli
e
d
envir
on
me
nt state
mach
in
e to over
c
o
me st
ate ex
plos
ion
and s
u
ccessfu
l
ly verifi
ed
a n
u
mber
of rel
e
v
ant
prop
erties a
b
o
u
t transmitter a
nd contro
ller
of
the SpaceW
ir
e in reas
on
abl
e CPU time.
Ke
y
w
ords
: Sp
aceW
ire, for
m
al ver
i
ficatio
n
,
mo
de
l check
i
n
g
, envir
on
ment
state mach
ine
,
CT
L, Cad
enc
e
SMV.
Copy
right
©
2013 Un
ive
r
sita
s Ah
mad
Dah
l
an
. All rig
h
t
s r
ese
rved
.
1. Introduc
tion
With the increasi
ng use of digital systems,
design errors will
ca
use serious
failures,
resulting in t
he lo
ss
of time and
mon
e
y. Especi
a
ll
y when th
e error i
s
di
sco
v
ered late i
n
the
desi
gn p
r
o
c
e
ss, la
rge a
m
ounts of effo
rt are
requi
re
d to co
rre
ct the erro
r. So we ne
ed
so
me
approa
che
s
t
o
di
scover e
rro
rs a
nd va
lidate d
e
si
gn
s a
s
ea
rly a
s
p
o
ssibl
e
.
Conve
n
tionall
y
,
simulatio
n
h
a
s
b
een th
e
main d
ebu
gg
ing te
chniq
u
e
, but it is i
n
com
p
lete
b
e
ca
use it ca
nno
t
involves all
p
o
ssible i
nput
values fo
r th
e co
mplex d
e
sig
n
. The
r
ef
ore, the
r
e
ha
s be
en
a recent
surge
of interest in fo
rmal
veri
fication
[1
]. One very
succe
ssful
formal verification ap
proa
ch
is
model che
cki
ng [2], it is a
n
automatic t
e
ch
niqu
e fo
r verifying finite-state
rea
c
ti
ve systems,
su
ch
as sequ
entia
l circuit desi
gns a
nd co
mmuni
cati
on
protocols.
The ba
sic id
ea of the model
che
c
king is t
hat it repre
s
e
n
ts t
he state
of the system
transfe
r stru
cture
with finite state mach
ine
(FSM), an
d repre
s
e
n
ts th
e pro
pertie
s
of the sy
ste
m
with CT
L formul
a, then
traverse FS
M to
che
c
k the co
rrectn
ess of the temporal logic form
ul
a. If temporal logi
c formul
a is n
o
t corre
c
t, the
system
will give an exampl
e fo
r user to find the error.
In this pa
per we verifie
d
the Spa
c
e
W
ire link inte
rfa
c
e [3], the ci
rcuit d
e
si
gn i
n
clu
d
e
s
eight m
odule
s
a
s
Figu
re
1
：
tran
smitter, cont
rolle
r,
receiver
, tim
e
r, recovery,
credit
co
unt
er,
tx_baudratecounter
and
error n
o
tificat
i
on. The mai
n
function
of controller i
s
to control t
he
transfo
rmatio
n betwe
en th
e states in th
e link, this
m
odule
control
s
the tran
smi
tter to send n
u
ll,
FCT and
no
rmal-cha
ra
cter
(N-Cha
r), al
so co
ntro
l
s
t
he reset of transmitte
r a
n
d
re
ceive
r
re
set
(the RX
-Rese
t, the TX-Re
s
et). The tra
n
smitter is
resp
onsi
b
le for
en
codi
ng dat
a a
nd tran
smittin
g
it using
the
DS en
co
ding
tech
nique.
T
he receiver
i
s
respon
sibl
e
for d
e
coding
the DS
sig
n
a
ls
(Din and Sin) to produc
e
a s
e
que
nce of
N-Chars
(data, EOP, EEP)
that are
pass
ed on to t
h
e
host
syste
m
. The
recovery is
used to
get rece
ive clock (RX_
CL
OCK)
by sim
p
ly
XORi
ng
t
he
received
Dat
a
and Stro
be
sign
als tog
e
ther. Th
e ti
me
r provides th
e
After
6.4µs a
nd After 12.8
µ
s
timeouts u
s
e
d
in link i
n
itia
lization. Th
e
function
of
error
notificatio
n is to de
al
with a vari
ety of
errors in the link. The cre
d
it counte
r
is u
s
ed to
control the numb
e
r of
normal
-
characters (N-Ch
a
r)
received by receive
r
, avoiding input bu
ffer over
flow
.The tx_baud
ratecounte
r
is re
spo
n
si
ble
for
controlling th
e freque
ncy o
f
the signal sent to transmi
tter module.
Literatu
re [4]
alre
ady verif
i
ed all
eight
module
s
se
p
a
rately, this
pape
r
we ve
rified the
comp
ositio
nal
model
of tra
n
smitter an
d
controlle
r, ex
tracted
relev
ant p
r
ope
rtie
s a
nd
used t
h
e
Cad
e
n
c
e SM
V [5-7] tool
to verify the interfa
c
e b
e
t
ween t
w
o
module
s
, furt
her
ensure the
corre
c
tne
s
s
of the whole
de
sign. SM
V is a
form
al
v
e
rificatio
n
sy
stem fo
r
h
a
rd
wa
re d
e
si
gns,
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
On The Mo
de
l Che
cki
ng of The Spa
c
e
W
i
r
e Lin
k
Interfa
c
e (Wei
Hua
)
741
based on a
t
e
ch
niqu
e call
ed symboli
c
model
chec
ki
ng [8].
Whe
n
to verify th
e
co
mpo
s
ition
a
l
model of tra
n
smitter an
d
controll
er, the size of
the prog
ram o
r
circuit will increa
se, and
th
e
numbe
r
of
state will
in
cre
a
se
expo
nent
ially and
ca
u
s
e th
e
state
explosi
on, thi
s
p
ape
r
will t
a
ke
the approp
ria
t
e method of modelin
g and
simplific
atio
n
techniq
u
e
s
to solve this p
r
oble
m
.
Figure 1. Structure of Th
e
Space
w
ire Li
nk Interfa
c
e
The re
st of the pape
r is organi
ze
d as follows. In se
ction 2, we briefly introdu
ce
transmitter a
nd co
ntrolle
r
of spa
c
e
w
ire. In sect
io
n 3, we present our exp
e
rie
n
c
e on th
e mo
del
che
c
king
of transmitte
r a
n
d
co
ntrolle
r
of
Space
W
i
r
e
u
s
ing
the
Ca
d
ence SMV to
ol. In sectio
n
4,
we u
s
e environment state
machi
ne to solve stat
e explosi
on. Secti
on 5 co
ncl
u
d
e
s the pa
per.
2. Transmitter and Co
ntr
o
ller Descrip
tion
2.1. Transmitter
The tran
smitter i
s
re
spon
sible
for
en
codi
ng
data
a
nd tra
n
smitting it u
s
ing
the
DS
encodin
g
te
chniqu
e. Figu
re 2 i
s
th
e
structu
r
e
of the tra
n
smitter, it ha
s
six
comp
one
nts.
It
receives
8 bits N-Chars fro
m
the host
system, turn
th
em into a se
rial data, then
transmit it wi
th
StrobeO
ut. If there i
s
neit
her
a Time
-Cod
e, FCT
n
o
r a
n
N-Cha
r
to tra
n
smit, the tra
n
smit
ter
sen
d
s
NULL.
The tra
n
smitter send
s N-Cha
r
s
only if
the ho
st syst
em at t
he oth
e
r en
d of the
link
has
ro
om in it
s ho
st receive buffer. T
h
is is indi
cate
d
by the othe
r li
nk inte
rfa
c
e
sendin
g
an
FCT,
sho
w
in
g that
it is ready to
accept
anoth
e
r 8
N-Cha
r
s. If a link i
n
te
rface
receive
s
a
n
F
C
T, it
will
transmit 8 N-Cha
r
s.
Whe
n
the Tick_IN
signal i
s
asse
rted the
trans
mitter
send
s out a Time-Cod
e as
soo
n
as
the transmitter ha
s finish
ed sen
d
ing t
he cu
rre
nt
chara
c
te
r or control code.
The value of
th
e
Time-Cod
e is the value of the Time_In and Contro
l
_
Flag_In
sign
als at the point in time when
Tick_IN i
s
asserte
d
.
A typical inte
rface
bet
wee
n
the ho
st
system
a
nd the
tran
smitter
compri
se
s TX
_Re
ady,
TX_Write an
d TX_Data.
Whe
n
the tra
n
smitter i
s
re
ady to receiv
e anothe
r N-Cha
r
from th
e host
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NIKA
Vol. 11, No. 2, Februa
ry 2013 : 740 – 746
742
system, it a
s
sert
s the
TX_
R
ea
dy sig
nal.
Wh
en th
e
h
o
st
sy
st
em h
a
s an N-
Ch
ar to tran
smit a
nd
the TX_
R
ea
d
y
sign
al i
s
a
s
serte
d
it m
a
y put th
e
N-Char onto
th
e TX_Data
line
s
a
nd asse
rt the
TX_Write sig
nal. Wh
en the tran
smitte
r ha
s re
gist
ered th
e N-Cha
r
data it
de-a
s
se
rts
the
TX_Re
ady si
gnal.
Figure 2. The
Tran
smitter
Structu
r
e
2.2. Contr
o
ller
Controlle
r ha
s seven
wo
rking
co
nditio
n
s
，
it control
s
the
ch
ang
e
of the state
s
of the
transmitter. Its op
eratio
n i
s
sho
w
n in F
i
gure
3.
Co
ntrolle
r convert
s
bet
wee
n
th
e seve
n stat
es
depe
nding
o
n
different tri
ggers, in
different
wo
rk
condition
allo
ws t
r
an
smitte
r to send
different
data type, so as to co
ntrol t
he tran
smitter.
Figure 3. State Diag
ram for Controll
er
The ErrorRe
s
et state
sh
all be e
n
tere
d afte
r a
system reset, after link
op
eration
i
s
terminate
d
for any re
ason
or if t
here i
s
an erro
r duri
n
g link initiali
zation. In the Erro
rReset state
the Tran
smitter
shall
be
reset.
Whe
n
the reset si
gn
al is
de-asse
rted, the
ErrorRe
s
et state
shall
be left uncon
ditionally after a delay of 6.4µs (no
m
inal
) and the stat
e machi
ne sh
all move to the
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
On The Mo
de
l Che
cki
ng of The Spa
c
e
W
i
r
e Lin
k
Interfa
c
e (Wei
Hua
)
743
Erro
rWait sta
t
e. In the ErrorWait state
the tra
n
smitter shall
be
re
set. The
Erro
rWait state
shall
be left un
con
d
itionally afte
r a d
e
lay of
12.8µs
and t
he state
ma
chine
shall
mo
ve to the Re
ady
state. In the
Erro
rWait sta
t
e, a
d
i
sc
on
ne
c
t
io
n e
r
r
o
r
is
de
te
c
t
ed
, or
if a
fte
r
the
go
tN
UL
L
c
o
nd
itio
n
is set, a parit
y erro
r or
escap
e
erro
r o
c
curs,
o
r
any
cha
r
a
c
ter
oth
e
r than
a NULL is
re
ceive
d
,
then the
stat
e ma
chine
shall move
b
a
ck to t
he E
rro
rReset sta
t
e. In
the Ready state
the
Tran
smitter
shall be rese
t. The state machi
ne
shal
l wait in the Ready
state
until the Link
Enabled becomes true and then it
shal
l move on int
o
the Starte
d state. If, whi
l
e in the Ready
state, a di
sco
nne
ction e
r
ro
r is
dete
c
ted,
or if a
fter th
e
gotNULL
co
n
d
ition is
set,
a pa
rity error
or
escap
e
error
occurs, or an
y chara
c
ter o
t
her
than a NULL is received, then the state machin
e
shall m
o
ve to the Erro
rReset st
ate. In the Started stat
e the tr
an
smit
ter sh
all be e
nable
d
and th
e
transmitter shall se
nd
NULLs. Th
e sta
t
e machi
ne
shall move to
the Con
n
e
c
ting state if the
gotNULL condition is
s
e
t. If, while in th
e Started s
t
ate, a dis
c
o
nnec
t
ion error is
detec
ted, or if
after the
got
NULL
co
nditi
on i
s
set, a
p
a
rity erro
r o
r
escap
e
e
r
ror
occurs,
or
an
y cha
r
a
c
ter o
t
her
than a
NULL
is
re
ceived,
then the
stat
e ma
chin
e
shall move
to
the Erro
rRe
s
et
state. In
the
Con
n
e
c
ting state the tran
smitter shall
be ena
bled t
o
sen
d
FCT
s
and
NULL
s. If an FCT
is
received
the
state m
a
chin
e shall
move
to the
Ru
n
state. If a
di
scon
ne
ct e
rro
r, parity e
r
ror
or
escap
e
e
rro
r
is dete
c
ted,
o
r
if any
cha
r
a
c
ter
ot
he
r tha
n
NULL
or F
C
T i
s
receive
d
, or th
e 12.8
µ
s
timeout then
the
state m
a
chi
ne
sh
all
move to
the
ErrorRe
s
et
state. In the
Ru
n
state t
h
e
transmitter i
s
ena
bled
to
send
Time-Co
des,
FCT
s
,
N-Ch
ars
and
NULL
s. If the
link inte
rface
is
disa
bled, or if a disco
nne
ct
erro
r, parity error, es
ca
pe
erro
r or cred
it error i
s
detected, while in
the Run
st
ate, then the stat
e m
a
chi
ne shall
move to t
he Erro
rRe
s
et state.
An
ErrAnaly
s
is_
D
ataSave st
ate wa
s add
ed in ord
e
r to improve th
e error an
alysis a
nd process
ability. When an
error occurs
or the link is
di
sabled i
n
the
run state, F
S
M enter into
ErrAnaly
s
is_
D
ataSave
sta
t
e. In the
sam
e
time,
FSM
save
and
an
a
l
yze the
erro
r and
the
data
.
If
the data
ha
s
been
save
d a
nd the
error h
a
s b
een
re
ad,
then the
FSM enter into
Erro
rReset
st
ate,
or still in the ErrAnal
y
s
is_DataSave state.
3. Model Ch
ecking
We ab
stracte
d
the cont
roll
er mod
u
le co
de and tran
smitter module
code from o
u
r whole
desi
gn, gen
erated a SMV model from V
e
rilog in the
Cad
e
n
c
e SM
V checkin
g
tool.
3.1. Properti
es De
scripti
on
Acco
rdi
ng to
the fun
c
tion
s of the
tran
smitter an
d
co
ntrolle
r d
e
scri
bed i
n
Se
ctio
n 2,
we
give 9
pro
p
e
r
ties. In the
fo
llowing
CTL
(
Comp
utat
ion
a
l Tree
Logi
c) exp
r
e
ssi
on
s, “*”,
“->” an
d
“
^”
mean lo
gical “and
”, “imply
” and “xo
r”, re
spe
c
tive
ly.“AG” an
d “AX”
are
CTL o
perators
meani
n
g
for
all paths in all
states, and f
o
r all pat
h
s
in
the next state, resp
ectivel
y
.
Prope
rty1: After link e
r
ror t
he Data
sign
als shall be
set to zero. Th
e CTL exp
r
e
ssi
on is
the following:
Property1: SPEC AG(Di
sconnectionE
rr
or=1 -> AF DataOut=0 );
Prope
rty2: After lin
k e
rro
r t
he Strob
e
si
g
nals
sh
all be
set to zero. The CT
L exp
r
e
ssi
on i
s
the following:
Property2: SPEC AG(Di
sconnectionE
rr
or=1 -> AF StrobeOut=0
);
Prope
rty3:In the ErrorWai
te state, the
Data
sig
nal
s
shall
be
set to zero.
T
he
CTL
expre
ssi
on is
the followin
g
:
Property3:SPEC AG (Spac
ewireC
ontrollerCurrentState = 0 &!
Reset & After64
->
AF
DataOut=
0 );
Prope
rty4:In the Erro
rWait
e
state, the
St
robe
sign
al
s shall be
set to zero. T
he CT
L
expre
ssi
on is
the followin
g
:
Property4: SPEC AG (Spac
e
wireControllerCurre
ntState =
0 &!Res
e
t & After64 ->
AF
StrobeO
ut=0 );
Prope
rty5:In the Re
ady sta
t
e, the Data signal
s
sh
all b
e
set to zero.
The CTL exp
r
essio
n
is
the following:
Property5:SPEC AG (Spac
e
wire
ControllerCurrentState =
1 &!Reset & Af
ter128 ->
AF
DataOut=
0 );
Prope
rty6:In the Rea
d
y state, the Strobe si
gnal
s
shall b
e
set
to zero. Th
e CTL
expre
ssi
on is
the followin
g
:
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NIKA
Vol. 11, No. 2, Februa
ry 2013 : 740 – 746
744
Property6: SPEC AG
(Spac
e
wireControllerCurre
ntState = 1 &!
Res
e
t & After128
-> AF
StrobeO
ut=0 );
Prope
rty7: After Reset the
Data
sign
als
shall
be
set t
o
ze
ro. T
he
CTL
expre
s
si
on is th
e
following:
Property7:SPEC AG (Reset ->
AF DataOut=
0
);
Prope
rty8: After Re
set the
Strobe sign
a
l
s sh
all be se
t to zero. Th
e CTL exp
r
e
ssi
on is
the following:
Property8: SPEC AG (Reset
-> AF StrobeOut=0 );
Prope
rty9: In
the Conn
ecti
ng state, if th
e tr
ansmitter sen
d
s a F
C
T, the Data and
Strobe
sign
als me
et DS encodin
g
rule. The
CTL
expressio
n
is the following:
Property9:SPEC AG(AX (Provide_F
CT
)& Spac
ewi
r
eControllerNex
tSta
te=4 & !Reset -
> AF(((AX AX DataOut
)
^(A
X
DataOut)) ^
((AX AX StrobeOut) ^ (AX
StrobeO
ut))));
3.2. Experimental Results
All
the
prope
rties we
re ch
ecked on
a
Micr
osoft Wi
ndo
ws XP
(2.
93G
Hz/2
GB).
Table
1
summ
ari
z
e
s
the experime
n
tal results i
n
clu
d
ing the
corre
c
tne
s
s of propertie
s
, CPU time
in
se
con
d
s, the
numbe
r of BDD n
ode
s ge
nerat
e
d
and t
he numb
e
r of
states rea
c
h
ed.
Table 1. Experime
n
tal Re
sults
Properties
results
CPU time
（）
seconds
BDD
Nodes Allocated
States Reached
propert
y
1
true
273.140625
20204995
6.33826e+029
propert
y
2
true
194.765625
13071242
2.5353e+030
propert
y
3
true
106.037791
9803754
6.33826e+029
propert
y
4
true
263.113372
11295352
2.5353e+030
propert
y
5
true
369.553416
9974210
6.33826e+029
propert
y
6
true
86.000727
11443055
2.5353e+030
propert
y
7
true
415.265625
10377115
3.16913e+029
propert
y
8
true
69.925872
11784565
1.26765e+030
propert
y
9
---
---
---
---
---
---
---
---
Prope
rty 1 to prope
rty 8 were verified
in reasona
bl
e CPU time. But when we
verified
the prop
erty 9, the compu
t
er run ab
out three ho
urs a
nd did not give any result, prod
uci
ng sta
t
e
explosi
on. The scale of the model is
expone
nt
ial both in the numbe
r of variabl
es a
n
d
the
numbe
r of p
a
rallel
execu
t
ion syste
m
comp
one
nts,
this me
an
s: For exa
m
pl
e, if you ad
d a
boole
an vari
a
b
le in the
pro
g
ram, d
oubl
e
the co
mple
xi
ty of its prop
erty verificati
on [9]. Whe
n
we
verify the co
mpositio
nal
model
of tra
n
smitter
and
cont
rolle
r, the si
ze
of the p
r
og
ram
wil
l
increase, the
number of va
riables
will increase and
in transmitter the data
wh
i
c
h i
s
transmitted
is
8 bits, so cau
s
e the state e
x
plosio
n.
4. En
v
i
ronment Sta
t
e Ma
chine
In order to
overcome
st
ate spa
c
e
e
x
plos
io
n, we
ado
pted
co
mpositio
nal
reasonin
g
method to
cut the
whole
system
into
small
pa
rts,
then u
s
e
th
e sm
all p
a
rt
s to ve
rify the
prop
ertie
s
. But becau
se t
he compo
n
e
n
ts de
pen
d
on ea
ch
oth
e
r, we
have
to assume
the
behavio
r of t
he othe
r
co
mpone
nts
when
we ve
ri
f
y
the prope
rties of o
ne
comp
one
nt. The
rea
s
oni
ng p
r
o
c
e
ss of this m
e
thod a
s
follo
w [10]:
||
Nf
f
Mg
M
Ng
Here, we a
r
e
assertin
g that if:
1.
N sat
i
sf
ies f
2.
if the enviro
n
m
ent of M
sa
tisfies f, then
M sa
ti
sfies g
then the
co
mpositio
n of
M and
N
will sati
sfy
g.
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
On The Mo
de
l Che
cki
ng of The Spa
c
e
W
i
r
e Lin
k
Interfa
c
e (Wei
Hua
)
745
The advanta
ge of doin
g
the verificati
on in this m
anne
r is th
at we neve
r
h
a
ve to
examine the
comp
osite
st
ate sp
ace of
M and
N.
In
stead,
we
ch
eck if u
s
ing j
u
st N,
and th
en
che
c
k g usi
n
g
only M and the assum
p
tio
n
g whi
c
h is a
n
environ
men
t
of M.
Based
on the
above comp
osition
a
l re
asoning m
e
tho
d
, we e
s
tabli
s
h envi
r
onm
e
n
t state
machi
ne to e
x
press the
b
ehavior
of the cont
ro
lle
r, only abst
r
a
c
ting away the
behavio
r of the
controlle
r whi
c
h involve
s
t
he p
r
ope
rty 9
.
Becau
s
e
property 9
mea
n
s in
the
con
nectin
g
state,
if
the transmitter sen
d
s a F
C
T, the Data and Strobe si
g
nals me
et DS enco
d
ing rul
e
. So we igno
re
the errors in the link a
nd some varia
b
le
s whi
c
h d
o
no
t involve the
prop
erty 9. Then we mode
l the
abstracte
d co
ntrolle
r in SMV instead of o
r
iginal
cont
rol
l
er mod
u
le co
de in circuit d
e
sig
n
.
Figure 4 is the ab
stra
cte
d
environ
me
nt st
ate machine and
rep
r
esents the b
ehavior of
the controlle
r. States S
0
to S6
co
rresp
ond
w
i
th Er
rorR
es
et, Er
rorW
ait, Rea
d
y,
Started,
Con
n
e
c
ting, Run a
nd ErrAnalysis_DataSave ,
resp
ectively. TX_Re
s
et, Send_
NULL, Send_
FCT
and Send_Al
l
are the interf
ace
s
with tra
n
smitter. Th
e
y
are valid on
ly in certain st
ates.
Figure 4. Environme
n
t State Machi
n
e
The environm
ent state machine is comp
ose
d
wi
th the
transmitter,
as sho
w
n in Figure 5.
We u
s
e environment state
machi
ne to control
s
t
he ch
ange of the st
ates of the tra
n
smitter.
Figure 5. Co
mbined State
Machin
e
Then
we veri
fied Property 9:SPEC AG(AX
(Provide_FCT)& stat
e=S4 -> AF(((AX AX
DataO
u
t)^(A
X
DataOut))
^ ((AX AX StrobeO
ut) ^ (A
X StrobeOut
)))); The re
sult
sho
w
s
as T
a
ble
2. By this method, Prop
erty 9 was ve
ri
fied in SMV with a reasona
ble
CPU time.
Table 2. Experime
n
tal Re
sults After Establishi
ng En
vironme
n
t State Machi
n
e
Propert
y
result
CPU time
（）
seconds
BDD
Nodes Allocated
States Reached
propert
y
9
true
391.847020
60928438
4.95176e+027
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NIKA
Vol. 11, No. 2, Februa
ry 2013 : 740 – 746
746
5. Conclusio
n
In this
pap
e
r
, we a
pplie
d mod
e
l
ch
ecking
to ve
rify tran
smitter
and
controller
of
Space
W
i
r
e. Ho
wever, we encounte
r
ed state
spa
c
e
e
x
plosio
n prob
lem. This
ha
s been
solve
d
by
establi
s
hi
ng environ
ment state
ma
chin
e
whi
c
h
we
redu
ce
d un
related
de
sig
n
details
wh
en
verifying
a
p
r
ope
rty
,
In this wo
rk, m
odel ch
eckin
g
of all
the
prop
ertie
s
are
do
ne with
a
rea
s
on
able ti
me.
Referen
ces
[1]
C Kern, M Greenstreet,
Formal Verific
a
tion in Hard
wa
re
De
si
gn
: A Su
rvey.
ACM
T
r
ans. on Desi
g
n
Automatio
n
of Electron
ic S
y
st
ems. 1999; 4: 123-
193.
[2]
EM Clarke, O Grumberg, DA
Peled.
Mode
l Checki
ng.
MIT
Press. 2000.
[3]
ECSS Stand
ard ECSS-E-ST
-50-1
2
C. Spac
e
W
ire – Links. N
odes, Ro
uters and N
e
t
w
orks.
[4]
Dai
Z
h
iq
uan.
F
o
rmal v
e
rification for t
he syst
em of harsh
environment and
high-
s
peed
bus based on
mo
de
l checki
n
g
. Beiji
ng: Ca
pi
tal Normal U
n
i
v
ersit
y
. 2
011.
[5]
K
McMilla
n.
Getting started
with SMV
. SMV Refere
nce
Manu
al. Ca
de
nce Berk
ele
y
Labs: Berk
el
e
y
,
199
9.
[6]
K
McMillan.
T
h
e SMV lang
ua
ge.
SMV Reference Ma
nu
al. Cad
ence B
e
rkele
y
L
abs: Ber
k
ele
y
. 19
99.
[7]
K
McMillan.
The Model Checking System
.
SMV Refe
rence Ma
nua
l. Cade
nce Be
rkele
y
L
a
b
s
:
Be
rke
l
ey
. 20
02.
[8]
K
McMillan.
Sy
mb
olic Mo
de
l Checki
ng; Klu
w
er Acade
mic
Publ
ishers
. Bo
ston: Massach
usetts. 1993.
[9]
Michacl Huth, Mark Ry
an.
Lo
gic in C
o
mpute
r
Science
. Ch
in
a Machi
ne Pre
ss. 2007.
[10]
Pnue
li
A.
In Transiti
on for Glob
al to Modu
l
a
r T
e
mp
oral R
easo
n
in
g Abo
u
t Progra
m
s
In
KR
Apt
ed
Log
ics an
d Mo
dels of Co
ncurr
ent System
. N
A
T
0
ASI 13. Sprin
ger
.
198
4.
Evaluation Warning : The document was created with Spire.PDF for Python.