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

プルーフチェッカーを用いた超並列演算器の設計検証

使用证明检查器验证大规模并行算术单元的设计

基本信息

批准号：
13780219
负责人：
和崎克己
金额：
$ 1.34万
依托单位：
Shinshu University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2001
资助国家：
日本
起止时间：
2001 至 2002
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13780219/
关键词：
形式検証系多ソート代数設計検証ハードウェア記述言語 FPGA

项目摘要

「ロジック」の問題に関して,演算回路を数学的定義に基づいて設計し,設計検証と動作の正しさをプルーフチェッカー(Proof Checker)を用いて証明する方策について検討した.回路を定義していくための数学的概念は,回路の構造として,回路内の全信号点を表す状態空間,入出力信号間の写像で定義される演算子,演算に必要な入力信号点を表す演算子から信号点への写像,および演算結果を表す演算子から出力信号点への写像,といった4つの空間と写像の対として定義する,多ソート代数構造を用いた.これは,従来のシミュレーション手法などで用いている,狭い条件下での演算子,信号線,遅延情報の組とは異なり,信号点の状態空間を0/1の値だけをとり得る2値空間だけでなく,ハイインピーダンス状態や連続空間など,様々な空間で回路を定義できることを示す.この構造を基に,入力信号により出力信号が一意に決定できる演算子を一つだけ持つような演算回路を定義した.この結果,演算子が当該回路の入出力信号点の間を写像する関数として正当か,結果が一意に定まる関数が存在するか,入力信号点の状態が変化した場合,演算結果が安定となるか,などの重要な性質が数学的に証明可能であることを示した.次に,演算回路の合成について定義する.合成後の回路は,上述の構造における各空間・写像の和をとったものであり,この合成回路に関しても,結果が一意に定まるか,演算結果が安定となるか,などの性質が証明可能となった.本研究の目標は,現在有力視されている代数計算モデルのうち,多ソート代数モデルを取り上げ,正当性の証明をプルーフチェッカーを用いることにある.更に,検証済みの計算モデルをVHDL(ハードウェア記述言語)などへ自動変換し,FPGA(Field Programmable Gate Array)などの試作用デバイスを用いて並列演算器の実装の行い,動作の検証を行う必要がある.それにより,設計検証方法による動作原理の違いを明確にし,信頼性の高い演算器実装に関する数理的手法を確立する.本年度は,次の2つの展開研究を並行して進めた.(1)計算モデルを基にした回路から,ゲートアレイ配置配線ソフトウェアによりターゲットデバイス用の配置配線情報を生成した。各プロセッサ要素には,計算モデル上で動作の正当性を検証済みの高速加算・減算器,並列配列型乗算器などを搭載している.これにより,動作時における動的再構成などが容易なマルチコンテクスト・ハードウェアの構成が可能となった(2)「多ソート代数モデル」による並列演算器の計算モデルを昨年度作成したが,この拡張として,高速演算性を実現するためのキャリー先見回路やキャリーモニタ回路を有した超高速加算器などの数学モデルを構築した。定義は数学的帰納法を用い,自然数Nのオーダーで計算モデルを作成した。その後、プルーフチェッカーで証明可能とした.

The problem of "Proof" is related to the definition of arithmetic loop mathematics, the design of design, the proof of design and the correction of action. The mathematical concept of loop definition is that all signal points in the loop represent the state space, the image between input and output signals is defined, the algorithm for calculating the necessary input signal points represents the image of signal points, and the algorithm results represent the image of signal points represents the image of output signals. The algorithm, signal line, delay information group, signal point state space 0/1 value group, signal point 2 value group, signal point state space 0/1 value group, signal point 2 value group, signal point 2 value group, signal point state space 0/1 value Based on this structure, the input signal and the output signal are determined in one sense, and the algorithm is defined in one sense. As a result, when the operator writes an image between the input and output signal points of the loop, the correlation number is valid, and the result is determined by the same meaning. When the state of the input signal point changes, the calculation result is stable. This shows that the important properties of the input signal point are mathematically provable. Secondly, the synthesis of computational circuits requires definition. After synthesis, the loop is opposite to the structure described above. The sum of each space and image is equal to the sum of each space and image. The synthetic loop is related to the sum of each space and image. The result is equal to the sum of each space and image. The calculation result is equal to the sum of each space and image. The purpose of this study is to present a powerful view of algebraic computation, multi-algebra, and justification. In addition, the verification of the calculation module VHDL(VHDL) to automatic conversion,FPGA(Field Programmable Gate Array) to test the role of the module to use the parallel algorithm in the implementation of the operation, the operation of the verification is necessary. In this paper, the design method of verification, the principle of operation and the mathematical method of reliability are established. This year, the second time to carry out research and parallel progress. (1)The calculation of the basic parameters of the loop, the configuration of the information generated High speed adder/subtracter, parallel arrangement type calculator, for verifying the correctness of the operation of each element. (2) Calculation of parallel calculators is easy to construct in the past year, and high speed calculation performance is realized in the past year. The definition of mathematical inclusion method is used, and the natural number N is calculated. After a while, he was able to prove that it was possible.