Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model

• GHAREHBAGHI Amir Masoud

  VLSI Design and Education Center (VDEC), The University of Tokyo

• FUJITA Masahiro

  VLSI Design and Education Center (VDEC), The University of Tokyo

抄録

This paper presents a method for automatic rectification of design bugs in processors. Given a golden sequential instruction-set architecture model of a processor and its erroneous detailed cycle-accurate model at the micro-architecture level, we perform symbolic simulation and property checking combined with concrete simulation iteratively to detect the buggy location and its corresponding fix. We have used the truth-table model of the function that is required for correction, which is a very general model. Moreover, we do not represent the truth-table explicitly in the design. We use, instead, only the required minterms, which are obtained from the output of our backend formal engine. This way, we avoid adding any new variable for representing the truth-table. Therefore, our correction model is scalable to the number of inputs of the truth-table that could grow exponentially. We have shown the effectiveness of our method on a complex out-of-order superscalar processor supporting atomic execution of instructions. Our method reduces the model size for correction by 6.0x and total correction time by 12.6x, on average, compared to our previous work.

収録刊行物

• IEICE Transactions on Information and Systems

  IEICE Transactions on Information and Systems E97.D (4), 852-863, 2014

  一般社団法人 電子情報通信学会

キーワード

• design error diagnosis
• design error correction
• micro architecture debugging
• formal verification
• processors

詳細情報

• CRID: 1390282679354463616
• NII論文ID: 130003394911
• DOI: 10.1587/transinf.e97.d.852
• ISSN: 17451361
• ISSN: 09168532
• Web Site: https://www.jstage.jst.go.jp/article/transinf/E97.D/4/E97.D_852/_pdf
• 本文言語コード: en
• データソース種別:
  • JaLC
  • Crossref
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可