[hw] Add SVA assert property for !(contr_rd_inflight && contr_rd_pending) invariant #24

Context

In MAST PR #19 (merged 2026-05-06), the contr_rd_* arbiter has two state bits in src/global_mem_controller.sv:

• contr_rd_inflight — set when a contr_rd is mid-AXI4-transaction
• contr_rd_pending — set when a contr_rd_en pulse arrives but cannot be serviced this cycle

The state machine guarantees these are never simultaneously true: when grant_contr_rd fires, both contr_rd_inflight is set AND contr_rd_pending is cleared (lines 207-211).

Action

Add a SystemVerilog assertion to make the invariant explicit and machine-checkable in simulation:

// Both bits set simultaneously would mean a contr_rd is in flight AND another
// is pending — but grant_contr_rd clears pending the same cycle it sets inflight.
assert property (@(posedge clk) disable iff (!rst)
    !(contr_rd_inflight && contr_rd_pending))
    else $error("Arbiter invariant violated: inflight && pending");

This catches future refactors that might inadvertently break the invariant (e.g. someone changing the grant condition without clearing pending).

Refs

• MAST PR feat(rtl): replace mock global_mem_controller with AXI4 manager skeleton #19: feat(rtl): replace mock global_mem_controller with AXI4 manager skeleton #19
• Review thread, real finding [ci] GitHub Actions workflow for Verilator simulation on PR #4

Authored by Agent R (Reviewer).