Art

J-GLOBAL ID：200902278373395137   Reference number：09A0383443

Checker Generation of Assertions with Local Variables for Model Checking

モデルチェッキングのための局所変数によるアサーションのチェッカ生成

Author (3)： TAKEUCHI Sho (Osaka Univ.) ,  HAMAGUCHI Kiyoharu (Osaka Univ.) ,  KASHIWABARA Toshinobu (Osaka Univ.)
Material： IPSJ Transactions on System LSI Design Methodology (Web)  (情報処理学会論文誌トランザクション System LSI Design Methodology(Web))
Volume： 2  Page： 80-92 (J-STAGE)  Publication year： 2009 
JST Material Number： U0110A  ISSN： 1882-6687  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： ENGLISH (EN)

Thesaurus term： *hardware design ,  variable of state ,  *finite automaton ,  computer algorithm ,  syntax ,  semantics ,  hardware description language ,  delay circuit ,  FIFO ,  memory capacity ,  constraint condition(restriction) ,  *model checking ,  programming language ,  storage control
Semi thesaurus term： Verilog ,  アサーション【プログラミング言語】 ,  model verification ,  formal verification

JST classification (2)： Computer system development  (JD02010R) ,  CAD,CAM  (JE10000A)

Reference (14)：

• 1) IEEE Std 1800-2005: IEEE Standard for SystemVerilog — Unified Hardware Design, Specification, and Verification Language, IEEE Computer Society (2005).
• 2) Property Specification Language (PSL). http://www.mel.nist.gov/psl/
• 3) Clarke, Jr., E.M., Grumberg, O. and Peled, D.A.: Model Checking, The MIT Press (1999).
• 4) McMillan, K.L.: Symbolic Model Checking, Kluwer Academic Publishers (1993). Some Complexity Results for System Verilog Assertions, Computer-Aided Verification, LNCS 4144, pp.205-218 (2007).
• 5) Foster, H., Krolnik, A. and Lacey, D.: Assertion-based Design, 2nd Ed., Springer (2004).

Terms in the title (3)： モデルチェッキング ,  アサーション ,  チェッカ