多値非同期式回路の形式的検証に関する研究  [in Japanese] Verification of Asynchronous Circuits based on Multiple-Valued Logic  [in Japanese]

非同期式回路はクロックを用いず、信号遷移の因果関係により動作を行なうため、同期式より高速化、低電力化が可能であると言われている。非同期式回路は2本の信号線を用いて1ビットのデータを表す2線2相方式を用いて実現されることが多いが、多値論理を用いて単線式で実現しようという提案もある。そこで本研究では、多値論理を用いた非同期式回路の形式的検証の方法を提案する。検証には既存の非同期式回路検証ツールを用いた。多値論理素子の動作をペトリネットを用いてモデル化し、既存のツールを拡張することにより多値論理非同期式回路の検証を可能とした。

Since asynchronous circuits work based on causality relation between signals without global clocks, it is said that they can enjoy better performance and lower power consumption than synchronous circuits. Asynchronous circuits are often designed based on 2-rail coding. Such designs are usually implemented by using two wires for each signal, but single wire implementation based on multi-valued logics is also proposed. In this work, we focus on formal verification of asynchronous circuits implemented by B-ternary Logic. We propose how to model the B-ternary logic elements with Petri net and how to expand an existing verification tool such that it can handle circuits which consist of those B-ternary logic elements.