Hardware Verification with respect to Program Specification

程序规范的硬件验证

• 批准号: 14580377
• 负责人: KIMURA Shinji
• 金额: $ 1.86万
• 依托单位: Waseda University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 2004
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14580377/
• 关键词: High-level Design Verification; C based Hardware Design; Reconfigurable Hardware; Verification of Arithmetic Circuits; Equivalence Verification; Uninterpreted Function; 設計検証; 高位検証; 再構成可能素子の検証; テクノロジーマッピング検証; 映像処理向け検証; 再構成可能アーキテクチャ検証; マルチメディア処理

With the recent development of integrated circuit technology, we can integrate 1 million transistors in one chip. For the design of such huge circuits, high-level design methodologies have been developed and applied to many application specific chips. In the high-level design, programming languages are used to describe the functionality and the description is automatically converted to hardware modules based on high-level synthesis algorithms. So the modification and verification should be done at programming level and high-level verification methods are needed. In this research, we have developed several basic algorithms to show the correctness of hardware modules with respect to the program specification.At first, we have surveyed the current research on the equality with uninterpreted function and its application to software and hardware verification. We have also checked the current equality systems such as SVC, CLVL, etc. We have applied these systems for the verification of arith … More metic circuits and shown the limitation of such systems. We have also applied the equality checking systems for the verification of parallel and pipeline circuits.In the equality checking, the algorithm uses logic formulae to represent and decide the equality. For the acceleration of the decision procedure, we proposed a prototyping system based on new look-up-table architecture of Field Programmable Gate Array. We have devised the architecture and proposed a mapping method for the new architecture. The architecture is more area-efficient and faster compared to the usual loop-up-table architecture.For the program specification, we have proposed a control-data-flow graph based data-path optimization methods. Especially, we focused on the bit-width of data-paths and proposed an optimization method of integer operations and an error estimation method for floating point operations. With the optimization and estimation algorithms, we can verify application specific circuits written in C programs.We have also worked on the high-level test and proposed a test pattern compaction method with small area overhead for system-on-chip design. Less

随着集成电路技术的发展，我们可以在一块芯片上集成一百万个晶体管。为了设计如此庞大的电路，高级设计方法已经被开发出来，并应用于许多特定的应用芯片。在高级设计中，采用编程语言对功能进行描述，并基于高级综合算法将描述自动转换为硬件模块。因此，修改和验证应在编程层面进行，并需要高层次的验证方法。在本研究中，我们开发了几种基本算法来显示硬件模块相对于程序规范的正确性。本文首先综述了未解释函数等式的研究现状及其在软硬件验证中的应用。我们也检查了现有的平等系统，如SVC， CLVL等。我们已经将这些系统应用于仿真电路的验证，并指出了这些系统的局限性。我们还将等式校验系统应用于并联电路和管路电路的验证。在等式检验中，算法使用逻辑公式来表示和确定等式。为了加快决策过程，提出了一种基于现场可编程门阵列新查表架构的原型系统。我们设计了体系结构，并提出了新体系结构的映射方法。与通常的循环上表体系结构相比，该体系结构具有更高的面积效率和更快的速度。针对程序规范，提出了一种基于控制数据流图的数据路径优化方法。重点研究了数据路径的位宽问题，提出了整数运算的优化方法和浮点运算的误差估计方法。通过优化和估计算法，我们可以验证用C程序编写的特定应用电路。我们还进行了高级测试，并提出了一种用于片上系统设计的小面积开销的测试模式压缩方法。少

项目成果

An Optimization Method in Floating-point to Fixed-point Conversion using Positive and Negative Error Analysis and Sharing of Operations

一种利用正负误差分析和运算共享的浮点到定点转换的优化方法

• 发表时间: 2004
• 期刊: Proc.of Workshop on Synthesis and System Integration of Mixed Technologies (SASIMI'2004)
• 作者: N.Doi;T.Horiyama;M.Nakanishi;S.Kimura
• 通讯作者: S.Kimura

中村, 中西, 堀山, 鈴木, 木村, 渡邉: "環境適応可能なリアルタイム視線推定LSIの設計と評価"第15回 回路とシステム(軽井沢)ワークショップ. 293-298 (2002)

Nakamura、Nakanishi、Horiyama、Suzuki、Kimura、Watanabe：“环境自适应实时注视估计 LSI 的设计和评估”第 15 届电路与系统（轻井泽）研讨会 293-298（2002 年）。

非線形計画法と整数解の探索に基づく高位合成向けビット長最適化

基于非线性规划和整数解搜索的高级综合位长优化

• 发表时间: 2005
• 期刊: 情報処理学会システムLSI設計技術研究会報告
• 作者: 土井伸洋;堀山貴志;中西正樹;木村晋二
• 通讯作者: 木村晋二

Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High Level Synthesis

用于高级综合的浮点到定点转换的小数部分的位长度优化

• 发表时间: 2003
• 期刊: IEICE Trans.Fundamentals E86-A, No.12
• 作者: N.Doi;T.Horiyama;N.Nakanishi;S.Kimura;K.Watanabe
• 通讯作者: K.Watanabe

A Hybrid Dictionary Test Data Compression for Multiscan-based Designs

基于多重扫描的设计的混合字典测试数据压缩

• 发表时间: 2004
• 期刊: IEICE Trans.Fundamentals E87-A, No.12
• 作者: Y.Shi;S.Kimura;M.Yanagisawa;T.Ohtsuki
• 通讯作者: T.Ohtsuki