Skip to main content

Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

Author(s): Zhang, Hongce; Gupta, Aarti; Malik, Sharad

To refer to this page use:
Abstract: In this work we propose to use Syntax-Guided Synthesis (SyGuS) for lemma generation in a word-level IC3/PDR framework for bit-vector problems. Hardware model checking is moving from bit-level to word-level problems, and it is expected that model checkers can benefit when such high-level information is available. However, for bit-vectors, it is challenging to find a good word-level interpolation strategy for lemma generation, which hinders the use of word-level IC3/PDR algorithms. Our SyGuS-based procedure, SyGuS- 𝖯𝖣𝖱 , is tightly integrated with an existing word-level IC3/PDR framework 𝖯𝖣𝖱 . It includes a predefined grammar template and term production rules for generating candidate lemmas, and does not rely on any extra human inputs. Our experiments on benchmarks from the hardware model checking competition show that SyGuS- 𝖯𝖣𝖱 can outperform state-of-the-art Constrained Horn Clause (CHC) solvers, including those that implement bit-level IC3/PDR. We also show that SyGuS- 𝖯𝖣𝖱 and these CHC solvers can solve many instances faster than other leading word-level hardware model checkers that are not CHC-based. As a by-product of our work, we provide a translator Btor2CHC that enables the use of CHC solvers for general hardware model checking problems, and contribute representative bit-vector benchmarks to the CHC-solver community.
Publication Date: 2021
Citation: Zhang, Hongce, Aarti Gupta, and Sharad Malik. "Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking." In International Conference on Verification, Model Checking, and Abstract Interpretation (2021): pp. 325-349. doi:10.1007/978-3-030-67067-2_15
DOI: 10.1007/978-3-030-67067-2_15
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 325 - 349
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Verification, Model Checking, and Abstract Interpretation
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.