Parallel Logic Design Verification Based on Module Dependence

基于模块依赖的并行逻辑设计验证

• 批准号: 18500043
• 负责人: HIRAISHI Hiromi
• 金额: $ 2.29万
• 依托单位: Kyoto Sangyo University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18500043/
• 关键词: 設計検証; モデル検査; モジュール分割; 共有二分決定グラフ; 並列アルゴリズム; 遷移関係

形式的論理設計検証手法として記号モデル検査を取り上げ、モジュールの依存関係や内部の制御構造に着目して変数順を決めるアルゴリズムを提案し、これにより効率を数倍から数百倍向上出来ることを示した。また、分割した遷移関係を用いるアルゴリズムの中で、値が変化しない変数を早期に削除することにより、数倍から数十倍の効率向上が得られることを示した。さらに、並列論理関数処理として動的並列化法を提案し、その有効性も示した。

The formal logic design verification method and the symbolic object inspection are used to determine the dependencies of objects and the internal control structure, and the efficiency of this system is several times to hundreds of times higher. In addition, the number of times the number of times In addition, parallel logic processing and dynamic parallel transformation method are proposed, and there is no need to show it.

项目成果

SATアルゴリズムを利用した記号モデル検査について

关于使用 SAT 算法进行符号模型检查

• 发表时间: 2008
• 作者: Hironori Washizaki;Satoru Takano;Yoshiaki Fukazawa;Yoichi Tomioka;富岡洋一;Yoichi Tomioka;平石裕実;平石 裕実;平石裕実
• 通讯作者: 平石裕実

記号モデル検査器SMVにおけるBDDの変数順について

关于符号模型检查器SMV中BDD的变量顺序

• 发表时间: 2009
• 作者: Hironori Washizaki;Satoru Takano;Yoshiaki Fukazawa;Yoichi Tomioka;富岡洋一;Yoichi Tomioka;平石裕実
• 通讯作者: 平石裕実