Synthesizing Environment Invariants for Modular Hardware Verification

Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik

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

6 Scopus citations


We automate synthesis of environment invariants for modular hardware verification in processors and application-specific accelerators, where functional equivalence is proved between a high-level specification and a low-level implementation. Invariants are generated and iteratively strengthened by reachability queries in a counterexample-guided abstraction refinement (CEGAR) loop. Within each iteration, we use a syntax-guided synthesis (SyGuS) technique for generating invariants, where we use novel grammars to capture high-level design insights and provide guidance in the search over candidate invariants. Our grammars explicitly capture the separation between control-related and data-related state variables in hardware designs to improve scalability of the enumerative search. We have implemented our SyGuS-based technique on top of an existing Constrained Horn Clause (CHC) solver and have developed a framework for hardware functional equivalence checking that can leverage other available tools and techniques for invariant generation. Our experiments show that our proposed SyGuS-based technique complements or outperforms existing property-directed reachability (PDR) techniques for invariant generation on practical hardware designs, including an AES block encryption accelerator, a Gaussian-Blur image processing accelerator and the PicoRV32 processor.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings
EditorsDirk Beyer, Damien Zufferey
Number of pages24
ISBN (Print)9783030393212
StatePublished - 2020
Event21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020 - New Orleans, United States
Duration: Jan 16 2020Jan 21 2020

Publication series

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


Conference21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020
Country/TerritoryUnited States
CityNew Orleans

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Synthesizing Environment Invariants for Modular Hardware Verification'. Together they form a unique fingerprint.

Cite this