分割統治法たよる形式的機能検証のためのインタフェイスプロトコルに対するアサーショハンの分割

摘要

本稿では，デイジタルシステム設計のRT (Register Transfer)レベルにおいて，BCA (Bus Cycle Accurate) レベルでのインタフェースプロトコルに対するアサーション群をコンポーネント単位のアサーション群に分割し，それを用いて各コンポーネントの形式的な機能検証を行う方法を提案する．本手法により，段階的設計における検証をコンポーネント単位の分割統治法により行うための，各コンポーネントに対するインタフェイスプロトコルの制約が得られる．提案手法では，コンポーネントの入出力関係に着目し，アサーション群を分割する．例題について本手法を適用し，コンポーネント単位でのインタフェイスプロトコルの制約に対して，満たすべき性質が検証可能であることが確認できた．