Leveraging Piecewise Composition to Infer Environment Constraints for Hardware Designs
Kaki Ryan, Cynthia Sturton · 2025
We introduce a symbolic execution-based framework to generate the environment constraints needed to formally verify a hardware design. The core of the approach is a new search strategy that leverages piecewise composition, a divide-and-conquer algorithm introduced in prior work, to guide symbolic execution toward paths more likely to generate needed environment constraints. In our preliminary evaluation using the decoder module of the OpenTitan SoC, the framework finds the needed constraints without overconstraining the environment.