A-QED verification of hardware accelerators

Eshan Singh; Florian Lonsing; Saranyu Chattopadhyay; Maxwell Strange; Peng Wei; Xiaofan Zhang; Yuan Zhou; Deming Chen; Jason Cong; Priyanka Raina; Zhiru Zhang; Clark Barrett; Subhasish Mitra

doi:10.1109/DAC18072.2020.9218715

A-QED verification of hardware accelerators

Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Maxwell Strange, Peng Wei, Xiaofan Zhang, Yuan Zhou, Deming Chen, Jason Cong, Priyanka Raina, Zhiru Zhang, Clark Barrett, Subhasish Mitra

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking - however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

Original language	English (US)
Title of host publication	2020 57th ACM/IEEE Design Automation Conference, DAC 2020
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9781450367257
DOIs	https://doi.org/10.1109/DAC18072.2020.9218715
State	Published - Jul 2020
Event	57th ACM/IEEE Design Automation Conference, DAC 2020 - Virtual, San Francisco, United States Duration: Jul 20 2020 → Jul 24 2020

Publication series

Name	Proceedings - Design Automation Conference
Volume	2020-July
ISSN (Print)	0738-100X

Conference

Conference	57th ACM/IEEE Design Automation Conference, DAC 2020
Country/Territory	United States
City	Virtual, San Francisco
Period	7/20/20 → 7/24/20

Keywords

Accelerators
Bounded Model Checking
Formal verification
Pre-silicon verification
QED
Quick Error Detection

ASJC Scopus subject areas

Computer Science Applications
Control and Systems Engineering
Electrical and Electronic Engineering
Modeling and Simulation

Online availability

10.1109/DAC18072.2020.9218715

Library availability

Discover UIUC Full Text

Cite this

Singh, E., Lonsing, F., Chattopadhyay, S., Strange, M., Wei, P., Zhang, X., Zhou, Y., Chen, D., Cong, J., Raina, P., Zhang, Z., Barrett, C., & Mitra, S. (2020). A-QED verification of hardware accelerators. In 2020 57th ACM/IEEE Design Automation Conference, DAC 2020 Article 9218715 (Proceedings - Design Automation Conference; Vol. 2020-July). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DAC18072.2020.9218715

A-QED verification of hardware accelerators. / Singh, Eshan; Lonsing, Florian; Chattopadhyay, Saranyu et al.
2020 57th ACM/IEEE Design Automation Conference, DAC 2020. Institute of Electrical and Electronics Engineers Inc., 2020. 9218715 (Proceedings - Design Automation Conference; Vol. 2020-July).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Singh, E, Lonsing, F, Chattopadhyay, S, Strange, M, Wei, P, Zhang, X, Zhou, Y, Chen, D, Cong, J, Raina, P, Zhang, Z, Barrett, C & Mitra, S 2020, A-QED verification of hardware accelerators. in 2020 57th ACM/IEEE Design Automation Conference, DAC 2020., 9218715, Proceedings - Design Automation Conference, vol. 2020-July, Institute of Electrical and Electronics Engineers Inc., 57th ACM/IEEE Design Automation Conference, DAC 2020, Virtual, San Francisco, United States, 7/20/20. https://doi.org/10.1109/DAC18072.2020.9218715

@inproceedings{2d2a9f76d7584c589f795b20c8db3b36,

title = "A-QED verification of hardware accelerators",

abstract = "We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking - however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).",

keywords = "Accelerators, Bounded Model Checking, Formal verification, Pre-silicon verification, QED, Quick Error Detection",

author = "Eshan Singh and Florian Lonsing and Saranyu Chattopadhyay and Maxwell Strange and Peng Wei and Xiaofan Zhang and Yuan Zhou and Deming Chen and Jason Cong and Priyanka Raina and Zhiru Zhang and Clark Barrett and Subhasish Mitra",

note = "Publisher Copyright: {\textcopyright} 2020 IEEE.; 57th ACM/IEEE Design Automation Conference, DAC 2020 ; Conference date: 20-07-2020 Through 24-07-2020",

year = "2020",

month = jul,

doi = "10.1109/DAC18072.2020.9218715",

language = "English (US)",

series = "Proceedings - Design Automation Conference",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

booktitle = "2020 57th ACM/IEEE Design Automation Conference, DAC 2020",

address = "United States",

}

TY - GEN

T1 - A-QED verification of hardware accelerators

AU - Singh, Eshan

AU - Lonsing, Florian

AU - Chattopadhyay, Saranyu

AU - Strange, Maxwell

AU - Wei, Peng

AU - Zhang, Xiaofan

AU - Zhou, Yuan

AU - Chen, Deming

AU - Cong, Jason

AU - Raina, Priyanka

AU - Zhang, Zhiru

AU - Barrett, Clark

AU - Mitra, Subhasish

PY - 2020/7

Y1 - 2020/7

N2 - We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking - however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

AB - We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking - however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

KW - Accelerators

KW - Bounded Model Checking

KW - Formal verification

KW - Pre-silicon verification

KW - QED

KW - Quick Error Detection

UR - http://www.scopus.com/inward/record.url?scp=85093982543&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85093982543&partnerID=8YFLogxK

U2 - 10.1109/DAC18072.2020.9218715

DO - 10.1109/DAC18072.2020.9218715

M3 - Conference contribution

AN - SCOPUS:85093982543

T3 - Proceedings - Design Automation Conference

BT - 2020 57th ACM/IEEE Design Automation Conference, DAC 2020

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 57th ACM/IEEE Design Automation Conference, DAC 2020

Y2 - 20 July 2020 through 24 July 2020

ER -

A-QED verification of hardware accelerators

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this