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

Amir Masoud GHAREHBAGHI; Masahiro FUJITA

doi:10.1587/transinf.E97.D.852

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

Amir Masoud GHAREHBAGHI, Masahiro FUJITA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E97-D No.4 pp.852-863

Publication Date: 2014/04/01

Publicized

Online ISSN: 1745-1361

DOI: 10.1587/transinf.E97.D.852

Type of Manuscript: PAPER

Category: Dependable Computing

Authors

Amir Masoud GHAREHBAGHI
The University of Tokyo
Masahiro FUJITA
The University of Tokyo

Keyword

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

Cite this

Copy

Amir Masoud GHAREHBAGHI, Masahiro FUJITA, "Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model" in IEICE TRANSACTIONS on Information, vol. E97-D, no. 4, pp. 852-863, April 2014, doi: 10.1587/transinf.E97.D.852.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E97.D.852/_p

Copy

@ARTICLE{e97-d_4_852,
author={Amir Masoud GHAREHBAGHI, Masahiro FUJITA, },
journal={IEICE TRANSACTIONS on Information},
title={Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model},
year={2014},
volume={E97-D},
number={4},
pages={852-863},
abstract={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.},
keywords={},
doi={10.1587/transinf.E97.D.852},
ISSN={1745-1361},
month={April},}

Copy

TY - JOUR
TI - Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model
T2 - IEICE TRANSACTIONS on Information
SP - 852
EP - 863
AU - Amir Masoud GHAREHBAGHI
AU - Masahiro FUJITA
PY - 2014
DO - 10.1587/transinf.E97.D.852
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E97-D
IS - 4
JA - IEICE TRANSACTIONS on Information
Y1 - April 2014
AB - 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.
ER -