Assume-guarantee and case splitting

Assume-guarantee

When two blocks A and B talk to each other, a property of the combined system can be proven in pieces:

1. Prove block A's outputs obey interface rule R, assuming B behaves according to rule S.
2. Prove block B's outputs obey S, assuming A behaves according to R.
3. Prove the system property on a model where A and B are replaced (or simplified) using R and S.

Circular reasoning is a risk: for safety properties it is sound when each step is proven "up to time t" for all t, which is what tools do — but be careful with liveness. The reusable protocol checker from Chapter 7, with its assume/assert flip, is exactly this method applied to a single interface.

Case splitting

If a design has several modes, prove each mode separately by adding a mode assumption per run:

// run 1:  m_mode: assume property (mode == 2'd0);
// run 2:  m_mode: assume property (mode == 2'd1);
// run 3:  m_mode: assume property (mode == 2'd2);
// run 4:  m_mode: assume property (mode == 2'd3);
// plus, if mode can change at run time, a run with mode free (possibly bounded)

Case splits are under-approximations: the set of cases must be complete (all modes) and the mode must truly be static, or you need an extra run covering mode changes.