Synthesizing Environment Invariants for Modular Hardware Verification

In Verification, Model Checking, and Abstract Interpretation

Environment invariants are needed in modular hardware verification where functional equivalence is proved between a high-level specification and a low-level implementation. We automate the synthesis of such environment invariants using syntax-guided synthesis (SyGuS) technique. Invariants are generated and iteratively strengthened by reachability queries in a counterexample-guided abstraction refinement (CEGAR) loop. Our experiments show that the proposed SyGuS-based technique complements or outperforms existing property-directed reachability (PDR) techniques for invariant generation on practical hardware designs.

Hongce Zhang
Hongce Zhang
Assistant Professor in Microelectronics Thrust

My research interest is on hardware formal verification.