权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

VLSI搭載電子機器設計への形式的手法の適用による設計生産性並びに設計再利用性向上技術に関する研究

通过将形式化方法应用于配备VLSI的电子设备的设计来提高设计生产力和设计可重用性的技术研究

基本信息

批准号：
04F04350
负责人：
SAKUNKONCHAK Thanyapat (2006)
金额：
$ 1.54万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2004
资助国家：
日本
起止时间：
2004 至 2006
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-04F04350/
关键词：
システムLSI 形式的検証技術同期検証 SpecC言語

项目摘要

VLSIを搭載した電子機器の設計においては、設計生産性を向上させるために、設計工程のできるだけ早い段階で、設計誤りを発見・修正することが重要である。その実現手段の1つとして、テストパタンに依存しない検証ができる形式的検証の適用が有効であると考えられる。本研究では、主に、システムレベルでの設計を対象に、形式的検証の適用によって、網羅的な検証を行い、設計のやり直しを防ぐことを目的の1つとしている。対象とする設計記述は、Cベースのシステム設計言語であるSpecC言語で記述された並列プロセスを含むものである。検証手法は、反例に基づいた設計抽象化改良技術を利用している。この手法では、検証が成功した場合には、設計誤りがないことが証明される。検証が失敗した場合であっても、設計に誤りがない可能性があり、記述の抽象化を改良して検証を繰り返す必要がある。2006年度は、2005年度までに構築した同期検証フレームワークをベースとして、SpecC言語で記述されたシステムの同期検証を完全に行うことができるツールを目指し、実際にシステムレベル設計に利用可能なレベルに近いツールを開発した。同時平行的に、上記フレームワークに必要なabstraction refinementなどの要素技術についての改良・新規提案も行った。

Design of VLSI mounted electronic machines, design productivity, design engineering, design error detection, correction, etc. The application of the method of realization depends on the form of examination. This study focuses on the design of objects, forms and applications of evidence in the design of objects, forms and applications. For example, the design description of the C language is included in the description of the C language The method of proof is based on the design of abstract improvement technology. The method is correct, the proof is successful, the design is wrong, and the proof is correct. Failure of verification, design error, possibility, description, improvement, verification, necessity In 2006 and 2005, the construction of the synchronization test system was completed, and the specification C language was used to describe the synchronization test system. At the same time, the parallel, the above note, the necessary abstraction refinement, the elements of technology, the improvement of the new proposal, the implementation of the new proposal

项目成果

期刊论文数量（4）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Synchronization Verification in System-Level Design with ILP Solver

使用 ILP 求解器进行系统级设计的同步验证

DOI：
发表时间：
2005
期刊：
ACM-IEEE International Conference on Formal Methods and Mod els for Codesign (MEMOCODE 2005) 2005
影响因子：
0
作者：
Thanyapat Sakunkonchak;Satoshi Komatsu;Masahiro Fujita
通讯作者：
Masahiro Fujita

線形計画法を利用したシステムレベル設計での動作並列化前後での等価性検証手法

线性规划系统级设计中操作并行化前后的等价验证方法