Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

In Verification, Model Checking, and Abstract Interpretation

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

Hongce Zhang
Hongce Zhang
Assistant Professor in Microelectronics Thrust

My research interest is on hardware formal verification.