Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning

Finite-state verification techniques are often hampered by the state-explosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. We were interested in determining if assume-guarantee reasoning could provide an ad-vantage over monolithic verification. Using recent advances in assume-guarantee reasoning that automatically generate assump-tions, we undertook a study that considered all two-way decompo-sitions for a set of systems and properties, using two different veri-fiers. By increasing the number of repeated tasks for a system, we evaluated the decompositions as the systems were scaled. In very few cases were we able to show that assume-guarantee reasoning could verify properties on larger systems than monolithic verifica-tion could. Additionally, assume-guarantee reasoning could only verify these properties on systems a few sizes larger than mono-lithic verification. This negative result, although preliminary, raises doubts about the usefulness of assume-guarantee reasoning as an effective technique