Document

4.2.6 2分決定グラフに基づく記号モ
デル検査

2.
3.
4.
BDDにおける論理演算
fp =fp
Sp = S – Sp
fp q =fp  fq
Sp q = Sp Sq
fpq =fp  fq
Sp  q = Sp  Sq
fEXq(x1,x2)=
Exist(N(x1,x2,x1’,x2’)fq(x1’,x2’), {x1’,x2’})
BDDにおける論理演算 AND

記法
f(V) = f(x1, …, xi-1, xi, xi+1, …)
 f(V)|xi=0 = f(x1, …, xi-1, 0, xi+1, …)
 f(V)|xi=1 = f(x1, …, xi-1, 1, xi+1, …)


シャノン展開
f(V) = xi f(V)|xi=0  xi f(V)|xi=1
BDDにおける論理演算 AND
f(V) = xi f(V)|xi=0  xi f(V)|xi=1
xi
f(V)|xi=0
f(V) g(V) =
f(V)|xi=1
xi (f(V)|xi=0 g(V)|xi=0)  (xi g(V)|xi=1 g(V)|xi=1)
BDDにおける論理演算 AND
f(V)
xi
f(V)|xi=0
f(V) g(V)
f(V)|xi=1
xi
f(V)|xi=0g(V)|xi=0
f(V)|xi=1g(V)|xi=1
g(V)
xi
g(V)|xi=0
AND
g(V)|xi=1
再帰的に求めることができる
BDDにおける論理演算 AND
AND
0
AND
0
1
{ if (f = 0 or g = 0) return 0;
if (f = 1) return g;
if (g = 1) return f;
…
BDDにおける論理演算 AND
x1x2
x1  x3
x1
x1
x1x2 x1  x3
x1
x1
x2
x2
x2
x3
0
1
x1
0
1
x3
0
1
BDDにおける論理演算 OR
OR
1
OR
1
0
{ if (f = 1 or g = 1) return 1;
if (f = 0) return g;
if (g = 0) return f;
…
BDDにおける論理演算 OR
x1x2 x1  x3
x1x2 x1  x3
x1
x1
x2
x2
x2
x3
x3
0
x1
x1
x1
1
0
1
BDDにおける論理演算 Exist
E
Exist(f(x1, x2, x3), {x2})
:= g(x1, x3) = 1  f(x1, x3) = 1 for some x2
x1x2  x3
x1x2  x3
x1
x1
x1
x2
x2
x3
0
Eに含まれる
変数はORを
とって消す
x3
1
0
1
BDDにおける論理演算 Not
x1x2  x3
x1x2  x3
x1
x1
x1
x2
x2
x2
x3
x3
x3
0
(x1x2  x3)
1
0
1
4.2.7 SMVによる適用例アービタ
override in 0
grant out
req in5
e5
ack out5
req in4
e4
ack out4
req in3
e3
ack out3
req in2
e2
ack out2
req in1
e1
ack out1
token in
override
out
grant in
トークン
override in 0
grant out
req in5
1
e5
ack out5
req in4
1
e4
ack out4
req in3
1
e3
ack out3
req in2
1
e2
ack out2
req in1
1
e1
ack out1
token in
override
out
grant in
アービターセル
トークンリング方式
override in 0
req in5
grant out
e5
ack out5
e4
ack out4
req in3
e3
ack out3
req in2
e2
ack out2
req in1
e1
ack out1
req in4
1
token in
override
out
grant in
アービタセルの
記述
MODULE arbiter-cell(above,below,init-token)
VAR
Persistent : boolean;
Token : boolean;
Request : boolean;
ASSIGN
init(Token) := init-token;
next(Token) := token-in;
init(Persistent) := 0;
next(Persistent) := Request & (Persistent | Token);
DEFINE
above.token-in := Token;
override-out := above.override-out | (Persistent & Token);
grant-out := !Request & below.grant-out;
ack-out := Request & (Persistent & Token | below.grant-out);
アービタ全体の記述
req in5
req in4
req in3
req in2
req in1
override in
0
e5
e4
e3
e2
e1
token in override
out
grant out
ack out5
ack out4
ack out3
ack out2
ack out1
grant
in
MODULE main
VAR
e5 : arbiter-cell(self,e4,0);
e4 : arbiter-cell(e5,e3,0);
e3 : arbiter-cell(e4,e2,0);
e2 : arbiter-cell(e3,e1,0);
e1 : arbiter-cell(e2,self,1);
DEFINE
e1.token-in := token-in;
override-out := 0;
grant-out := !e1.override-out;
CTL式の記述 1

どの二つのack-outも同時に1とならない
MODULE main
…
SPEC
AG (
!(e1.ack-out &
& !(e1.ack-out
& !(e1.ack-out
& !(e1.ack-out
& !(e2.ack-out
& !(e2.ack-out
& !(e2.ack-out
& !(e3.ack-out
& !(e3.ack-out
& !(e4.ack-out
)
e2.ack-out)
& e3.ack-out)
& e4.ack-out)
& e5.ack-out)
& e3.ack-out)
& e4.ack-out)
& e5.ack-out)
& e4.ack-out)
& e5.ack-out)
& e5.ack-out)
CTL式の記述 2

Requestが１となれば，いつか必ずack-outが
1となる
MODULE arbiter-cell(above,below,init-token)
…
SPEC
AG(Request -> AF(ack-out))
SPEC
AG(Request -> AF(Request -> ack-out))
SPEC
AG(Request -> !EG(Request & !ack-out))

Download Report