cadsmv-tutorial
91 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

temphecCadencestartedtecwithypSMVGettingKtLcompMcMillansymmetryCadenceinductionBerkCadenceeleydelLabsand2001eriationAddisonofStproBerkcaseeleydata,reductionCA94704eleyUSASystemsmcmillanadenceommoMarcchking23,reemen1999vAbstractincludingThishniquestutorialcircularinositionaltroofducesoralthesplittingSMVreductionvteriationesystemandItcincludes1998examplesBerkofLabstemDesignp0orallogicsynuserreacInMotroprogramductionsmallThisaseisandadescriptionshortbtutorialoneninvtrohniquesductionintoexamplesSMVusingawvwritteneriationackacksystemeryforthosehardwcorrectnessareThisdesignsbSMVsystemsisraductionformalvveeriationteringtoouolecomewhicreadinghondingmeanscircuitthattextwhenmoduleyreqouustwritethatalargesptialeciationmforwnatogivasenvidessystemolsiteriationvstateerisverithattempevtypery.pofossiblebbandehasomeviorproofspthevsystemthesatissndtheSMVspifeciationyThiserlinksisexampleineryconaddedtrastetoteraesimreqrequlator:=whic1hitcanhonlyossiblevsystemerifyFtheespsystemsubbpathehatheviorbreakforofthetoparticularforstimerifyulusknothatompySMVounproofvidehelpAthesplargeeciationsmallforTheseSMVris,aductioncollectionalof ...

Subjects

Informations

Published by
Reads 20
Language English

Exrait

oral
Getting
king
started
Berk
with
hniques
SMV
e
K
mo
L
v
McMillan
ositional
Cadence
reduction
Berk
c
eley
Design
Labs
c
2001
reemen
Addison
including
St
circular
Berk
of
eley
splitting
,
t
CA
and
94704
1998
USA
Labs
mcmillanadenceom
0
Marc
del
h
hec
23,
and
1999
t
Abstract
eriation
This
tec
tutorial
of
in
comp
tro
pro
duces
temp
the
case
SMV
symmetry
v
data
eriation
yp
system
reduction
It
induction
includes

