Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

Hongce Zhang, Aarti Gupta, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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- 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 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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Proceedings
EditorsFritz Henglein, Sharon Shoham, Yakir Vizel
PublisherSpringer Science and Business Media Deutschland GmbH
Pages325-349
Number of pages25
ISBN (Print)9783030670665
DOIs
StatePublished - 2021
Event22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 - Copenhagen, Denmark
Duration: Jan 17 2021Jan 19 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12597 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021
CountryDenmark
CityCopenhagen
Period1/17/211/19/21

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • Bit-vector theory
  • CHC solver
  • Hardware model checking
  • Lemma generation
  • Syntax-guided synthesis (SyGuS)

Fingerprint Dive into the research topics of 'Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking'. Together they form a unique fingerprint.

Cite this