Development of formal design methodology for VLSI datapaths based on Galois-field arithmetic operations

2016 Fiscal Year Final Research Report

• Project/Area Number: 25240006
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Computer system
• Research Institution: Tohoku University
• Principal Investigator: Homma Naofumi 東北大学, 電気通信研究所, 教授 (00343062)
• Co-Investigator(Kenkyū-buntansha): 青木 孝文 東北大学, 情報科学研究科, 教授 (80241529)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Keywords: 計算機システム / LSI設計技術 / ハードウェアセキュリティ

Outline of Final Research Achievements

This research project developed a formal design methodology for VLSI datapaths consisting of arithmetic operations on Galois fields. First, we provided (1) a formal description for Galois-field arithmetic circuits based on polynomial basis and normal basis which are frequently used for cryptography and error-correction code, and then developed (2) a formal verification method, which is applicable to the circuit description, using computer algebra. In addition, (3) we applied the design and verification methods to a cryptographic processor. More precisely, we designed a processor datapath for AES, which is one of the ISO/IEC international standard block ciphers, by the developed method. Furthermore, we developed an automatic generator for generating a variety of Galois-field arithmetic circuits depending on various design specification.

Free Research Field

計算機科学