平成20年度 VDEC論理CAD基礎技術セミナー
（ＲＴＬと上位設計に対する形式的検証技術)


〜ご連絡 (2008/5/2)〜
開催日が7月23日, 24日に決定しました。
参加申し込みを開始致しました。

本セミナーの目的・概要

　従来からC言語ベース設計や高位設計手法に関して、数多くのセミナーやチュートリアルが開催されてきています。しかし、当該技術が新規のものであり、かつ現在も研究が鋭意進められている分野であることから、簡潔な技術的講義の後、

「まずは、ちょっと使って、体験してみる」

ことを通して、具体的にどのようなものであるか、また自分の使っている設計手法との親和性などについての直感的理解が大切であると考えます。そして、結果的に、

「自分の要求に沿ったツールが実現できるか、自分で考えてみる」

ことができるようになれば、ツールに惑わされることもなく、効率的な設計ができると考えます。また、将来ＣＡＤツールに関する研究開発を行う上での基盤技術の習得も目指しています。

　そこで、最小限の講義による理解を元に、実際に各種高位設計ツールを実際に体験できるセミナーを企画しました。大学院学生・社会人の両方を対象として構成しており、前提知識は従来のLSI設計手法の基本だけで理解できるものとします。

　今回は特に、ＲＴＬや上位設計における形式的検証に関係する基盤技術についてセミナーを開催します。 　本セミナーでは、主に、形式的検証で広く用いられている論理式を扱う技術の理解と習得のため、パブリックドメインツールを用いた演習を行います。セミナーは、２日間で構成されており、下記の内容の講義と実際のツールを使った演習から構成されています。 　演習では、実際にツールを使ってみることに重点が置かれています。C言語設計や高位設計の話しはよく聞くが、実際に使うということがどういうことかがはっきりしないと感じておられる方に最適です。

開催日

2008年 7月23日(水)、24日(木) (2日間、受講参加日の指定可)
変更後の日程が確定次第、掲載します。

講習会日程

7月23日(水)　高位設計・検証
10:00-12:00 レジスタ転送レベルより上位の設計合成・検証技術の基本の解説、ならびに関連研究動向、およびツール開発状況について講義形式で説明する。また、24日に行うＳＡＴ技術やモデル検査技術の基礎や動向についても合せて解説する。
（講師： VDEC 藤田昌宏 教授）
12:00-13:30 昼食
13:30-16:30 上位設計では、従来のビットレベルでの検証とは異なる、整数やビットベクターを対象として効率的な検証が行われている。この演習では、算術演算を含む論理式の真偽判定ツールCVC3とCプログラム検証のための限定モデル検査器CBMCの使用法や実際の検証を体験する。
（担当： VDEC 教職員）

7月24日(木) SAT問題・モデル検査
10:00-12:00 近年、劇的に性能向上している論理関数の充足可能性判定(SAT)ツールの使い方について、いくつかの問題に応用しながら演習形式で体得する。また最近注目されているQSAT問題やMAXSAT問題についても、演習を通して実際に判定ツールを体験することで理解を深める。
（講師： VDEC 教職員）
12:00-13:30 昼食
13:30-16:30 パブリックなモデル検査器であるNuSMVについて、入力となるモデル記述とプロパティについて説明し、演習を通してツールの使い方や出力に対する解釈について学習する。
（担当： VDEC 所属研究室の大学院生）

開催場所

東京大学武田先端知ビル (本郷キャンパス浅野地区)、1階セミナー室
アクセス方法へのリンク

参加対象

一般 (ＲＴＬや高位設計における形式的検証技術に興味のある社会人、教育機関在籍の教職員、学生)

定員・参加費

40名程度、参加費無料 (当日配布する資料をもとに演習を行います。)

申込方法

申し込みページをご参照下さい。 (申し込みページへ)

問合せ先

企画運営　：　名倉 徹 　
E-mail：nakura＠vdec.u-tokyo.ac.jp

申込受付　：　吉澤 真吾　
E-mail：seminar＠vdec.u-tokyo.ac.jp
VDEC Homepage