Helper assertions and invariants

Lesson 2.6 showed why induction fails on unreachable states and how a helper assertion fixes it. In real designs, helpers usually relate several pieces of state. Good sources of helper invariants:

• Encodings: FSM state is one-hot; a pointer is less than its depth.
• Relationships: count == wptr - rptr; credits plus in-flight packets equal the maximum.
• Mutual exclusion: two FSMs are never both in their "owner" state.
• Shadow / redundant state: a registered copy equals the original one cycle later.

// Credit-based link: credits available + packets in flight + slots used downstream == MAX
// (sender, wire pipeline and receiver all in one formal model)
a_credit_conservation: assert property (
    sender.credits + CW'($countones(pipe_valid)) + receiver.used == CW'(MAX_CREDITS));

A helper like this is often the difference between a proof that runs forever and one that finishes in seconds, because it lets induction ignore the vast number of states where the counts do not add up.