Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)
Abstract
We build the first machine-learning-based algorithm selection tool for hardware verification described in the Btor2 format. In addition to hardware verifiers, our tool also selects from a set of software verifiers to solve a given Btor2 instance, enabled by a Btor2-to-C translator. We propose two embeddings for a Btor2 instance, Bag of Keywords and Bit-Width Aggregation. Pairwise classifiers are applied for algorithm selection. Upon evaluation, our tool Btor2-Select solves 30.0% more instances and reduces PAR-2 by 50.2%, compared to the PDR implementation in the HWMCC'20 winner model checker AVR. Measured by the Shapley values, the software verifiers collectively contributed 27.2% to Btor2-Select's performance.
Cite
Text
Lu et al. "Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)." AAAI Conference on Artificial Intelligence, 2025. doi:10.1609/AAAI.V39I28.35275Markdown
[Lu et al. "Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)." AAAI Conference on Artificial Intelligence, 2025.](https://mlanthology.org/aaai/2025/lu2025aaai-algorithm/) doi:10.1609/AAAI.V39I28.35275BibTeX
@inproceedings{lu2025aaai-algorithm,
title = {{Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)}},
author = {Lu, Zhengyang and Chien, Po-Chun and Lee, Nian-Ze and Ganesh, Vijay},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2025},
pages = {29426-29427},
doi = {10.1609/AAAI.V39I28.35275},
url = {https://mlanthology.org/aaai/2025/lu2025aaai-algorithm/}
}