Formal plausibility checks for environment constraints

Functional verification of a System-On-Chip (SoC) module requires that the legal behavior of its environment is modeled as part of the verification IP. In early stages of the SoC design process so called environment constraints are used for this purpose. As long as a complete implementation of the environment is not yet available these constraints restrict the inputs of the device under verification to reasonable values. Using such constraints during functional verification, however, imposes a high risk that legal environment behavior is pruned away. In this case some faulty behavior of the DUV may not be stimulated, i.e., the constraints may mask a bug. Since the individual modules of an SoC are usually developed simultaneously it may not be possible to check the constraints against the environment of a module before integration. Detecting verification gaps due to overconstrained environment assumptions at this late stage of the design process, however, requires a step back into module verification and may compromise project closure. In order to overcome this bottleneck of the verification flow we suggest two efficient plausibility checks for constraints that can be conducted without a concrete implementation of the considered environment. Our experimental results show that the proposed techniques detect issues that would otherwise remain undetected at least until module integration. The tests are applicable in both formal and constrained random verification environments.