Computer Science Engineering
Resume:
THE INSTITUTE OF ELECTRONICS, TECHNICAL REPORT OF IEICE.
INFORMATION AND COMMUNICATION ENGINEERS
E-mail: *********@***.*.*-*****.**.**
1
[8]
A Hardware Acceleration for Semi-Formal Model Checking
Satoshi MORISHITA, Hiroaki YOSHIDA, and Masahiro FUJITA
Department of Electronics Engineering, Faculty of Engineering, University of Tokyo
7-3-1 Hongo, Bunkyo-ku, Tokyo, 113-8656 Japan
VLSI Design and Education Center, University of Tokyo
2-11-16 Yayoi, Bunkyo-ku, Tokyo, 113-0032 Japan
E-mail: *********@***.*.*-*****.**.**
Abstract The veri cation becomes important now as the design becomes complex and large-scale.
Model checking which is one of the most important veri cation has been held back by the state ex-
plosion problem, which is the problem that the number of states grows exponentially in the number of
system components. So we propose an e cient model checking method in this paper. We have enhanced
a semi-formal bounded model checking [8] by using a hardware accelerator and modi ed the codes to
be easily implemented on a hardware. The experimental results with some examples show that the
proposed method can execute model checking in short time.
Key words Model Checking
1.
1. 1
LSI 3 4
LSI
1
1. 2
1. 2. 1
(Model Checking) [1] (FSM:Finite State Machine) (Temporal Logic) FSM 1
(Ex- 1
plicit) (Implicit)
FSM
SPIN [2] FSM
[3]
FSM
(BDD:Binary Decision Diagram) [4]
(SAT )
BDD SMV [3]
SAT NuSMV [5]
(BMC:Bounded
Model Checking) [6] 0, 1, 3
1 0, 1
{0, 1} {0, 0}
SPIN NuSMV {0, }
1. 2. 2 5 AND {0, 1, 1, 1, 1}
0
1 0
[8] 1 0
{0,,,, }
BDD [4]
2
1 (MULT32-10 )
1 6 b it_ in_ x
16 A
out
XO R
14 %
16 B 24 %
1 6 b it_ in_ y
17 %
2 MULT32-n
44 %
{1, -, 1, - } {1, -, 0, 0 }
{0, -, 1, - }
(1, 0, 0, 1 )
{0, 0, 0, 1 } {0, -, 1, - } (a )
(c)
(b )
1 0
1 0
1. 3
3 BDD
1. LSI
BDD [4] BDD
BDD
1. 2. 2
3 BDD
(a) BDD (b) BDD
(c) 3
BDD
2.
2. 1
(a) 4
BDD
BDD
(a c d) d
1 0
0
2 2 16 2
BDD
n
BDD (b = 1)
0 2
BDD
0 MULT32-n
(a) (b)
MULT32-10
ITE BDD
10
(a) ITE
CPU Core 2 Duo T7200
(b) ITE
(2.0GHz) :2GB
(b) ITE
IBM Rational Quantify [7]
BDD
1 1
2. 3
2. 2
2. 2
2
3
3 2
a
Cube BDD
c
c
a b out
{ a, b, c, d } = {1, -, 0, 1 }
d d
d
a
u u
1 0 0
1 b
u u
0
1
a b
u u
a
u u
4 BDD
a.cube[n]
2 b.value
out.cube[n]
(MULT32-10 ) a.value
b.cube[n]
1 1.5
(a, b) out u
n 3
4 1
a b
b
out
4 {1, 1, 0, 0}
4 1 5
{0,,, } {1,,, 1}
1
1 1.5
5 n
n 1 4n
1
1
1 1
1 m
O(nm) {1,, 0, } (1, 1, 0, 0)
2. 4 HW/SW
{1, 0, 1, 0}
5
3
4
n
- m
n
6 HW/SW
#Input Vectors Per Communication
n
8 (MULT32-9 )
m
8 MULT32-9
6
(S )
(m /S ) S
1
-
3. FPGA PC
2.
FPGA
FPGA
FPGA Xilinx
Virtex-II Pro FPGA
UDP/IP
UDP/IP
6 S
UDP/IP
7
PowerPC Virtex-II Pro
1/S m
m
m /S m
MULT32-n MULT32-n
2n
m S
60%
5
4 MULT32 [ ] (
160
/ )
140
120
Runtime [sec]
100 5.7 1.0 5.7
MULT32-8
80 25.9 3.7 7.0
MULT32-9
60
122.5 16.5 7.4
MULT32-10
40
575.3 88.0 6.5
MULT32-11
20
6.7
0
1-10-100-**** 10000
#Input Vectors Per Communication
9 (MULT32-9 )
BDD
MULT32-9
FPGA
160
MULT32-9 26
-
-
UDP/IP
2. 4
MULT32-9 1
FPGA
32
S 32 S
6.7
MULT32-9
9 S
S
[1] E. M. Clarke, O. Grumberg, D. A. Peled, Model
S = 1 checking. MIT Press, 2000.
[2] G. J. Holzmann, The Model Checker SPIN, IEEE
Trans. on Software Engineering, vol.23, no.5, pp.279-
295, May 1997.
3.7 7 [3] K. L. McMillan, Symbolic model checking: an ap-
proach to the state explosion problem. Kluwer Aca-
demic Publishers, 1993.
MULT32
[4] R. E. Bryant, Graph-based algorithms for Boolean
function manipulation, IEEE Trans. Comput.,
vol.C-35, no.8, pp.677-691, Aug. 1986.
[5] A. Cimatti, E. M. Clarke, E. Giunchiglia, F.
Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani,
2 and A. Tacchella. NuSMV 2: An OpenSource Tool
for Symbolic Model Checking, In Proc. of the Inter-
4
national Conference on Computer Aided Veri cation,
pp.359-364, July 2002.
6.7 [6] A. Biere, A. Cimatti, E. M. Clarke and Y. Zhu,
Symbolic Model Checking without BDDs, in Tools
and Algorithms for the Construction and Analysis of
Systems, Lecture Notes In Computer Science 1579,
Springer-Verlag, pp.193-207, 1999.
4. [7] Rational Software Corporation, Quantify, 1999.
[8] J. D. Bingham and A. J. Hu, Semi-Formal Bounded
Model Checking, In Proc. of the 14th International
Conference on Computer Aided Veri cation 2002,
Lecture Notes In Computer Science 2404, Springer-
Verlag, pp.236-249, July 2002.
6
Contact this candidate