Erik Seligman, Cadence; Karthik Baddam, Qualcomm
Have you ever worked on a large formal property verification (FPV) problem, and had to decompose the problem into smaller pieces to make it possible? This is a natural technique used during modern design verification, and a necessity due to the inherent complexity of the “model checking” problem, the main problem addressed by current commercial FPV tools. Usually such decomposition is handled by writing ad hoc user-level scripts. These scripts define the various pieces of the problem, and assemble the results together in the end to ensure the design is fully validated. However, this reliance on user-level scripts creates a key avenue for potential errors or escapes; indeed, we have seen numerous real-life cases where the subdivided problem was run perfectly on the tools, but an error was made during assembly or in porting specifications from a previous project. In this paper we present a new FPV tool concept, “Proof Structure”, which augments standard model checking to empower the user to carry out this decomposition in a rigorous, well-defined way—with the tool given enough information to prove that the overall results are combined with correct reasoning, or identify any holes in the process. We describe the main operations supported by our current implementation of Proof Structure, and show how it has helped engineers at HPE to achieve convergence on a difficult FPV problem, using multi-step decomposition and gaining high confidence in the overall soundness of their result.
