深さを保った順序回路の状態遷移の変更によるSequiential Depth計算の高速化

全文

(1)情報処理学会第67回全国大会. 4A-6. 深さを保った順序回路の状態遷移の変更による Sequential Depth 計算の高速化何虹†. 中村一博‡. 名古屋大学工学部. †. 高木一義‡. 高木直史‡. 名古屋大学大学院情報科学研究科. はじめに順序回路の動作の深さ (Sequential depth) を知ることは、回路の全ての動作で誤りがないことを検証する上で重要な問題である。Sequential depth を計算する方法として、順序回路の動作に対応する有限状態機械 (FSM) の全ての状態に対して、初期状態への遷移を追加し Sequential depth 計算を高速化する方法が提案されている [1]。本稿では、初期状態への遷移の追加を全ての状態に対して行うのではなく、選択的に行うことにより、 Sequential depth 計算を高速化する手法を提案する。. 1. 順序回路の Sequential Depth 計算 Sequential depth は、順序回路の動作に対応する FSM において、初期状態から最も遠い状態までの深さを表すものである。Sequential depth が求まると、その深さまでの動作を検証するだけで、全ての動作が保証される。定義 1 有限状態機械 M は M = (Q, Σ, ∆, δ, λ, q0 ) と定義される。ここで、Q は有限状態集合、Σ は入力アルファベット、∆ は出力アルファベット、δ は状態遷移関数 Q × Σ → Q、λ は出力関数 Q × Σ → ∆、q0 は初期状態 (q0 ∈ Q) である。 qi , qj ∈ Q について、qi から qj への連続した状態遷移を walk といい、状態遷移の数を walk の長さという。通る状態が全て異なる walk を path という。また FSM の状態 qi と qj の最短の path の長さを qi と qj の距離といい、d(qi , qj ) で表す。特に FSM の初期状態 q0 からある状態 q への距離 d(q0 , q) を状態 q の深さという。定義 2 Sequential depth は次のように定義される。 maxq∈Q d(q0 , q) 定義 3 状態遷移関係関数 T を以下のように定義する。   1 if qi+1 = δ(qi , a), qi , qi+1 ∈ Q, T (qi , a, qi+1 ) = a∈Σ  0 otherwise. 2. 定義 4 walkk (qi , qj ) を以下のように定義する。 walk1 (qi , qj ) = ∃aT (qi , a, qj ) walkk (qi , qj ) = ∃qi+1 ∃qi+2 . . . ∃qi+(k−1) walk1 (qi , qi+1 ) · walk1 (qi+1 , qi+2 ) . . . walk1 (qi+(k−1) , qj ) 定義 5 pathk (qi , qj ) を以下のように定義する。 path1 (qi , qj ) = ∃aT (qi , a, qj ) · (qi 6= qi+1 ) pathk (qi , qj ) = ∃qi+1 ∃qi+2 . . . ∃qi+(k−1) path1 (qi+1 , qi+2 ). ∗ Efficient Sequential Depth Computation with State Transition Modifications † Hong He, School of Engineering, Nagoya University ‡ Kazuhiro Nakamura, Kazuyoshi Takagi, and Naofumi Takagi, Graduate School of Information Science, Nagoya University. ‡. . . . path1 (qi+(k−1) , qj ){(qi+2 6= qi )} · {(qi+3 6= qi ) · (qi+3 6= qi+1 )} . . . {(qj 6= qi ) . . . (qj 6= qi+(k−2) )} 定義 6 depthk (q0 , q) を以下のように定義する。ここで、I(q) は q が初期状態なら１を返す関数である。 depthk (q0 , q) = I(q0 ) · pathk (q0 , q). · ¬pathk−1 (q0 , q) . . . ¬path1 (q0 , q). (1). Sequential depth は、式 (1) の充足可能性判定を繰り返すことにより求められる [1]。k = 1 における式 (1) の充足可能性判定から始め、式 (1) が充足可能である間 k の値をインクリメントし、式 (1) が充足可能である最大の k の値を求める。この値が Sequential depth である。充足可能性判定は SAT-solver を用いて行う。全ての状態から初期状態への遷移を加えた Sequential Depth 計算 FSM の全ての状態に対して初期状態への遷移を追加すると、式 (1) の充足可能性判定はよりシンプルな式 (2) の充足可能性判定に置き換えられる [1]。. 3. depthk (q0 , q) = I(q0 ) · pathk (q0 , q) · ¬walkk−1 (q0 , q) (2) 式 (2) の充足可能性判定は、次の式 (3), (4) の充足可能性判定に分けて行われる。. I(q0 ) · pathk (q0 , q). I(q0 ) · walkk−1 (q0 , q). (3) (4). 式 (3) の充足可能性判定を行い、式 (3) を満たす q に対して、式 (4) の充足可能性判定を行う。式 (4) が充足不可能ならば、式 (2) は充足可能と判定される。式 (4) が充足可能ならば、q 以外の解を再び式 (3) で求め、式 (4) の判定を行う。式 (3) を満たす全ての q に対して式 (4) が充足可能ならば、式 (2) は充足不可能と判定される。深さを保った状態遷移の変更による Sequential depth 計算本研究では、全ての状態に対して初期状態への遷移を追加する状態遷移の変更 [1] のみでなく、Sequential depth の変わらない種々の変更を用いる計算手法を提案する。提案手法は、初期状態への遷移のみが異なる複数の FSM の状態遷移関数を用い、それらを順番に切り替えながら式 (3), (4) の充足可能性判定を行う。図１に、提案手法で用いる Sequential depth の変わらない変更を行った種々の FSM の例を示す。(a) は変更前の元の FSM、(b) は初期状態に対してのみ初期状態. 4. 1−11.

