モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法  [in Japanese] A Monitor Generation Method for Formal Monitor-based Verification Considering Input Constraints  [in Japanese]

Search this Article

Author(s)

Abstract

本論文では, ハードウェアインターフェース仕様全体をより包括的に検証することを目指し, 正規表現ベースの仕様記述言語からモニタ回路を生成する手法を示す.モニタ回路の生成は自動的に行われるため, 複雑な仕様に対するモニタ回路であっても人手で設計する場合に比べ, 誤りの混入を避けることができる.また, モジュール単位の検証の際, 通常では入力制約を付加する必要があるが, 本論文では仕様記述から, 入力制約を自動的に抽出して, モニタ回路に直接反映させる手法について述べる.実験では設計例としてバスプロトコルであるAMBA AHBに従って設計された回路を取り上げ, 実際に仕様を記述してモニタを生成し, 形式検証を行った結果を示す.

In order to verify hardware module interfaces, various verification methods have been proposed. This paper focuses on formal monitor-based verification of module interfaces. In our method, first, we describe specifications of module interfaces in a language based on regular expressions, then construct behavior models from the description. Finally, we generate a monitor circuit. When we verify module interfaces formally, some input constraints are usually required. We show how to generate monitors including input constraints automatically from specifications. In verification experiments, we show that modules that comply AMBA AHB bus protocol can be verified by monitors formally.

Journal

  • IEICE technical report

    IEICE technical report 105(354), 73-78, 2005-10-21

    The Institute of Electronics, Information and Communication Engineers

References:  6

Codes

  • NII Article ID (NAID)
    110003500121
  • NII NACSIS-CAT ID (NCID)
    AN10013006
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    7704907
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top