Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. Chattopadhyay, S., Lonsing, F., Piccolboni, L., Soni, D., Wei, P., Zhang, X., Zhou, Y., Carloni, L., Chen, D., Cong, J., Karri, R., Zhang, Z., Trippel, C., Barrett, C., & Mitra, S. arXiv:2108.06081 [cs], August, 2021. arXiv: 2108.06081![Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper abstract bibtex Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED${\textasciicircum}2$). A-QED${\textasciicircum}2$ systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED${\textasciicircum}2$; in particular, if the full HA under verification contains a bug, then A-QED${\textasciicircum}2$ ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED${\textasciicircum}2$.
@article{chattopadhyay_scaling_2021,
title = {Scaling {Up} {Hardware} {Accelerator} {Verification} using {A}-{QED} with {Functional} {Decomposition}},
url = {http://arxiv.org/abs/2108.06081},
abstract = {Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED\${\textasciicircum}2\$). A-QED\${\textasciicircum}2\$ systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED\${\textasciicircum}2\$; in particular, if the full HA under verification contains a bug, then A-QED\${\textasciicircum}2\$ ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED\${\textasciicircum}2\$.},
urldate = {2021-09-27},
journal = {arXiv:2108.06081 [cs]},
author = {Chattopadhyay, Saranyu and Lonsing, Florian and Piccolboni, Luca and Soni, Deepraj and Wei, Peng and Zhang, Xiaofan and Zhou, Yuan and Carloni, Luca and Chen, Deming and Cong, Jason and Karri, Ramesh and Zhang, Zhiru and Trippel, Caroline and Barrett, Clark and Mitra, Subhasish},
month = aug,
year = {2021},
note = {arXiv: 2108.06081},
keywords = {Computer Science - Logic in Computer Science},
}
Downloads: 0
{"_id":"zjHMKRfZyBFwenmfB","bibbaseid":"chattopadhyay-lonsing-piccolboni-soni-wei-zhang-zhou-carloni-etal-scalinguphardwareacceleratorverificationusingaqedwithfunctionaldecomposition-2021","author_short":["Chattopadhyay, S.","Lonsing, F.","Piccolboni, L.","Soni, D.","Wei, P.","Zhang, X.","Zhou, Y.","Carloni, L.","Chen, D.","Cong, J.","Karri, R.","Zhang, Z.","Trippel, C.","Barrett, C.","Mitra, S."],"bibdata":{"bibtype":"article","type":"article","title":"Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition","url":"http://arxiv.org/abs/2108.06081","abstract":"Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED${\\textasciicircum}2$). A-QED${\\textasciicircum}2$ systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED${\\textasciicircum}2$; in particular, if the full HA under verification contains a bug, then A-QED${\\textasciicircum}2$ ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED${\\textasciicircum}2$.","urldate":"2021-09-27","journal":"arXiv:2108.06081 [cs]","author":[{"propositions":[],"lastnames":["Chattopadhyay"],"firstnames":["Saranyu"],"suffixes":[]},{"propositions":[],"lastnames":["Lonsing"],"firstnames":["Florian"],"suffixes":[]},{"propositions":[],"lastnames":["Piccolboni"],"firstnames":["Luca"],"suffixes":[]},{"propositions":[],"lastnames":["Soni"],"firstnames":["Deepraj"],"suffixes":[]},{"propositions":[],"lastnames":["Wei"],"firstnames":["Peng"],"suffixes":[]},{"propositions":[],"lastnames":["Zhang"],"firstnames":["Xiaofan"],"suffixes":[]},{"propositions":[],"lastnames":["Zhou"],"firstnames":["Yuan"],"suffixes":[]},{"propositions":[],"lastnames":["Carloni"],"firstnames":["Luca"],"suffixes":[]},{"propositions":[],"lastnames":["Chen"],"firstnames":["Deming"],"suffixes":[]},{"propositions":[],"lastnames":["Cong"],"firstnames":["Jason"],"suffixes":[]},{"propositions":[],"lastnames":["Karri"],"firstnames":["Ramesh"],"suffixes":[]},{"propositions":[],"lastnames":["Zhang"],"firstnames":["Zhiru"],"suffixes":[]},{"propositions":[],"lastnames":["Trippel"],"firstnames":["Caroline"],"suffixes":[]},{"propositions":[],"lastnames":["Barrett"],"firstnames":["Clark"],"suffixes":[]},{"propositions":[],"lastnames":["Mitra"],"firstnames":["Subhasish"],"suffixes":[]}],"month":"August","year":"2021","note":"arXiv: 2108.06081","keywords":"Computer Science - Logic in Computer Science","bibtex":"@article{chattopadhyay_scaling_2021,\n\ttitle = {Scaling {Up} {Hardware} {Accelerator} {Verification} using {A}-{QED} with {Functional} {Decomposition}},\n\turl = {http://arxiv.org/abs/2108.06081},\n\tabstract = {Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED\\${\\textasciicircum}2\\$). A-QED\\${\\textasciicircum}2\\$ systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED\\${\\textasciicircum}2\\$; in particular, if the full HA under verification contains a bug, then A-QED\\${\\textasciicircum}2\\$ ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED\\${\\textasciicircum}2\\$.},\n\turldate = {2021-09-27},\n\tjournal = {arXiv:2108.06081 [cs]},\n\tauthor = {Chattopadhyay, Saranyu and Lonsing, Florian and Piccolboni, Luca and Soni, Deepraj and Wei, Peng and Zhang, Xiaofan and Zhou, Yuan and Carloni, Luca and Chen, Deming and Cong, Jason and Karri, Ramesh and Zhang, Zhiru and Trippel, Caroline and Barrett, Clark and Mitra, Subhasish},\n\tmonth = aug,\n\tyear = {2021},\n\tnote = {arXiv: 2108.06081},\n\tkeywords = {Computer Science - Logic in Computer Science},\n}\n\n","author_short":["Chattopadhyay, S.","Lonsing, F.","Piccolboni, L.","Soni, D.","Wei, P.","Zhang, X.","Zhou, Y.","Carloni, L.","Chen, D.","Cong, J.","Karri, R.","Zhang, Z.","Trippel, C.","Barrett, C.","Mitra, S."],"key":"chattopadhyay_scaling_2021","id":"chattopadhyay_scaling_2021","bibbaseid":"chattopadhyay-lonsing-piccolboni-soni-wei-zhang-zhou-carloni-etal-scalinguphardwareacceleratorverificationusingaqedwithfunctionaldecomposition-2021","role":"author","urls":{"Paper":"http://arxiv.org/abs/2108.06081"},"keyword":["Computer Science - Logic in Computer Science"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"article","biburl":"https://bibbase.org/zotero/bxt101","dataSources":["Wsv2bQ4jPuc7qme8R"],"keywords":["computer science - logic in computer science"],"search_terms":["scaling","hardware","accelerator","verification","using","qed","functional","decomposition","chattopadhyay","lonsing","piccolboni","soni","wei","zhang","zhou","carloni","chen","cong","karri","zhang","trippel","barrett","mitra"],"title":"Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition","year":2021}