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
N1 - This work was supported in part by the DARPA POSH program. REFERENCES [Andraus 04] Andraus, A. A., and K. Sakallah, “Automatic abstraction and verification of verilog models,” Proc. DAC, 2004. [Bayazit 05] Bayazit, A. A., and S. Malik, “Complementary use of runtimevalidationandmodelchecking,”Proc.ICCAD, 2005. [Campbell 19] Campbell, K., et al., “Hybrid Quick Error Detection: Validation and Debug of SoCs Through High-Level Synthesis,” IEEETrans.CAD, 2019. [Cascaval 10] Cascaval, C., et al., “A taxonomy of accelerator architectures and their programming models,” IBM Journal of ResearchandDevelopment, 2010. [Chi 19] Chi, Y., et al., “Rapid Cycle-Accurate Simulator for High-LevelSynthesis,”Proc.Intl.Symp.FPGAs, 2019. [Clarke 01] Clarke, E., et al., “Bounded Model Checking using SatisfiabilitySolving,”FormalMethodsinSystemDesign, 2001. [Cong 12] Cong, J., et al., “Architecture support for accelerator-rich CMPs,”Proc.DAC, 2012. [Cong 17] Cong, J., et al., “Bandwidth Optimization Through On-ChipMemoryRestructuringforHLS,”Proc.DAC, 2017. [Cota 15] Cota, E. G., et al., “An Analysis of Accelerator Coupling in HeterogeneousArchitectures,”Proc.DAC, 2015. [Fadiheh 18] Fadiheh, M. R., et al., “Symbolic quick error detection using symbolic initial state for pre-silicon verification,” Proc. DATE, 2018. [Fadiheh 19] Fadiheh, M. R., et al., “Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking,” Proc.DATE, 2019. [Foster 15] Foster, H. D., “Trends in Functional Verification: A 2014 Industry Study,”Proc.DAC, 2015. [Hara 09] Hara, Y., et al., “Proposal and Quantitative Analysis of the CHStone Benchmark Program Suite for Practical C-based High-level Synthesis,”JournalofInformationProcessing, 2009. [Huang 18] Huang, B-Y., et al., “Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification,” ACM Trans. Design Automation of Electronic Systems, 2019. [Jones 96] Jones, R., C-J. H. Seger and D. L. Dill, “Self-ConsistencyChecking,”Proc.FMCAD, 1996. [Keller 76] Keller, R.M., “Formal Verification of Parallel Programs,”Communs.of ACM, 1976. [Lin 15] Lin, D., et al., “A Structured Approach to Post-Silicon Validation and Debug Using Symbolic Quick Error Detection,” Proc.IEEEIntl.TestConf., 2015. [Patel 08] Patel, S., and W. Hwu, “Accelerator Architectures,” IEEE Micro, 2008. [Reid 16] Reid, A., et al., “End-to-end verification of processors withISA-Formal,”Proc.Computer-AidedVerification, 2016. [RESULTS 20] https://github.com/upscale-project/aqed-dac2020-results [Sen 05] Sen, K., et al., “CUTE: a concolic unit testing engine for C,”ACMSIGSOFTSoftwareEngineeringNotes, 2005. [Singh 18] Singh, E., et al., “Logic Bug Detection and Localization Using Symbolic Quick Error Detection,” IEEE Trans. CAD, 2018. [Singh 19] Singh, E., et al., “Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study,” Proc.DATE, 2019. [Zhou 18] Zhou, Y., et al., “Rosetta: A Realistic High-Level Synthesis Benchmark Suite for Software Programmable FPGAs,” Proc.Intl.Symp.FPGAs, 2018.
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 - https://www.scopus.com/pages/publications/85093982543
UR - https://www.scopus.com/pages/publications/85093982543#tab=citedBy
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 -