TY - GEN
T1 - Symbolic Trajectory Evaluation
T2 - 12th Conference on Formal Methods in Computer-Aided Design, FMCAD 2012
AU - Kirankumar, V. M.Achutha
AU - Gupta, Aarti
AU - Ghughal, Rajnish
PY - 2012
Y1 - 2012
N2 - Formal Verification (FV) is widely acknowledged for improving validation effectiveness. Usually formal verification has been used to supplement more traditional coverage oriented testing activities. Arithmetic Data-path FV has matured over the time to completely replace traditional dynamic validation methodologies. Moreover, it gives an additional promise of 100% data-space coverage. Symbolic Trajectory Evaluation (STE) is the best proven method of FV on Intel® data-path designs. The Floating Point Units (FPUs) are generally very data-path intensive. In the next generation Intel Processor Graphics design, the FPU was completely re-architected and this necessitated a methodology which could guarantee complete verification in a tight verification schedule. STE was brought in to meet this formidable target. This paper discusses the efficient application of this methodology to achieve convincing results. More than 201 bugs were caught in a very short verification cycle using STE.
AB - Formal Verification (FV) is widely acknowledged for improving validation effectiveness. Usually formal verification has been used to supplement more traditional coverage oriented testing activities. Arithmetic Data-path FV has matured over the time to completely replace traditional dynamic validation methodologies. Moreover, it gives an additional promise of 100% data-space coverage. Symbolic Trajectory Evaluation (STE) is the best proven method of FV on Intel® data-path designs. The Floating Point Units (FPUs) are generally very data-path intensive. In the next generation Intel Processor Graphics design, the FPU was completely re-architected and this necessitated a methodology which could guarantee complete verification in a tight verification schedule. STE was brought in to meet this formidable target. This paper discusses the efficient application of this methodology to achieve convincing results. More than 201 bugs were caught in a very short verification cycle using STE.
UR - http://www.scopus.com/inward/record.url?scp=84874730645&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84874730645&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84874730645
SN - 9781467348324
T3 - 2012 Formal Methods in Computer-Aided Design, FMCAD 2012
SP - 149
EP - 156
BT - 2012 Formal Methods in Computer-Aided Design, FMCAD 2012
Y2 - 22 October 2012 through 25 October 2012
ER -