ZBDDとpartial order reductionに基づく非同期式回路検証方式について  [in Japanese] Verification of Asynchronous Circuits based on ZBDD and Partial Order Reduction  [in Japanese]

非同期式回路は,クロックを用いず,信号遷移の因果関係により動作する.そのため設計検証においては,各信号線が状態を持つと考える必要があることから,同期式と比較して本質的に状態数が多く,爆発的に増大する傾向にある.本研究では,トレース理論に基づく非同期式回路の検証において,ZBDDを用いたシンボリックな状態探索に,検証に不必要な状態の生成を抑えるpartial order reducitonを組み合わせる事を提案する.また,実際にいくつかの非同期式回路の検証を行なう.

Asynchronous circuits works based on causal relationship between signal transitions. However, state spaces of asynchtronous circuits are huge, because every wire has states. Thus, formal verification of asynchronous circuits is more difficult than that of synchronous ones. In this paper, we propose combining symbolic state traversal based on ZBDD with partial order reduction, which generates reduced global state spaces, for trace theoretic verification of asytnchronous circuits. We also demonstrate the verification of several asynchronous circuits.