(2) 表 1 ISCAS 回路の Sequential depth 計算の結果. 00/0. 00. 10. 01/0 00,01/0 01. (a) 00/0. 00. 01. 00. 00,01/1. 01 00/1. 00,01/0 (b) 1-. 00/0. 01/0 00,01/0 01. 01/1 (d). 図1. 10. 01/1. 00,01/1 11 00/1. (c) 1-. 100. 00/0. 01/0 00,01/0. 1-. 11. 01/1. 00/1. 1-. 10. 01/0. s298 s641 s713 s953 s967 s1269 s1423 s3271 s3330 s3384 s4863. 11. 01/1. 1-. Circuit R. 100. 10 00,01/1. 1-. 00/0. 01/0 00,01/0 01. 11 00/1. I. 00,01/1. 01/1. 1-. 10 00,01/1. 14 19 19 29 29 37 74 116 132 183 104. 3 35 35 16 16 18 17 26 40 43 49. ours [sec] 105.78 150.10 172.28 190.65 214.27 3600(10) 3600(38) 3600(14) 3600(8) 3600(12) 3600(4). original Sequential [1][sec] Depth 100.98 18 157.40 6 200.51 6 218.24 10 256.59 10 3600(9) 3600(10) 3600(14) 3600(6) 3600(11) 3600(4) -. 実験結果提案手法と従来手法 [1] を C 言語を用いて実装し、SunBlade2000 (CPU1.2GHz, UltraSPARCIII Cu, メモリ 2048MB) 上で実験を行った。SAT-solver には zchaff(version:2003.7.1)[3] を使用した。表 1 に 11 個の ISCAS89 ベンチマーク回路に対して Sequential depth 計算を行った結果を示す。N = 4 とした。R は状態変数の数、I は入力変数の数である。ours, original はそれぞれ、提案手法、従来手法を用いた計算に要した時間である。Sequential depth が求まらなければ、3600 秒の制限で到達した深さを () で示す。求まった場合はその値を Sequential depth に示す。この結果から、Sequential depth が求まった 5 つの回路のうち 4 つの回路に対して、提案手法が従来手法より高速であることが分かる。他の 6 つの回路のうち、4 つの回路に対しては、提案手法が従来手法より深くまで計算できた。残りの回路に対しては、提案手法は従来の手法と同じ深さまで計算できた。特に s1423 においては、従来手法が 3600 秒で 10 までに対して、提案手法が深さ 38 まで計算できた。. 5. 11 00/1. (e). 初期状態への遷移を加えた種々の FSM. へ遷移を加えた FSM[2]、(c) は状態変数列のうち、左側の変数が 0 である状態のみから初期状態へ遷移を加えた FSM、(d) は右側の状態変数が 0 である状態のみから初期状態へ遷移を加えた FSM である。(e) は全ての状態に対して初期状態へ遷移を加えた FSM である [1]。図１の各状態遷移には入力/出力がラベル付けされており、ラベル 1-は追加された状態遷移にラベル付けれた新しい状態初期化用の入力シンボルである。00 は初期状態である。(a) の FSM の Sequential depth は 2 であり、 (b), (c), (d), (e) の Sequential depth も 2 である。式 (3), (4) の充足可能性判定の繰り返しにより求まる Sequential depth は、(b), (c), (d), (e) のどの変更法を用いても同じであるが、充足可能性判定問題を解く SATsolver の特性のため、どれを用いるかによって Sequential depth 計算に要する時間は変化する。また、SAT-solver により得られる充足可能解が複数ある場合、どの変更法を用いるかによって、式 (3), (4) の繰り返し計算において得られる充足可能解の順序が異なる。場合によっては繰り返しが速く終了し、計算が速く進む可能性がある。一般に、Sequential depth の変わらない状態遷移の変更は無数に考えられる。我々は変更の種類を FSM の状態変数の数 n に対して n + 2 通りに限定し、それらのうち N 種類を順次切り替えながら計算を行うヒューリスティックな手法を提案する。n + 2 通りの変更として、 [1], [2] の変更に加え、n 個の状態変数のうちある 1 個の変数を除いた他の n − 1 個の全ての変数の値が 0 であるという状態に対してのみ初期状態への遷移を追加するという、ある 1 個の変数の取り方によって n 通りある変更を用いる。これらの変更法から得られる n + 2 種類の FSM の状態遷移関係関数を、毎回切り替えながら、式 (3), (4) の充足可能性判定を行う。. まとめ本稿では、複数の選択的な状態の初期化により得られる深さが同じ FSM を切り替えながら Sequential depth を計算する手法を提案した。今後は、この選択的初期化法の自由度を高め、より効率的な手法について考える。. 6. 参考文献 [1] Maheer Mneimneh and Karem Sakallah, “SATbased Sequential Depth Computation,” Proc. of ASP-DAC’03, 2003.. [2] 高畠亮, “順序回路の初期状態への遷移を加えた Sequential depth 計算の高速化”, 名古屋大学工学部電気電子情報工学科情報コース卒業研究報告, 2004. [3] M.Moskewicz, C.Madigan, Y.Zhao, L.Zhang, S.Malik, “Chaff:Engineering an Efficient SAT solver,” Proc. of 37th DAC,2000.. 1−12.

(3)