WEKO3
アイテム
論理シミュレーションをベースとしたプロセサ制御の効率的検証手法
https://ipsj.ixsq.nii.ac.jp/records/27984
https://ipsj.ixsq.nii.ac.jp/records/27984ca64335a-1606-401d-9f95-a3195fb5e013
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 1994 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | SIG Technical Reports(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 1994-10-27 | |||||||
タイトル | ||||||||
タイトル | 論理シミュレーションをベースとしたプロセサ制御の効率的検証手法 | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | Effective Verification Method for Processor Controls Based on Logic Simulation | |||||||
言語 | ||||||||
言語 | jpn | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
資源タイプ | technical report | |||||||
著者所属 | ||||||||
富士通研究所CAD研究部 | ||||||||
著者所属 | ||||||||
富士通研究所CAD研究部 | ||||||||
著者所属 | ||||||||
富士通研究所CAD研究部 | ||||||||
著者所属 | ||||||||
富士通研究所CAD研究部 | ||||||||
著者所属(英) | ||||||||
en | ||||||||
CAD Laboratory, Fujitsu Laboratories Ltd. | ||||||||
著者所属(英) | ||||||||
en | ||||||||
CAD Laboratory, Fujitsu Laboratories Ltd. | ||||||||
著者所属(英) | ||||||||
en | ||||||||
CAD Laboratory, Fujitsu Laboratories Ltd. | ||||||||
著者所属(英) | ||||||||
en | ||||||||
CAD Laboratory, Fujitsu Laboratories Ltd. | ||||||||
著者名 |
中田, 恒夫
× 中田, 恒夫
|
|||||||
著者名(英) |
Tsuneo, Nakata
× Tsuneo, Nakata
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 近年,論理シミュレーションを用いたプロセサの論理検証の高速化技術が次々と開発されているが,入力である検証プログラムの開発は,人手やランダム生成に頼っていた.我々は,この検証プログラムを自動生成する手法を開発した.本手法では,プロセサの数学的モデルとして有限状態マシンを考え,特定の制御に対する検証プログラム生成問題を,状態集合への到達可能性問題にマッピングした.検証したい制御に関する仕様を抽出しモデル化しているため,形式的検証で問題となる状態数の増加は緩やかである.本手法の下で,パイプライン制御やキャッシュ制御に対する検証プログラム自動生成を実現しているが,レジスタ転送レベルで記述されたハードウェアの検証データ生成にも適用可能である. | |||||||
論文抄録(英) | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | This paper presents an efficient verification method for processor controls using logic simulation. Currently, the verification program that is the input sequence for logic simulation, is developed mainly by hand or by weighted random generators. Our method uses a finite state machine as processor model. The problem of generating the verification program is then mapped into the reachability problem for the finite state machine, which can be solved efficiently by using BDD's. We have succeeded in applying this method to the pipeline control and cache control for microprocessors, and we hope it can also be expanded to the verification data generation for hardware systems in register transfer level. | |||||||
書誌レコードID | ||||||||
収録物識別子タイプ | NCID | |||||||
収録物識別子 | AA11451459 | |||||||
書誌情報 |
情報処理学会研究報告システムLSI設計技術(SLDM) 巻 1994, 号 93(1994-SLDM-072), p. 139-144, 発行日 1994-10-27 |
|||||||
Notice | ||||||||
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
出版者 | ||||||||
言語 | ja | |||||||
出版者 | 情報処理学会 |