Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)
Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Vijay Ganesh
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.
BibTeX
@article{Lu_Chien_Lee_Ganesh_2025, title={Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)}, volume={39}, url={https://ojs.aaai.org/index.php/AAAI/article/view/35275}, DOI={10.1609/aaai.v39i28.35275}, abstractNote={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.}, number={28}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Lu, Zhengyang and Chien, Po-Chun and Lee, Nian-Ze and Ganesh, Vijay}, year={2025}, month={Apr.}, pages={29426-29427} }