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

Abstract

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
PublisherSpringer
Pages202-225
Number of pages24
ISBN (Print)9783030393212
DOIs
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

Conference

Conference21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020
CountryUnited States
CityNew Orleans
Period1/16/201/21/20

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., & Malik, S. (2020). Synthesizing Environment Invariants for Modular Hardware Verification. In D. Beyer, & D. Zufferey (Eds.), Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings (pp. 202-225). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11990 LNCS). Springer. https://doi.org/10.1007/978-3-030-39322-9_10