著者
森岡 澄夫 佐藤 証
出版者
一般社団法人情報処理学会
雑誌
情報処理学会論文誌 (ISSN:18827764)
巻号頁・発行日
vol.44, no.5, pp.1321-1328, 2003-05-15
被引用文献数
21 8

次期米国標準の128ビット共通鍵ブロック暗号AESにおいて,論理設計の工夫によって回路の消費電力を減らす方法を検討した.今回筆者らが行った調査では,AESの消費電力の大半をS-Boxと呼ばれる非線形変換を行う組合せ回路が占めており,S-Boxの消費電力は回路中を伝播するダイナミックハザードの量で決まる.本稿では,消費電力の少ないS-Boxの論理回路構成法(multi-stage PPRM)を提案する.その方法では,合成体上で演算を行うことによって回路規模を減らすとともに,二段論理を何ステージか直列につなげることによって,各ゲートへの信号到達時間を揃えハザード発生を減らす.この結果,これまで知られているS-Box回路と比べて半分から3分の1以下の消費電力を達成した.本手法は,S-Boxにガロア体の逆元演算を用いたその他多くの共通鍵暗号回路にも有効である.Reducing the power consumption of AES circuits is a critical problem when the circuits are used in low power embedded systems.We found the S-Boxes consume much of the total AES circuit power and the power for an S-Box is mostly determined by the number of dynamic hazards.In this paper,we propose a low-power S-Box circuit architecture: a multi-stage PPRM architecture.In this S-Box, (i) arithmetic operations are peformed over a composite field in order to reduce the total circuit size,and (ii) each arithmetic operation over sub-fields of the composite field is implemented as PPRM logic (AND-XOR logic) in order to reduce the generation and propagation of dynamic hazards.Low power consumptions of 29uW at 10\,MHz using 0.13um 1.5V CMOS technology were achieved,while the consumptions of the conventional S-Boxes are two or more times larger.The proposed method is effective in the other common-key ciphers whose S-Boxes use Galois field inversion.
著者
北道 淳司 森岡 澄夫 東野 輝夫 谷口 健一
雑誌
全国大会講演論文集
巻号頁・発行日
vol.47, pp.123-124, 1993-09-27

ハードウェア記述言語では,複数の動作の並列実行を自然に記述できるものが多い.しかし,複数の動作が同じレジスタ,バス,端子等に異なるデータを転送する(データ代入の衝突)かどうかを判断することは難しい.高信頼という観点からは,データ代入の衝突が起きないことを保証し,その記述から高位合成することが望ましい.本論文では,2.において,同期式順序回路を対象とし,複数動作が実行される順序回路の一モデルを示し,そのモデル上でのデータ代入の衝突を定義する,3.において,衝突が起きないことを検証するアルゴリズムを与える.
著者
森岡 澄夫 柴田 直樹 東野 輝夫 谷口 健一
出版者
一般社団法人電子情報通信学会
雑誌
電子情報通信学会技術研究報告. VLD, VLSI設計技術
巻号頁・発行日
vol.96, no.299, pp.49-56, 1996-10-18
被引用文献数
5

加算器, 乗算器, ALUなど, 算術演算を行う組み合わせ論理回路が, そのワードレベル仕様F (整数上の論理式として書かれた入出力関係の記述) を正しく実現している事を, プレスブルガー文真偽判定手続きを用いて自動証明する方法と, 証明例について述べる. 証明は, いわゆるビットレベル検証 (各回路モジュールM_jごと, そのワードレベル仕様F_jがゲートレベルで正しく実現されていることの証明) とワードレベル検証 (各M_jの接続関係および各ワードレベル仕様F_jのもとで, Fが満たされることの証明) に分けて行う. 乗算など, プレスブルガー算術で直接扱えない演算を行う回路についても, その演算に関して数学的に成り立つ性質等を仮定することにより, 証明できる場合がある. 本手法の特徴は, 幾つかの工夫を行ったプレスブルガー真偽判定ルーチンを用いることにより, 各モジュールの演算ビット長 n が増えても, 回路中のモジュールの数や組合せ方が同じで, かつ仕様記述のサイズが n 依存していなければ, ワードレベル検証にかかる時間がほとんど増加しないことである. 例えば n ビット乗算器から 2n ビット乗算器を構成した場合のワードレベル検証を, 2分程度のCPU時間で行えた. ビットレベル検証についても, 演算ビット長が4ビット程度であれば, 例えば加減算・論理演算を行うALU (74382) について6分程度のCPU時間で行えた.
著者
北嶋 暁 森岡 澄夫 島谷 肇 東野 輝夫 谷口 健一
出版者
一般社団法人電子情報通信学会
雑誌
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ (ISSN:09151915)
巻号頁・発行日
vol.79, no.12, pp.1017-1029, 1996-12-25
参考文献数
15
被引用文献数
4

教育用CPU KUE-CHIP2を,各命令の意味を記述した要求仕様からRTレベルまで段階的に設計し,それをSFL記述に自動変換してハードウェア合成系パルテノンを用いて回路を得た.そして,その設計が正しいことを代数的手法に基づいた証明支援系を用いて完全に自動で証明した.自動で証明できた理由は,CPUでは,要求仕様も含め,各レベルの仕様が共通の基本関数(算術・論理演算,メモリの入出力)を用いて記述できる,CPUの正しさの証明では1命令ごとに正しく動作することを調べればよく,かつ1命令の実行では繰返しループを含まない,また,我々の開発した証明支援系では,項書換え,場合分け,整数上の論理式の恒真性判定などを一定の手順で自動実行する,扱う式の大きさが増大するのに対処した工夫をしている,などである.証明作業は,記述誤りに伴う再証明も含め2週間程度で行えた.CPUの命令数が増えても証明のための計算時間はそれに比例する程度ですむので,本実験の結果より,単一制御部をもつ非パイプラインCPUについては,本論文の手法により,その正しさの証明を,現実的な時間で自動で行うことが可能であると言える.