Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
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-APDR, is tightly integrated with an existing word-level IC3/PDR framework APDR. 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-APDR can outperform state-of-the-art Constrained Horn Clause (CHC) solvers, including those that implement bit-level IC3/PDR. We also show that SyGuS-APDR and these CHC solvers can solve many instances not solved by other leading hardware model checkers that are not CHC-based. As a by-product of our work, we provide a translator Btor2CHC that enables use of CHC solvers for general hardware model checking problems, and contribute representative bit-vector benchmarks to the CHC-solver community.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. Wilcox University of Washington
|Unbounded Procedure Summaries from Bounded Environments|
Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton UniversityMedia Attached
|Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking|
Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton UniversityMedia Attached