IEICE TRANSACTIONS on Information
Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model
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
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
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 -
English
