Skip to main content

Synthesizing Environment Invariants for Modular Hardware Verification

Author(s): Zhang, Hongce; Yang, Weikun; Fedyukovich, Grigory; Gupta, Aarti; Malik, Sharad

To refer to this page use:
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.
Publication Date: 2020
Citation: Zhang, Hongce, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, and Sharad Malik. "Synthesizing Environment Invariants for Modular Hardware Verification." In International Conference on Verification, Model Checking, and Abstract Interpretation (2020): pp. 202-225. doi:10.1007/978-3-030-39322-9_10
DOI: 10.1007/978-3-030-39322-9_10
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 202 - 225
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Verification, Model Checking, and Abstract Interpretation
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.