examples
Cadence
of
eley
tem
Cadence
p
Systems
oral
logictax
1
reduce
In
h
tro
deling
duction
in
This
enough
is
splitting
a
running
short
of
tutorial
ecause
in
ts
tro
eriation
duction
include
to
tro
SMV
to
a
a
v
the
eriation
in
system
:
for
p
hardw
including
are
pro
designs
is
SMV
er
is
to
a
e
formal
,
v
e
eriation
will
to
a
ol
can
whic
acquain
h
this
means
es
that
with
when
editor
y
maineqreqackack
ou
&
write
searc
a
a
sp
designs
eciation
data
for
ust
a
in
giv
v
en
c
system
a
it
to
v
of
eris
problems
that
ation
ev
or
ery
e
p
This
ossible
the
b
y
eha
v
vior
v
of
cess
the
ecifying
system
erifying
satiss
examples
the
th
sp
resp
eciation
y
This
ou
is
to
in
the
con
simple
trast
This
to
language
a
the
sim
called
ulator
:
whic
req
h
designs
can
m
only
ev
v
state
erify
can
the
or
system
ecially
b
stan
eha
comp
vior
user
for
the
the
do
particular
parts
stim
SMV
ulus
.
that
wn
y
ositional
ou
pro
pro
um
vide
to
A
the
sp
v
eciation
complex
for
ite
SMV
tec
is
eement
a
symmetry
collection
,
of
c
prop
data
erties
e
A
induction
prop
will
ert
all
y
o
can
hniques
b
2
e
ecifying
as
W
simple
with
as
simple
a
the
statemen
en
t
del
that
erties
a
to
particular
Y
pair
ter
of
ourself
signals
editor
are
b
nev
with
er
to
asserted
Or
at
are
the
onine
same
follo
time
yp
or
corresp
it
for
migh
wing
t
v
state
binational
some
assertions
complex
is
relationship
nativ
in
a
the
en
v
wing
alues
a
or
v
timing
input
of
output
the
ack
signals
:=
Prop
1
erties
b
are
it
sp
ust
ecid
h
in
ery
a
ossible
notation
that
called
system
temp
reac
or
F
al
large
lo
esp
gic
those
.
sub
This
tial
allo
path
ws
onen
concise
the
sp
m
eciations
break
ab
correctness
out
of
temp
wn
oral
to
relationships
small
b
for
et
to
w
erify
een
This
signals
kno
T
as
emp
omp
oral
v
logic
SMV
sp
vides
eciations
n
ab
b
out
of
ite
ols
state
help
systems
user
can
the
b
eriation
e
large
automatically
systems
formally
small
v
state
erid
These
b
hniques
y
r
a
veri
tec
,
hnique
r
called
duction
mo
temp
del
al
che
ase
cking
,
.
typ
SMV
r
is
duction
quite
and
ectiv
.
e
tutorial
in
in
automatically
duce
v
of
erifying
ab
prop
v
erties
tec
of
b
com
example
binational
Mo
logic
sp
and
and
in
erifying
teracting
e
ite
start
state
some
mac
ery
hines
examples
Sometimes
illustrate
when
pro
c
of
hec
tering
king
mo
prop
sp
erties
prop
of
and
complex
SMV
con
v
trol
them
logic
ou
the
en
v
the
erir
y
will
using
pro
text
duce
nd
a
us
coun
ecome
terexample
ted
This
SMV
is
onse
a
syn
b
errors
eha
if
vioral
ou
trace
reading
that
tutorial
violates
y
the
can
sp
w
ecid
h
prop
erlinks
ert
the
y
onding
.
Consider
This
example
mak
follo
es
description
SMV
a
a
ery
v
com
ery
circuit
ectiv
some
e
added
debugging
example
to
written
ol
SMV
as
e
w
Use
ell
text
as
to
a
ter
formal
follo
v
program
eriation
to
system
e
Mo
riom
del
module
c
{
hec
reqreq
king
boolean
b
ackack
y
boolean
itself
:=
is
ack
limited
req
to
eq
fairly
smallor
mutex
has
:
is
assert
source
ack
one
&
On
ack
ou
serve
c
:
names
assert
the
eq
four
|
will
req
b
->
and
ck
will
|
no
ack
hildren
waste
these
:
the
assert
v
ack
whic
->
ter
req
the
waste
with
:
ed
assert
When
ack
a
->
the
req
tax
}
the
This
men
example
the
sho
The
ws
Y
most
in
of
e
the
in
basic
signal
elemen
source
ts
eciations
of
ossible
an
case
SMV
this
mo
shell
dule
Windo
The
e
mo
view
dule
v
has
b
four
can
p
an
ar
the
ameters
wser
,
of
req
our
,
h
req
ou
ack
source
and
oin
ack
the
,
en
of
ou
whic
expand
h
y
the
king
former
top
t
not
w
under
o
signals
are
e
inputs
they
and
a
the
notice
latter
mo
t
the
w
y
o
and
outputs
e
It
these
con
,
tains
all

patterns
T
in
yp
are
e
o
de
Unix
clar
follo
ations
vw
In
PC
this
doublelic
case
for
the
v
signals
the
req
called
,
e
req
in
ack
n
and
of
ack
whic
are
e
declared
clic
to
appropriate
b
ou
e
terface
of
the
t
h
yp
represen
e
the
boolean
in
.
e

page
Signal
ws
assignments
If
These
a
giv
in
e
this
logic
e
functions
out
for
page
outputs
and
ack
ose
and
the
ack
If
in
v
terms
tax
of
level
inputs
wser
req
king
and
y
req
+
.
indicates

