抄録

○西村俊二・久我守弘・飯田全広・尼崎太樹・末吉敏則（熊本大）

一般に遅延依存(Delay Sensitive)の非同期回路は遅延非依存(Delay Insensitive, DI)の非同期回路と比べて設計・検証のコストが高いが，得られる回路はスピードと回路面積において優れる．本稿では遅延依存回路の検証コストを下げるべく，これまで不可能であった網羅的な検証を可能とする形式検証手法を提案する．提案の検証手法は様相論理の一種である多重様相論理に基づいており，回路中のある信号がゲートを通る前と通った後を別の世界として扱うことで遅延の抽象化を行っている．この検証手法を用いた例として遅延依存のFIFOの検証を行い，どのようなタイミング制約の下でFIFOとしての動作が可能となるのかを明らかにする．