データパスを含む非同期式回路の検証について  [in Japanese] Verification of asynchronous circuits including data-paths  [in Japanese]

従来の検証方式で, データパスを含む非同期式回路の形式的検証を行う際には, データパスの抽象化を行うのが一般的である.データパスを抽象化せずに検証を行うためには, データパスが取りうるすべての値の組合せ, 遷移系列について状態探索を行うことが必要となるので, 仕様記述が困難で, また検証時の状態が爆発的に増加する欠点がある.本研究では, 従来の欠点を解消するために, データパスを特定あるいはランダム値を用いて部分的に, 制御系を形式的に検証する手法を提案する.提案する手法を検証器に実装し, いくつかのデータパスを含む非同期式回路を検証した.その実験結果より提案する手法が有効であることを確認した.

When we want to verify asynchronous circuit including data-paths, we usually do the abstraction of the circuit to remove most of those data-paths.This is because verifying the circuit without abstraction requires to check the whole data values that the data-paths take, and this makes it too difficult to describe specifications and traverse its huge state space.In this paper, we propose to verify data-paths partially using some specific or random values with verifying the control parts formally as usual.This allows us to do the verification of a given circuit without abstraction which still gives us rather reliable results.We have implemented the proposed method, and verified several asynchronous circuits including data-paths.