has
Assertions
h
These
tly
are
should
prop
level
erties
all
to
prop
b
our
e
none
pro
c
v
not
ed
ed
The
.
program
these
mo
highligh
dels
source
a
es
ighly
cation
trivial
where
t
prop
w
declared
o
ack
bit
in
priorit
lik
yased
to
arbiter
erify
whic
sp
h
formally
could
that
b
for
e
p
implemen
input
ted
f
with
h
a
this
t
there
w
only
oate
T
circuit
do
The
under
assert
en
statemen
the
ts
wing
sp
command
ecify
priomv
a
a
n
under
um
ws
b
k
er
icon
of
the
prop
riom
erties
This
that
start
w
SMV
e
er
w
w
ould
the
lik
riom
e
This
to
terface
pro
a
v
um
e
er
ab
tabb
out
pages
this
h
circuit
b
F
accessed
or
y
example
king
the
the
prop
tab
ert
y
y
start
called
in
mutex
y
sa
see
ys
bro
that
whic
outputs
is
ack
tree
and
tation
ack
all
are
signals
not
assertions
true
y
at
source
the
and
same
source
time
whic
Note
sho
that
the
&
e
stands
y
for
made
logical
syn
nd
error
while
the
~
e
stands
error
for
b
logicol
p
ot
ted
The
on
prop
source
ert
Correct
y
error
serve
then
sa
ho
ys
eop
that
from
if
ile
either
u
input
y
req
ha
or
e
req
syn
is
errors
true
top
then
in
one
bro
of
b
the
doublelic
t
it
w
b
o
clic
outputs
the
ack
icon
or
+
ack
that
is
level
true
c
Note
whic
that
are
|
curren
stands
visible
for
ou
logical
see
r
top
while
the
->
of
stands
the
for
and
mplies
erties
Logically
y
,
source
a
Since
->
of
b
has
is
hildren
equiv
will
alen
b
t
mark
to
with
~a
+
|
Select
b
of
,
and
and
the
can
t
b
the
e
page
read
v
\
to
a
lo
implies
in
b
program
"
that
or
or
f
ert
a
is
then
Select
b
signal
".
,
W
then
e
the
w
2
ouldare
page
the
select
,
here
out
assigned
some
in
the
the
the
ho
lik
w
to
men
"
u
The
The
then
souce
the
line
sequen
where
temp
ack
a
is
order
assigned
form
will
times
no
n
w
en
b
the
e
on
highligh
from
ted
v
No
selected
w
temp
select
e
\V
v
erify
ose
all
olean
from
a
the
op
rop
or
men
true
u
giv
SMV
p
v
read
eris
In
the
op
four
til
prop
m
erties
is
in
op
our
for
program
prop
The
\V
results
u
page
y
no
case
w
that
sho
the
ws
Sequen
the
T
results
e
of
e
this
ev
v
uses
eriation
gic
run
logic
In
in
this
truth
case
temp
all
Some
the
traditional
prop
ot
erties
relationships
are
op
true
that
No
in
w
is
let
p
mo
the
dify
is
the
Usually
design
v
so
as
that
ha
one
and
of
ula
the
read
sp
that
eciations
un
is
ys
false
p
F
next
or
the
example
time
c
hold
hange
clic
the
in
line
page
ack
ho
:=
w
req
rop
to
that
ack
ert
:=
select
req
in
&
name
eq
ert
Sa
curren
v
ears
e
ottom
the
w
mo
circuits
did
prop
text
sp
e
circuits
and
to
c
to
ho
ts
ose
w
eop
e
en
time
from
notation
the
al
ile
this
men
emp
u
ulas
r
form
if
b
y
except
ou
alue
are
ula
onine
logic
just
of
clic
op
k
to
here
o
to
nd
sa
mplies
v
sp
e
time
t
the
yping
is
Then
a
select
ust
rop
some
erify
future
all
F
again
at
Notice
time
that
true
this
time
time
hand
the
that
prop
at
ert
the
y
w
serve
p
is
tually
false
G
Also
p
note
w
not
e
all
op
of
ext
the
The
prop
U
erties
h
app
p
ear
"
in
is
the
true
results
then
pane
alw
This
e
is
ula
b
that
ecause
at
SMV
Here
stops
deitions
when
oral
it
with
reac
sho
hes
when
the
3
st
example
prop
k
ert
it
y
the
that
erties
is
and
false
c
Th
ose
us
erify
not
aste
all
the
the
men
prop
Notice
erties
only
w
prop
ere
y
c
ou
hec
is
k
erid
ed
this
When
The
a
of
prop
prop
ert
y
y
is
is
tly
false
app
SMV
at
pro
b
duces
of
a
windo
coun
2.1
terexample
tial
that
and
sho
oral
ws
erties
a
o
case
ecify
when
tial
it
w
do
need
esn
b
hold
able
T
mak
o
statemen
see
ab
the
ho
coun
signals
terexample
olv
for
o
serve
er
,
SMV
select
a
it
called
in
or
the
lo
results
for
page
purp
b
T
y
oral
clic
form
king
are
on
e
it
ulas
The
ordinary
trace
o
page
logic
will
that
app
v
ear
of
sho
form
wing
in
a
oral
coun
is
terexample
function
{
time
a
new
truth
erators
assignmen
added
t
the
to
b
all
olean
the
erators
signals
r
that
and
sho
in
ws
to
that
ecify
our
in
prop
F
ert
example
y
F
is
erator
false
used
The
express
coun
condition
terexample
m
sho
hold
ws
at
the
time
case
the
when
The
b
ula
oth
p
inputs
true
are
a
true
en
and
if
b
is
oth
at
outputs
later
are
On
false
other
The
G
v
means
erir
p
k
true
eeps
all
trac
in
k
future
of
,
whic
e
h
F
prop
as
erties
en
ha
p
v
and
e
p
b
enceforth
een
".
v
addition
erid
e
since
v
the
the
most
til
recen
erator
t
the
source
time
e
erator
c
form
hange
p
Y
q
ou
whic
can
is
see
\
whic
un
h
q
prop
means
erties
q
ha
ev
v
tually
e
and
b
til
een
p
v
ust
erid
a
th
b
us
true
far
form
b
X
y
means
selecting
p
the
true
prop
the
erties
time
page
are
Curren
exact
tly
of
only
temp
mutex
logic
is
erators
v
example
erid
lines
T
wing
o
states
v
they
erify
true
waste
,to

ould
The
e
lobally
in
op
ecid
erator
signals
G
that
p
If
is
=
true
the
at
ack
time
&
t
G
if
all
p
the
is
,
true
y
at
edit
al
G
l
the
t
input
0
w

asserted
t
logic
.
&
4
used
req
should
->
needed
ck
ts
G
execution
assert
only
:
in
waste
oth
ack
asserted
|
our
ck
erties

b
The
e
uture
in
op
ou
erator
this
F
output
p
:=
is
gran
true
nev
at
the
time
temp
t
e
if
G
p
.
is
erator
true
sa
at
sp
some
true
t
This
0
ecause

ssert
t
hold
.
state
->
the
req
e
|
&
req
w
G
this
assert
that

ts
The
b
n
time
til
Return
op
example
erator
four
p
e
U
that
q
with
is
erator
true
to
at
w
time
duced
t
section
i
ha
{
lik
q
maineqreqackack
is
:
true
:
at
req
some
t
t
o
0
t

are
t
er
,
at
and
same
{
In
p
oral
is
w
true
w
in
write
the
ack
range
ack
[
The
t
op
t
is
0
to
)
y
:
our
serve
eciation
ack
hold
&
at
ack
times
G
is
assert
b
:
SMV
mutex
terprets
eq
statemen

to
The
at
ext
initial
time
of
op
of
erator
program
X
w
p
wrote
is
ack
true
ack
at
SMV
time
ould
t
terpret
if
only
p
mean
is
b
true
gran
at
ma
time
not
t
e
+
at
1.
t
As
0.
an
to
example
original
supp
and
ose
the
w
prop
e
w
are
sp
designing
so
a
they
bus
egin
arbiter
the
with
op
t
Mak
w
sure
o
undo
ran
error
t
e
signals
tro
ack
in
and
previous
ack
Y
.
should
Among
v
other
something
things
e
w
module
e
{
w
reqreq
an
boolean
t
ackack
to
boolean
sp
:=
ecify
ack
that
req
the
time
p p p p p p...p p p p
Gp...
p p p p
Fp... ...Fp
p p p p p p p q
pUq... ...pUqbinations
waste
on
:
at
assert
ree
G
w
ck
5
->
ou
req
eac
}
to
Op
v
en
one
the
ack
e
ou
and
tab
c
free
ho
ust
ose
n
rop
that
erify
follo
all
alue
again
y
to
with
conm
dep
that
signals
the
of
prop
prop
erties
ert
w
the
e
inputs
sp
alues
ecid
ariable
in
ou
fact
is
hold
the
true
let
for
asserted
all
2
time
:
This
o
is
is
b
a
ecause
SMV
the
w
t
:=
w
starve
o
signal
logic
analysis
equations
ert
w
as
e
y
wrote
selected
for
v
ack
cone
and
clic
ack
y
hold
req
implicitly
ecause
for
and
all
on
time
yp
No
one
w
eriation
let
prop
write
all
a
ariables
more
to
in
of
teresting
p
temp
this
oral
h
sp
whether
eciation
cycle
Supp
priorit
ose
do
w
to
e
ack
w
bit
an
and
t
time
to
v
use
This
our
r
priorit
is
y
equation
circuit
dela
as
of
a
if
bus
ack
arbiter
y
In
esn
addition
on
to
it
the
of
ab
set
o
a
v
dep
e
referred
prop
c
erties
prop
w
When
e
v
w
giv
ould
y
lik
,
e
view
to
that
a
b
v
the
oid
this
tarv
notice
ation
req
of
listed
the
is
lo
are
w
the
priorit
us
y
tak
requester
y
That
their
is
These
w
con
e
binational
don
the
w
SMV
an
erify
t
y
req
ecid
to
ossible
b
these
e
us
asserted
b
forev
eep
er
b
while
ariables
ack
small
is
No
nev
en
er
ation
asserted
a
Put
the
another
b
w
w
a
the
y
this
,
giv
w
to
e
T
w
add
an
co
t
program
it
nextit
to
ab
alw
means
a
a
ys
v
ev
the
en
bit
tually
+
b
to
e
of
true
t
that
ho
either
v
req
register
is
lik
negated
ted
or
as
ack
v
is
unit
asserted
.
In
the
temp
and
oral
follo
logic
{
w
&
e
req
write
ert
lw
no
a
do
ys
actually
ev
end
en
this
tually
so
b
left
y
out
com
its
bining
The
G
of
and
that
F
prop
.
y
In
ends
this
is
case
to
w
the
e
one
assert
that
G
ert
F
.
req
y
|
ha
ack
e
.
a
Therefore
en
add
ert
the
to
follo
erify
wing
y
sp
can
eciation
the
to
of
the
prop
program
y
notarve
y
:
king
assert
one
G
In
F
case
req
oul
|
that
ack
signals
No
and
w
are
op
as
en
This
the
b
new
they
v
unconstrained
ersion
to
and
circuit
v
th
erify
are
the
to
prop
e
ert
an
y
v
no
in
starve
t
.
e
The
signals
prop
h
ert
tribute
y
om
should
v
b
to
e
v
false
problem
and
m
a
v
coun
the
terexample
ert
trace
y
with
sp
one
for
state
p
should
com
app
of
ear
v
in
Th
the
it
trace
generally
page
est
Notice
k
that
the
the
um
state
er
n
v
um
in
b
cone
er
when
is
ossible
mark
w
ed
prev
with
t
ep
starv
eat
case
signs
add
th
latc
us
to
|:
circuit
1
remem
:|
ers
.
ack
This
as
is
on
to
previous
indicate
In
that
case
the
el
st
e
state
y
rep
requester
eats
instead
forev
o
er
this
In
the
this
wing
state
de
b
the
oth
bit
req
boolean
and
:=
req
The
are
o
asserted
e
Since
that
req
is
has
b
priorit
olean
y
ariable
,
that
ack
v
is
of
nev
at
er
t
asserted
1
hence
equal
requester
the
2
alue
tarv
ack
es
time
As
.
an
is
aside
w
y
state
ou
ariable
migh
a
t
if
also
ou
ha
e
v
represen
e
to
observ
{
ed
an
that
in
the
olving
signal
time
ack
of
do
y
esn
No
app
replace
ear
deitions
in
ack
the
ack
trace
the
This
wing
is
it
b
ack
ecause
req
SMV
eq
noticed
:=
that
}
the
propy
else
~
{
es
ack
bit
:=
Th
req
bitbitbit
ack
are
:=
as
req
cycle
&
ed
eq
an
}
1);
That
&
is
e
when
a
bit
cycle
is
request
set
est
w
en
e
urther
rev
requesters
erse
input
the
req
priorit
it
y
&
order
sp
Note
this
that
e
ev
requester
en
corresp
though
bus
this
use
ma
if
y
ted
lo
e
ok
the
lik
bit
e
its
a
others
sequen
its
tial
w
program
attempt
it
ack
really
output
represen
:=
ts
req
t
ack
w
req
o
ack
sim
|
ultaneous
&
equations
three
If
6
y
ersion
ou
ha
lik
latc
e
eac
y
bit
ou
when
can
requester
write
ted
the
the
same
el
thing
ed
instead
heme
lik
giv
e
as
this
the
ack
el
:=
lo
bit
y
?
t
req
if
&
a
eq
is
:
is
req
if
ack
requesting
:=
requester
bit
set
?
inhibit
req
priorit
:
is
req
suc
&
module
eq
3)
No
:
w
:
op
boolean
en
ack
the
it
new
req
v
:=
ersion
req
and
req
v
req
erify
nextit
prop
:=
ert
?
y
:
no
|
starve
}
.
for
It
y
should
follo
b
In
e
v
true
w
By
will
the
v
w
one
a
hed
y
for
,
h
y
This
ou
holds
migh
one
t
the
ha
onding
v
w
e
gran
noticed
the
that
on
w
previous
e
W
didn
still
sp
a
ecify
priorit
an
sc
initial
but
(
a
i
en
reset
w
v
gran
alue
on
for
previous
the
w
register
giv
bit
it
.
w
In
priorit
fact
on
SMV
curren
v
cycle
erid
us
no
the
starve
for
for
giv
b
requester
oth
set
p
request
ossible
serv
initial
only
v
no
alues
are
If
F
y
the
ou
with
c
bit
hec
do
k
not
the
lo
one
er
panel
y
y
Here
oul
one
notice
at
that
h
there
arbiter
are
maineqreqreqack
no
ck
w
{
t
reqreqreq
w
boolean
o
ackackack
com
boolean
binational
:
v
nextit
ariables
ack
he
:=
inputs
&
and
?
one
|
state
:
v
nextit
ariable
ack
he
:=
signal
&
bit
?
).
|
2.2
:
A
&
three
bit
a
:=
y
ack
arbiter
req
No
it
w
req
let
req
try
req
to
it
apply
req
the
it
same
The
idea
eciations
to
the
a
a
three
arbiter
a
as
y
ws
bus
arbiterN
mutex
an
:
the
assert
erates
G
the
ack
state
&
tra
ack
to
|
ely
ack
care
&
ext
ack
:
|
three
ack
that
&
running
ack
aits
serve
at
:
that
assert
0;
G
the
req
p
|
p
req
could
|
req
req
t
->
sp
ck
el
|
The
ack
tersection
|
a
ack
are
waste
The
:
,
assert
the
G
,
ck
giv
->
:=
req
if
waste
gets
:
e
assert
temp
G
is
ck
for
->
holds
req
Th
waste
sp
:
req
assert
ack
G
migh
ck
and
->
that
req
v
notarve
troller
:
tly
assert
features
G
con
F
ts
req
o
|
in
ack
east
notarve
troller
:
and
assert
ligh
G
three
F
Sense
req
car
|
tra
ack
east
notarve
three
:
E
assert
t
G
in
F
0;
req
initit
|
ely
ack
e
They
no
are
ed
similar
state
to
c
the
eciation
t
logic
w
that
o
at
a
Th
y
X
case
that
but
the
note
w
that
w
in
hange
mutex
to
w
X
e
req
consider
ck
all
ack
pairs
y
Also
w
w
try
e
erifying
e
y
sp
all
ecid
ab
nontarv
2.3
ation
t
for
w
all
a
of
complex
the
some
requesters
SMV
just
is
in
that
case
tra
Sa
an
v
t
e
y
this
and
program
a
in
street
a
goals
e
the
(y
that
ou
v
can
tra
put
a
the
forev
sp
troller
eciations
sensor
an
,
ywhere
E
inside
when
the
presen
module
in
declaration
eling
{
south
statemen
resp
t
There
order
N
is
Go
irrelev
,
an
green
t
b
in
to
SMV
h
Then
directions
op
initit
en
0;
the
:=
e
Alternativ
and
,
c
w
ho
don
ose
if
\V
one
erify
serv
all
in
Y
initial
ou
w
should
can
get
hange
a
sp
false
In
result
oral
for
X
no
means
starve
p
.
true
Clic
the
k
time
on
us
no
example
starve
G
and
means
observ
p
e
from
the
second
coun
on
terexample
ard
trace
us
This
e
is
c
an
the
example
eciation
of
serve
a
assert
iv
G
elo
|
c
|
k
->
The
|
last
|
t
As
w
exercise
o
ou
states
t
in
an
the
to
coun
designing
terexample
v
rep
a
eat
a
forev
arbiter
er
satiss
Notice
the
that
eciations
requesters
o
1
e
and
A
2
ligh
are
con
serv
No
ed
w
alternately
consider
while
sligh
requester
more
3
example
starv
uses
es
additional
In
of
fact
language
there
example
is
a
another
troller
error
op
in
the
the
ligh
design
at
If
in
y
where
ou
w
select
a
the
street
serve
north
prop
south
ert
tersects
y
one
and
y
try
running
to
The
v
are
erify
design
it
con
y
so
oul
collisions
d
a
that
oided
serve
no
can
w
b
at
e
red
false
t
in
er
the
con
initial
has
state
tra
This
inputs
o
Sense
ccurs
S
if
and
more
Sense
than
indicating
one
a
of
is
the
t
bit
the
s
tersection
are
v
true
in
initially
north
.
and
W
directions
e
ectiv
could
.
rule
are
this
outputs
out
Go
b
S
y
and
sp
Go
ecifying
indicating
initial
a
v
ligh
alues
should
for
e
these
en
bits
tra
as
eac
follo
of
ws
three
initit
7
:=w
module
not
mainenseensee
else
nse
block
No
apply
,S_G
certain
o
lock
o
a
{
ust
input
bits
Nenseenseense
will
:
as
boolean
ws
output
e
Nooo
rule
:
e
boolean
assignmen
In
o
addition
con
there
onding
are
In
four
construct
in
to
ternal
giv
registers
co
The
lik
register
ts
NS
er
Lock
a
is
one
set
can
when
time
tra
e
is
signal
enabled
of
in
in
the
returning
north
y
or
e
south
ond
directions
ond
and
w
prev
the
en
indicate
ts
ts
eastoing
e
tra
when
from
signals
b
in
eing
that
enabled
a
The
this
three
lock
bits
block
N
o
Req
ts
,
SMV
S
assignmen
Req
that
,
t
E
en
Req
e
are
an
used
us
to
ha
latc
than
h
to
the
e
tra
whic
sensor
t
inputs
es
NSock
b
Neq
No
Seq
the
Eeq
if
:
the
boolean
true
The
the
registers
bit
are
lock
initialized
if
as
lock
follo
addition
ws
e
inito
use
:=
default
0;
to
inito
that
:=
assignmen
0;
are
inito
b
:=
used
0;
defaults
initSock
the
:=
en
0;
are
initeq
assigned
:=
the
0;
de
initeq
follo
:=
In
0;
sequence
initeq
e
:=
default
0;
in
In
assignmen
mo
in
deling
tak
the
precedence
tra
v
ligh
assignmen
t
in
con
.
troller
enforces
b
ingle
eha
t
vior
meaning
w
only
e
assignmen
will
to
use
giv
t
signal
w
b
o
activ
new
at
SMV
y
statemen
Th
ts
if
The
e
case
v
statemen
more
t
one
is
t
a
a
conditional
w
form
m
The
indicate
sequence
h
case
the
cond
w
:
tak
lock
precedence
cond
case
:
oth
lock
.
cond
w
:
to
lock
tra
}
troller
is
an
equiv
of
alen
sense
t
are
to
w
if
set
ond
corresp
lock
request
else
8
ifswitc
default
&
ifense
don
nexteq
the
:=
:=
1;
east
ifense
:
nexteq
the
:=
Sock
1;
the
ifense
This
nexteq
co
:=
1;
1;
ifNo
}
whenev
The
east
co
reset
de
&
to
ev
op
is
erate
lo
the
en
northoing
The
ligh
in
t
:
is
}
then
0;
as
}
follo
is
ws
an
in
is
default
es
case
east
Neq
in
&
nexto
o
nexto
&
ho
eq
that
:
ligh
{
w
nextSock
h
:=
k
1;
to
nexto
south
:=
from
1;
ligh
}
is
No
case
&
&
ense
nextSock
:
:=
{
&
nexto
nexto
:=
:=
0;
:=
nexteq
Finally
:=
ligh
0;
hed
ifSo
there
nextSock
request
:=
c
0;
When
}
input
}
w
This
o
sa
t
ys
request
that
Eeq
if
o
a
1;
north
:
request
0;
is
9
latc
w
hed
er
and
if
the
south
north
t
ligh
on
t
e
is
switc
not
the
green
c
and
o
there
is
is
prev
no
t
east
and
request
tra
then
colliding
switc
south
h
t
on
de
the
similar
north
default
ligh
Seq
t
o
and
eq
set
{
the
:=
lo
nexto
c
1;
k
So
n
ense
ect
{
w
:=
e
nexteq
giv
0;
e
nextSock
priorit
0;
y
}
to
,
the
east
east
t
tra
switc
If
on
the
er
north
is
ligh
east
t
and
is
lo
on
k
and
o
there
the
is
sense
no
go
more
o
north
e
tra
h
switc
the
h
ligh
o
and
the
the
ligh
bit
t
case
clear
&
the
&
request
:
and
:=
switc
Eo
h
ense
o
{
the
:=
lo
nexteq
c
0;
k
Note