Skip to main content

Synthesizing Environment Invariants for Modular Hardware Verification

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

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1s546
Full metadata record
DC FieldValueLanguage
dc.contributor.authorZhang, Hongce-
dc.contributor.authorYang, Weikun-
dc.contributor.authorFedyukovich, Grigory-
dc.contributor.authorGupta, Aarti-
dc.contributor.authorMalik, Sharad-
dc.date.accessioned2021-10-08T19:46:52Z-
dc.date.available2021-10-08T19:46:52Z-
dc.date.issued2020en_US
dc.identifier.citationZhang, 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_10en_US
dc.identifier.issn0302-9743-
dc.identifier.urihttps://bo-yuan-huang.github.io/ILAng-Doc/vmcai20.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1s546-
dc.description.abstractWe 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.en_US
dc.format.extent202 - 225en_US
dc.language.isoen_USen_US
dc.relation.ispartofInternational Conference on Verification, Model Checking, and Abstract Interpretationen_US
dc.rightsAuthor's manuscripten_US
dc.titleSynthesizing Environment Invariants for Modular Hardware Verificationen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1007/978-3-030-39322-9_10-
dc.identifier.eissn1611-3349-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
EnvironmentInvariantModularHardwareVerif.pdf2.07 MBAdobe PDFView/Download


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